Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpaaeu Structured version   Unicode version

Theorem mpaaeu 35463
 Description: An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014.)
Assertion
Ref Expression
mpaaeu Polydeg degAA coeffdegAA
Distinct variable group:   ,

Proof of Theorem mpaaeu
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qsscn 11238 . . . . . 6
2 eldifi 3565 . . . . . . . . . 10 Poly Poly
32ad2antlr 725 . . . . . . . . 9 Poly deg degAA Poly
4 zssq 11234 . . . . . . . . . 10
5 0z 10916 . . . . . . . . . 10
64, 5sselii 3439 . . . . . . . . 9
7 eqid 2402 . . . . . . . . . 10 coeff coeff
87coef2 22920 . . . . . . . . 9 Poly coeff
93, 6, 8sylancl 660 . . . . . . . 8 Poly deg degAA coeff
10 dgrcl 22922 . . . . . . . . 9 Poly deg
113, 10syl 17 . . . . . . . 8 Poly deg degAA deg
129, 11ffvelrnd 6010 . . . . . . 7 Poly deg degAA coeffdeg
13 eldifsni 4098 . . . . . . . . 9 Poly
1413ad2antlr 725 . . . . . . . 8 Poly deg degAA
15 eqid 2402 . . . . . . . . . . 11 deg deg
1615, 7dgreq0 22954 . . . . . . . . . 10 Poly coeffdeg
1716necon3bid 2661 . . . . . . . . 9 Poly coeffdeg
183, 17syl 17 . . . . . . . 8 Poly deg degAA coeffdeg
1914, 18mpbid 210 . . . . . . 7 Poly deg degAA coeffdeg
20 qreccl 11247 . . . . . . 7 coeffdeg coeffdeg coeffdeg
2112, 19, 20syl2anc 659 . . . . . 6 Poly deg degAA coeffdeg
22 plyconst 22895 . . . . . 6 coeffdeg coeffdeg Poly
231, 21, 22sylancr 661 . . . . 5 Poly deg degAA coeffdeg Poly
24 simpl 455 . . . . . 6 coeffdeg Poly Poly coeffdeg Poly
25 simpr 459 . . . . . 6 coeffdeg Poly Poly Poly
26 qaddcl 11243 . . . . . . 7
2726adantl 464 . . . . . 6 coeffdeg Poly Poly
28 qmulcl 11245 . . . . . . 7
2928adantl 464 . . . . . 6 coeffdeg Poly Poly
3024, 25, 27, 29plymul 22907 . . . . 5 coeffdeg Poly Poly coeffdeg Poly
3123, 3, 30syl2anc 659 . . . 4 Poly deg degAA coeffdeg Poly
327coef3 22921 . . . . . . . . 9 Poly coeff
333, 32syl 17 . . . . . . . 8 Poly deg degAA coeff
3433, 11ffvelrnd 6010 . . . . . . 7 Poly deg degAA coeffdeg
3534, 19reccld 10354 . . . . . 6 Poly deg degAA coeffdeg
3634, 19recne0d 10355 . . . . . 6 Poly deg degAA coeffdeg
37 dgrmulc 22960 . . . . . 6 coeffdeg coeffdeg Poly deg coeffdeg deg
3835, 36, 3, 37syl3anc 1230 . . . . 5 Poly deg degAA deg coeffdeg deg
39 simprl 756 . . . . 5 Poly deg degAA deg degAA
4038, 39eqtrd 2443 . . . 4 Poly deg degAA deg coeffdeg degAA
41 aacn 23005 . . . . . . 7
4241ad2antrr 724 . . . . . 6 Poly deg degAA
43 ovex 6306 . . . . . . . 8 coeffdeg
44 fnconstg 5756 . . . . . . . 8 coeffdeg coeffdeg
4543, 44mp1i 13 . . . . . . 7 Poly deg degAA coeffdeg
46 plyf 22887 . . . . . . . 8 Poly
47 ffn 5714 . . . . . . . 8
483, 46, 473syl 18 . . . . . . 7 Poly deg degAA
49 cnex 9603 . . . . . . . 8
5049a1i 11 . . . . . . 7 Poly deg degAA
51 inidm 3648 . . . . . . 7
5243fvconst2 6107 . . . . . . . 8 coeffdeg coeffdeg
5352adantl 464 . . . . . . 7 Poly deg degAA coeffdeg coeffdeg
54 simplrr 763 . . . . . . 7 Poly deg degAA
5545, 48, 50, 50, 51, 53, 54ofval 6530 . . . . . 6 Poly deg degAA coeffdeg coeffdeg
5642, 55mpdan 666 . . . . 5 Poly deg degAA coeffdeg coeffdeg
5735mul01d 9813 . . . . 5 Poly deg degAA coeffdeg
5856, 57eqtrd 2443 . . . 4 Poly deg degAA coeffdeg
59 coemulc 22944 . . . . . . 7 coeffdeg Poly coeff coeffdeg coeffdeg coeff
6035, 3, 59syl2anc 659 . . . . . 6 Poly deg degAA coeff coeffdeg coeffdeg coeff
6160fveq1d 5851 . . . . 5 Poly deg degAA coeff coeffdeg degAA coeffdeg coeffdegAA
62 dgraacl 35459 . . . . . . . 8 degAA
6362ad2antrr 724 . . . . . . 7 Poly deg degAA degAA
6463nnnn0d 10893 . . . . . 6 Poly deg degAA degAA
65 fnconstg 5756 . . . . . . . 8 coeffdeg coeffdeg
6643, 65mp1i 13 . . . . . . 7 Poly deg degAA coeffdeg
67 ffn 5714 . . . . . . . 8 coeff coeff
6833, 67syl 17 . . . . . . 7 Poly deg degAA coeff
69 nn0ex 10842 . . . . . . . 8
7069a1i 11 . . . . . . 7 Poly deg degAA
71 inidm 3648 . . . . . . 7
7243fvconst2 6107 . . . . . . . 8 degAA coeffdegdegAA coeffdeg
7372adantl 464 . . . . . . 7 Poly deg degAA degAA coeffdegdegAA coeffdeg
74 simplrl 762 . . . . . . . . 9 Poly deg degAA degAA deg degAA
7574eqcomd 2410 . . . . . . . 8 Poly deg degAA degAA degAA deg
7675fveq2d 5853 . . . . . . 7 Poly deg degAA degAA coeffdegAA coeffdeg
7766, 68, 70, 70, 71, 73, 76ofval 6530 . . . . . 6 Poly deg degAA degAA coeffdeg coeffdegAA coeffdeg coeffdeg
7864, 77mpdan 666 . . . . 5 Poly deg degAA coeffdeg coeffdegAA coeffdeg coeffdeg
7934, 19recid2d 10357 . . . . 5 Poly deg degAA coeffdeg coeffdeg
8061, 78, 793eqtrd 2447 . . . 4 Poly deg degAA coeff coeffdeg degAA
81 fveq2 5849 . . . . . . 7 coeffdeg deg deg coeffdeg
8281eqeq1d 2404 . . . . . 6 coeffdeg deg degAA deg coeffdeg degAA
83 fveq1 5848 . . . . . . 7 coeffdeg coeffdeg
8483eqeq1d 2404 . . . . . 6 coeffdeg coeffdeg
85 fveq2 5849 . . . . . . . 8 coeffdeg coeff coeff coeffdeg
8685fveq1d 5851 . . . . . . 7 coeffdeg coeffdegAA coeff coeffdeg degAA
8786eqeq1d 2404 . . . . . 6 coeffdeg coeffdegAA coeff coeffdeg degAA
8882, 84, 873anbi123d 1301 . . . . 5 coeffdeg deg degAA coeffdegAA deg coeffdeg degAA coeffdeg coeff coeffdeg degAA
8988rspcev 3160 . . . 4 coeffdeg Poly deg coeffdeg degAA coeffdeg coeff coeffdeg degAA Polydeg degAA coeffdegAA
9031, 40, 58, 80, 89syl13anc 1232 . . 3 Poly deg degAA Polydeg degAA coeffdegAA
91 dgraalem 35458 . . . 4 degAA Poly deg degAA
9291simprd 461 . . 3 Poly deg degAA
9390, 92r19.29a 2949 . 2 Polydeg degAA coeffdegAA
94 simp2 998 . . . . . . . . . . 11 deg degAA coeffdegAA
95 simp2 998 . . . . . . . . . . 11 deg degAA coeffdegAA
9694, 95anim12i 564 . . . . . . . . . 10 deg degAA coeffdegAA deg degAA coeffdegAA
97 plyf 22887 . . . . . . . . . . . . . . . 16 Poly
98 ffn 5714 . . . . . . . . . . . . . . . 16
9997, 98syl 17 . . . . . . . . . . . . . . 15 Poly
10099ad2antrr 724 . . . . . . . . . . . . . 14 Poly Poly
10146, 47syl 17 . . . . . . . . . . . . . . 15 Poly
102101ad2antlr 725 . . . . . . . . . . . . . 14 Poly Poly
10349a1i 11 . . . . . . . . . . . . . 14 Poly Poly
104 simplrl 762 . . . . . . . . . . . . . 14 Poly Poly
105 simplrr 763 . . . . . . . . . . . . . 14 Poly Poly
106100, 102, 103, 103, 51, 104, 105ofval 6530 . . . . . . . . . . . . 13 Poly Poly
10741, 106sylan2 472 . . . . . . . . . . . 12 Poly Poly
108 0m0e0 10686 . . . . . . . . . . . 12
109107, 108syl6eq 2459 . . . . . . . . . . 11 Poly Poly
110109ex 432 . . . . . . . . . 10 Poly Poly
11196, 110sylan2 472 . . . . . . . . 9 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
112111com12 29 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
113112impl 618 . . . . . . 7 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
114 simpll 752 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
115 simpl 455 . . . . . . . . . 10 Poly Poly Poly
116 simpr 459 . . . . . . . . . 10 Poly Poly Poly
11726adantl 464 . . . . . . . . . 10 Poly Poly
11828adantl 464 . . . . . . . . . 10 Poly Poly
119 1z 10935 . . . . . . . . . . . 12
120 zq 11233 . . . . . . . . . . . 12
121 qnegcl 11244 . . . . . . . . . . . 12
122119, 120, 121mp2b 10 . . . . . . . . . . 11
123122a1i 11 . . . . . . . . . 10 Poly Poly
124115, 116, 117, 118, 123plysub 22908 . . . . . . . . 9 Poly Poly Poly
125124ad2antlr 725 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
126 simplrl 762 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
127 simplrr 763 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
128 simprr1 1045 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
129 simprl1 1042 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
130128, 129eqtr4d 2446 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg deg
13162ad2antrr 724 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA degAA
132129, 131eqeltrd 2490 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg
133 simprl3 1044 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdegAA
134129fveq2d 5853 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA
135129fveq2d 5853 . . . . . . . . . . . 12 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA
136 simprr3 1047 . . . . . . . . . . . 12 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdegAA
137135, 136eqtrd 2443 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg
138133, 134, 1373eqtr4d 2453 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdeg
139 eqid 2402 . . . . . . . . . . 11 deg deg
140139dgrsub2 35448 . . . . . . . . . 10 Poly Poly deg deg deg coeffdeg coeffdeg deg deg
141126, 127, 130, 132, 138, 140syl23anc 1237 . . . . . . . . 9 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg deg
142141, 129breqtrd 4419 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
143 dgraa0p 35462 . . . . . . . 8 Poly deg degAA
144114, 125, 142, 143syl3anc 1230 . . . . . . 7 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
145113, 144mpbid 210 . . . . . 6 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
146 df-0p 22369 . . . . . 6
147145, 146syl6eq 2459 . . . . 5 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
148 ofsubeq0 10573 . . . . . . . 8
14949, 148mp3an1 1313 . . . . . . 7
15097, 46, 149syl2an 475 . . . . . 6 Poly Poly
151150ad2antlr 725 . . . . 5 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
152147, 151mpbid 210 . . . 4 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
153152ex 432 . . 3 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
154153ralrimivva 2825 . 2 Poly Polydeg degAA coeffdegAA deg degAA coeffdegAA
155 fveq2 5849 . . . . 5 deg deg
156155eqeq1d 2404 . . . 4 deg degAA deg degAA
157 fveq1 5848 . . . . 5
158157eqeq1d 2404 . . . 4
159 fveq2 5849 . . . . . 6 coeff coeff
160159fveq1d 5851 . . . . 5 coeffdegAA coeffdegAA
161160eqeq1d 2404 . . . 4 coeffdegAA coeffdegAA
162156, 158, 1613anbi123d 1301 . . 3 deg degAA coeffdegAA deg degAA coeffdegAA
163162reu4 3243 . 2 Polydeg degAA coeffdegAA Polydeg degAA coeffdegAA Poly Polydeg degAA coeffdegAA deg degAA coeffdegAA
16493, 154, 163sylanbrc 662 1 Polydeg degAA coeffdegAA
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   w3a 974   wceq 1405   wcel 1842   wne 2598  wral 2754  wrex 2755  wreu 2756  cvv 3059   cdif 3411   wss 3414  csn 3972   class class class wbr 4395   cxp 4821   wfn 5564  wf 5565  cfv 5569  (class class class)co 6278   cof 6519  cc 9520  cc0 9522  c1 9523   caddc 9525   cmul 9527   clt 9658   cmin 9841  cneg 9842   cdiv 10247  cn 10576  cn0 10836  cz 10905  cq 11227  c0p 22368  Polycply 22873  coeffccoe 22875  degcdgr 22876  caa 23002  degAAcdgraa 35453 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-inf2 8091  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600  ax-addf 9601 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-se 4783  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-isom 5578  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6521  df-om 6684  df-1st 6784  df-2nd 6785  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-map 7459  df-pm 7460  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-sup 7935  df-oi 7969  df-card 8352  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-n0 10837  df-z 10906  df-uz 11128  df-q 11228  df-rp 11266  df-fz 11727  df-fzo 11855  df-fl 11966  df-mod 12035  df-seq 12152  df-exp 12211  df-hash 12453  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-clim 13460  df-rlim 13461  df-sum 13658  df-0p 22369  df-ply 22877  df-coe 22879  df-dgr 22880  df-aa 23003  df-dgraa 35455 This theorem is referenced by:  mpaalem  35465
 Copyright terms: Public domain W3C validator