Finish intuitionizing section "Elementary properties of complex polynomials" (#5075)

* Add df-quot to mmil.html

Adjust text on Metamath 100 item #89 accordingly.

* Add missing link in mmil.html

The text referred to an nCat page but neglected to link it.  Also
include the key point from that page in case it changes.

* copy dvply2 from set.mm to iset.mm

* add dvnply2 to mmil.html

* add dvnply to mmil.html

* add plycpn to mmil.html

Author: jkingdon

iset.mm

@@ -180499,6 +180499,14 @@ theorem as stated here (although versions with additional conditions,
       OXKARYQUUPUUGUWGAXLXJUWHUVAUWNXMXNUWHQAUVAYSUWHUVQQAYSVCUURUVQUWGUVRSUWHU
       UHAYSQUWHUUBARUUHANUWHMAYOMAGZYQUUPUUGUWGYOAEXOFGUWQAEXPAEMXQXRWBXJXSUUBA
       YBXTYAYKUWNXCAEUWLUVAUVBUFUGYCYDXHYEYFYGYHYLYIYJYMYN $.
+
+    $( The derivative of a polynomial is a polynomial.  (Contributed by Stefan
+       O'Rear, 14-Nov-2014.)  (Proof shortened by Mario Carneiro,
+       1-Jan-2017.) $)
+    dvply2 $p |- ( F e. ( Poly ` S ) -> ( CC _D F ) e. ( Poly ` CC ) ) $=
+      ( cply cfv wcel cc ccnfld csubrg cdv co crg cnring cnfldbas subrgid ax-mp
+      plyssc sseli dvply2g sylancr ) BACDZEFGHDEZBFCDZEFBIJUBEGKEUALFGMNOTUBBAP
+      QFBRS $.
   $}
 
 

mmil.raw.html

@@ -14399,6 +14399,27 @@
   <td>the set.mm proof uses mul0ord</td>
 </tr>
 
+<tr>
+  <td>dvnply2 , dvnply</td>
+  <td><i>none</i></td>
+  <td>should be feasible once Dn syntax is defined</td>
+</tr>
+
+<tr>
+  <td>plycpn</td>
+  <td><i>none</i></td>
+  <td>should be feasible once C^n syntax is defined</td>
+</tr>
+
+<tr>
+  <td id="missing-df-quot">df-quot</td>
+  <td><i>none</i></td>
+  <td>there might be issues around comparing to 0p but perhaps
+  even more fundamentally, the definition is saying the
+  degree of the remainder is less than the degree of the divisor
+  and it isn't clear that we can compare degrees like that</td>
+</tr>
+
 <tr>
   <td>fta1</td>
   <td><i>none</i></td>
@@ -15530,9 +15551,13 @@ <h2 style="border-top: 1px solid black; color: #006633; font-weight: bold; margi
   <tr>
     <td>67.  <i>e</i> is Transcendental</td>
     <td>There's a lot to develop in terms of polynomials
-    and algebraic numbers.  Also see <a href="">transcendental
-    number</a> at ncatlab concerning how we should
-    define transcendental.</td>
+    and algebraic numbers.  Also see <a
+    href="https://ncatlab.org/nlab/show/transcendental+number"
+    >transcendental
+    number</a> at nLab concerning how we should
+    define transcendental (probably the best definition
+    is that a transcendental number is one which is apart from
+    any algebraic number).</td>
   </tr>
 
   <tr>
@@ -15613,7 +15638,10 @@ <h2 style="border-top: 1px solid black; color: #006633; font-weight: bold; margi
 
   <tr>
     <td>89.  The Factor and Remainder Theorems</td>
-    <td>Requires further development of polynomials.</td>
+    <td>The question is whether quotient is well enough defined for
+    these theorems, and/or whether there is a way to state the theorems
+    so they would imply a taboo. Also see the <a href="#missing-df-quot"
+    >df-quot entry</a> above.</td>
   </tr>
 
   <tr>