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

Theorem mpaaeu 27223
 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 dgraalem 27218 . . . 4 degAA Poly deg degAA
21simprd 450 . . 3 Poly deg degAA
3 qsscn 10541 . . . . . . . 8
4 eldifi 3429 . . . . . . . . . . . 12 Poly Poly
54ad2antlr 708 . . . . . . . . . . 11 Poly deg degAA Poly
6 zssq 10537 . . . . . . . . . . . 12
7 0z 10249 . . . . . . . . . . . 12
86, 7sselii 3305 . . . . . . . . . . 11
9 eqid 2404 . . . . . . . . . . . 12 coeff coeff
109coef2 20103 . . . . . . . . . . 11 Poly coeff
115, 8, 10sylancl 644 . . . . . . . . . 10 Poly deg degAA coeff
12 dgrcl 20105 . . . . . . . . . . 11 Poly deg
135, 12syl 16 . . . . . . . . . 10 Poly deg degAA deg
1411, 13ffvelrnd 5830 . . . . . . . . 9 Poly deg degAA coeffdeg
15 eldifsni 3888 . . . . . . . . . . 11 Poly
1615ad2antlr 708 . . . . . . . . . 10 Poly deg degAA
17 eqid 2404 . . . . . . . . . . . . 13 deg deg
1817, 9dgreq0 20136 . . . . . . . . . . . 12 Poly coeffdeg
1918necon3bid 2602 . . . . . . . . . . 11 Poly coeffdeg
205, 19syl 16 . . . . . . . . . 10 Poly deg degAA coeffdeg
2116, 20mpbid 202 . . . . . . . . 9 Poly deg degAA coeffdeg
22 qreccl 10550 . . . . . . . . 9 coeffdeg coeffdeg coeffdeg
2314, 21, 22syl2anc 643 . . . . . . . 8 Poly deg degAA coeffdeg
24 plyconst 20078 . . . . . . . 8 coeffdeg coeffdeg Poly
253, 23, 24sylancr 645 . . . . . . 7 Poly deg degAA coeffdeg Poly
26 simpl 444 . . . . . . . 8 coeffdeg Poly Poly coeffdeg Poly
27 simpr 448 . . . . . . . 8 coeffdeg Poly Poly Poly
28 qaddcl 10546 . . . . . . . . 9
2928adantl 453 . . . . . . . 8 coeffdeg Poly Poly
30 qmulcl 10548 . . . . . . . . 9
3130adantl 453 . . . . . . . 8 coeffdeg Poly Poly
3226, 27, 29, 31plymul 20090 . . . . . . 7 coeffdeg Poly Poly coeffdeg Poly
3325, 5, 32syl2anc 643 . . . . . 6 Poly deg degAA coeffdeg Poly
349coef3 20104 . . . . . . . . . . 11 Poly coeff
355, 34syl 16 . . . . . . . . . 10 Poly deg degAA coeff
3635, 13ffvelrnd 5830 . . . . . . . . 9 Poly deg degAA coeffdeg
3736, 21reccld 9739 . . . . . . . 8 Poly deg degAA coeffdeg
3836, 21recne0d 9740 . . . . . . . 8 Poly deg degAA coeffdeg
39 dgrmulc 20142 . . . . . . . 8 coeffdeg coeffdeg Poly deg coeffdeg deg
4037, 38, 5, 39syl3anc 1184 . . . . . . 7 Poly deg degAA deg coeffdeg deg
41 simprl 733 . . . . . . 7 Poly deg degAA deg degAA
4240, 41eqtrd 2436 . . . . . 6 Poly deg degAA deg coeffdeg degAA
43 aacn 20187 . . . . . . . . 9
4443ad2antrr 707 . . . . . . . 8 Poly deg degAA
45 ovex 6065 . . . . . . . . . 10 coeffdeg
46 fnconstg 5590 . . . . . . . . . 10 coeffdeg coeffdeg
4745, 46mp1i 12 . . . . . . . . 9 Poly deg degAA coeffdeg
48 plyf 20070 . . . . . . . . . 10 Poly
49 ffn 5550 . . . . . . . . . 10
505, 48, 493syl 19 . . . . . . . . 9 Poly deg degAA
51 cnex 9027 . . . . . . . . . 10
5251a1i 11 . . . . . . . . 9 Poly deg degAA
53 inidm 3510 . . . . . . . . 9
5445fvconst2 5906 . . . . . . . . . 10 coeffdeg coeffdeg
5554adantl 453 . . . . . . . . 9 Poly deg degAA coeffdeg coeffdeg
56 simplrr 738 . . . . . . . . 9 Poly deg degAA
5747, 50, 52, 52, 53, 55, 56ofval 6273 . . . . . . . 8 Poly deg degAA coeffdeg coeffdeg
5844, 57mpdan 650 . . . . . . 7 Poly deg degAA coeffdeg coeffdeg
5937mul01d 9221 . . . . . . 7 Poly deg degAA coeffdeg
6058, 59eqtrd 2436 . . . . . 6 Poly deg degAA coeffdeg
61 coemulc 20126 . . . . . . . . 9 coeffdeg Poly coeff coeffdeg coeffdeg coeff
6237, 5, 61syl2anc 643 . . . . . . . 8 Poly deg degAA coeff coeffdeg coeffdeg coeff
6362fveq1d 5689 . . . . . . 7 Poly deg degAA coeff coeffdeg degAA coeffdeg coeffdegAA
64 dgraacl 27219 . . . . . . . . . 10 degAA
6564ad2antrr 707 . . . . . . . . 9 Poly deg degAA degAA
6665nnnn0d 10230 . . . . . . . 8 Poly deg degAA degAA
67 fnconstg 5590 . . . . . . . . . 10 coeffdeg coeffdeg
6845, 67mp1i 12 . . . . . . . . 9 Poly deg degAA coeffdeg
69 ffn 5550 . . . . . . . . . 10 coeff coeff
7035, 69syl 16 . . . . . . . . 9 Poly deg degAA coeff
71 nn0ex 10183 . . . . . . . . . 10
7271a1i 11 . . . . . . . . 9 Poly deg degAA
73 inidm 3510 . . . . . . . . 9
7445fvconst2 5906 . . . . . . . . . 10 degAA coeffdegdegAA coeffdeg
7574adantl 453 . . . . . . . . 9 Poly deg degAA degAA coeffdegdegAA coeffdeg
76 simplrl 737 . . . . . . . . . . 11 Poly deg degAA degAA deg degAA
7776eqcomd 2409 . . . . . . . . . 10 Poly deg degAA degAA degAA deg
7877fveq2d 5691 . . . . . . . . 9 Poly deg degAA degAA coeffdegAA coeffdeg
7968, 70, 72, 72, 73, 75, 78ofval 6273 . . . . . . . 8 Poly deg degAA degAA coeffdeg coeffdegAA coeffdeg coeffdeg
8066, 79mpdan 650 . . . . . . 7 Poly deg degAA coeffdeg coeffdegAA coeffdeg coeffdeg
8136, 21recid2d 9742 . . . . . . 7 Poly deg degAA coeffdeg coeffdeg
8263, 80, 813eqtrd 2440 . . . . . 6 Poly deg degAA coeff coeffdeg degAA
83 fveq2 5687 . . . . . . . . 9 coeffdeg deg deg coeffdeg
8483eqeq1d 2412 . . . . . . . 8 coeffdeg deg degAA deg coeffdeg degAA
85 fveq1 5686 . . . . . . . . 9 coeffdeg coeffdeg
8685eqeq1d 2412 . . . . . . . 8 coeffdeg coeffdeg
87 fveq2 5687 . . . . . . . . . 10 coeffdeg coeff coeff coeffdeg
8887fveq1d 5689 . . . . . . . . 9 coeffdeg coeffdegAA coeff coeffdeg degAA
8988eqeq1d 2412 . . . . . . . 8 coeffdeg coeffdegAA coeff coeffdeg degAA
9084, 86, 893anbi123d 1254 . . . . . . 7 coeffdeg deg degAA coeffdegAA deg coeffdeg degAA coeffdeg coeff coeffdeg degAA
9190rspcev 3012 . . . . . 6 coeffdeg Poly deg coeffdeg degAA coeffdeg coeff coeffdeg degAA Polydeg degAA coeffdegAA
9233, 42, 60, 82, 91syl13anc 1186 . . . . 5 Poly deg degAA Polydeg degAA coeffdegAA
9392ex 424 . . . 4 Poly deg degAA Polydeg degAA coeffdegAA
9493rexlimdva 2790 . . 3 Poly deg degAA Polydeg degAA coeffdegAA
952, 94mpd 15 . 2 Polydeg degAA coeffdegAA
96 simp2 958 . . . . . . . . . . 11 deg degAA coeffdegAA
97 simp2 958 . . . . . . . . . . 11 deg degAA coeffdegAA
9896, 97anim12i 550 . . . . . . . . . 10 deg degAA coeffdegAA deg degAA coeffdegAA
99 plyf 20070 . . . . . . . . . . . . . . . 16 Poly
100 ffn 5550 . . . . . . . . . . . . . . . 16
10199, 100syl 16 . . . . . . . . . . . . . . 15 Poly
102101ad2antrr 707 . . . . . . . . . . . . . 14 Poly Poly
10348, 49syl 16 . . . . . . . . . . . . . . 15 Poly
104103ad2antlr 708 . . . . . . . . . . . . . 14 Poly Poly
10551a1i 11 . . . . . . . . . . . . . 14 Poly Poly
106 simplrl 737 . . . . . . . . . . . . . 14 Poly Poly
107 simplrr 738 . . . . . . . . . . . . . 14 Poly Poly
108102, 104, 105, 105, 53, 106, 107ofval 6273 . . . . . . . . . . . . 13 Poly Poly
10943, 108sylan2 461 . . . . . . . . . . . 12 Poly Poly
110 0cn 9040 . . . . . . . . . . . . 13
111110subid1i 9328 . . . . . . . . . . . 12
112109, 111syl6eq 2452 . . . . . . . . . . 11 Poly Poly
113112ex 424 . . . . . . . . . 10 Poly Poly
11498, 113sylan2 461 . . . . . . . . 9 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
115114com12 29 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
116115impl 604 . . . . . . 7 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
117 simpll 731 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
118 simpl 444 . . . . . . . . . 10 Poly Poly Poly
119 simpr 448 . . . . . . . . . 10 Poly Poly Poly
12028adantl 453 . . . . . . . . . 10 Poly Poly
12130adantl 453 . . . . . . . . . 10 Poly Poly
122 1z 10267 . . . . . . . . . . . 12
123 zq 10536 . . . . . . . . . . . 12
124 qnegcl 10547 . . . . . . . . . . . 12
125122, 123, 124mp2b 10 . . . . . . . . . . 11
126125a1i 11 . . . . . . . . . 10 Poly Poly
127118, 119, 120, 121, 126plysub 20091 . . . . . . . . 9 Poly Poly Poly
128127ad2antlr 708 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
129 simplrl 737 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
130 simplrr 738 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA Poly
131 simprr1 1005 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
132 simprl1 1002 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
133131, 132eqtr4d 2439 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg deg
13464ad2antrr 707 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA degAA
135132, 134eqeltrd 2478 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg
136 simprl3 1004 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdegAA
137132fveq2d 5691 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA
138132fveq2d 5691 . . . . . . . . . . . 12 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdegAA
139 simprr3 1007 . . . . . . . . . . . 12 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdegAA
140138, 139eqtrd 2436 . . . . . . . . . . 11 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg
141136, 137, 1403eqtr4d 2446 . . . . . . . . . 10 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA coeffdeg coeffdeg
142 eqid 2404 . . . . . . . . . . 11 deg deg
143142dgrsub2 27207 . . . . . . . . . 10 Poly Poly deg deg deg coeffdeg coeffdeg deg deg
144129, 130, 133, 135, 141, 143syl23anc 1191 . . . . . . . . 9 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg deg
145144, 132breqtrd 4196 . . . . . . . 8 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA deg degAA
146 dgraa0p 27222 . . . . . . . 8 Poly deg degAA
147117, 128, 145, 146syl3anc 1184 . . . . . . 7 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
148116, 147mpbid 202 . . . . . 6 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
149 df-0p 19515 . . . . . 6
150148, 149syl6eq 2452 . . . . 5 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
151 ofsubeq0 9953 . . . . . . . 8
15251, 151mp3an1 1266 . . . . . . 7
15399, 48, 152syl2an 464 . . . . . 6 Poly Poly
154153ad2antlr 708 . . . . 5 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
155150, 154mpbid 202 . . . 4 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
156155ex 424 . . 3 Poly Poly deg degAA coeffdegAA deg degAA coeffdegAA
157156ralrimivva 2758 . 2 Poly Polydeg degAA coeffdegAA deg degAA coeffdegAA
158 fveq2 5687 . . . . 5 deg deg
159158eqeq1d 2412 . . . 4 deg degAA deg degAA
160 fveq1 5686 . . . . 5
161160eqeq1d 2412 . . . 4
162 fveq2 5687 . . . . . 6 coeff coeff
163162fveq1d 5689 . . . . 5 coeffdegAA coeffdegAA
164163eqeq1d 2412 . . . 4 coeffdegAA coeffdegAA
165159, 161, 1643anbi123d 1254 . . 3 deg degAA coeffdegAA deg degAA coeffdegAA
166165reu4 3088 . 2 Polydeg degAA coeffdegAA Polydeg degAA coeffdegAA Poly Polydeg degAA coeffdegAA deg degAA coeffdegAA
16795, 157, 166sylanbrc 646 1 Polydeg degAA coeffdegAA
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  wreu 2668  cvv 2916   cdif 3277   wss 3280  csn 3774   class class class wbr 4172   cxp 4835   wfn 5408  wf 5409  cfv 5413  (class class class)co 6040   cof 6262  cc 8944  cc0 8946  c1 8947   caddc 8949   cmul 8951   clt 9076   cmin 9247  cneg 9248   cdiv 9633  cn 9956  cn0 10177  cz 10238  cq 10530  c0p 19514  Polycply 20056  coeffccoe 20058  degcdgr 20059  caa 20184  degAAcdgraa 27213 This theorem is referenced by:  mpaalem  27225 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-0p 19515  df-ply 20060  df-coe 20062  df-dgr 20063  df-aa 20185  df-dgraa 27215
 Copyright terms: Public domain W3C validator