Metamath Proof Explorer

Theorem 2sqr3minply

Description: The polynomial ( ( X ^ 3 ) - 2 ) is the minimal polynomial for ( 2 ^c ( 1 / 3 ) ) over QQ , and its degree is 3 . (Contributed by Thierry Arnoux, 14-Jun-2025)

Ref Expression
Hypotheses 2sqr3minply.q 
|- Q = ( CCfld |`s QQ )
2sqr3minply.1 
|- .- = ( -g ` P )
2sqr3minply.2 
|- .^ = ( .g ` ( mulGrp ` P ) )
2sqr3minply.p 
|- P = ( Poly1 ` Q )
2sqr3minply.k 
|- K = ( algSc ` P )
2sqr3minply.x 
|- X = ( var1 ` Q )
2sqr3minply.d 
|- D = ( deg1 ` Q )
2sqr3minply.f 
|- F = ( ( 3 .^ X ) .- ( K ` 2 ) )
2sqr3minply.a 
|- A = ( 2 ^c ( 1 / 3 ) )
2sqr3minply.m 
|- M = ( CCfld minPoly QQ )
Assertion 2sqr3minply 
|- ( F = ( M ` A ) /\ ( D ` F ) = 3 )

Proof

Step Hyp Ref Expression
1 2sqr3minply.q 
 |-  Q = ( CCfld |`s QQ )
2 2sqr3minply.1 
 |-  .- = ( -g ` P )
3 2sqr3minply.2 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
4 2sqr3minply.p 
 |-  P = ( Poly1 ` Q )
5 2sqr3minply.k 
 |-  K = ( algSc ` P )
6 2sqr3minply.x 
 |-  X = ( var1 ` Q )
7 2sqr3minply.d 
 |-  D = ( deg1 ` Q )
8 2sqr3minply.f 
 |-  F = ( ( 3 .^ X ) .- ( K ` 2 ) )
9 2sqr3minply.a 
 |-  A = ( 2 ^c ( 1 / 3 ) )
10 2sqr3minply.m 
 |-  M = ( CCfld minPoly QQ )
11 eqid 
 |-  ( CCfld evalSub1 QQ ) = ( CCfld evalSub1 QQ )
12 1 fveq2i 
 |-  ( Poly1 ` Q ) = ( Poly1 ` ( CCfld |`s QQ ) )
13 4 12 eqtri 
 |-  P = ( Poly1 ` ( CCfld |`s QQ ) )
14 cnfldbas 
 |-  CC = ( Base ` CCfld )
15 cndrng 
 |-  CCfld e. DivRing
16 cncrng 
 |-  CCfld e. CRing
17 isfld 
 |-  ( CCfld e. Field <-> ( CCfld e. DivRing /\ CCfld e. CRing ) )
18 15 16 17 mpbir2an 
 |-  CCfld e. Field
19 18 a1i 
 |-  ( T. -> CCfld e. Field )
20 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
21 20 simpli 
 |-  QQ e. ( SubRing ` CCfld )
22 20 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
23 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
24 15 21 22 23 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
25 24 a1i 
 |-  ( T. -> QQ e. ( SubDRing ` CCfld ) )
26 2cn 
 |-  2 e. CC
27 3cn 
 |-  3 e. CC
28 3ne0 
 |-  3 =/= 0
29 27 28 reccli 
 |-  ( 1 / 3 ) e. CC
30 cxpcl 
 |-  ( ( 2 e. CC /\ ( 1 / 3 ) e. CC ) -> ( 2 ^c ( 1 / 3 ) ) e. CC )
31 26 29 30 mp2an 
 |-  ( 2 ^c ( 1 / 3 ) ) e. CC
32 9 31 eqeltri 
 |-  A e. CC
33 32 a1i 
 |-  ( T. -> A e. CC )
34 cnfld0 
 |-  0 = ( 0g ` CCfld )
35 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
36 8 fveq2i 
 |-  ( ( CCfld evalSub1 QQ ) ` F ) = ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .- ( K ` 2 ) ) )
37 36 fveq1i 
 |-  ( ( ( CCfld evalSub1 QQ ) ` F ) ` A ) = ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` A )
38 37 a1i 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` A ) = ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` A ) )
39 eqid 
 |-  ( Base ` P ) = ( Base ` P )
40 cnfldsub 
 |-  - = ( -g ` CCfld )
41 16 a1i 
 |-  ( T. -> CCfld e. CRing )
42 21 a1i 
 |-  ( T. -> QQ e. ( SubRing ` CCfld ) )
43 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
44 43 39 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
45 1 qdrng 
 |-  Q e. DivRing
46 45 a1i 
 |-  ( T. -> Q e. DivRing )
47 46 drngringd 
 |-  ( T. -> Q e. Ring )
48 4 ply1ring 
 |-  ( Q e. Ring -> P e. Ring )
49 47 48 syl 
 |-  ( T. -> P e. Ring )
50 43 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
51 49 50 syl 
 |-  ( T. -> ( mulGrp ` P ) e. Mnd )
52 3nn0 
 |-  3 e. NN0
53 52 a1i 
 |-  ( T. -> 3 e. NN0 )
54 6 4 39 vr1cl 
 |-  ( Q e. Ring -> X e. ( Base ` P ) )
55 47 54 syl 
 |-  ( T. -> X e. ( Base ` P ) )
56 44 3 51 53 55 mulgnn0cld 
 |-  ( T. -> ( 3 .^ X ) e. ( Base ` P ) )
57 47 mptru 
 |-  Q e. Ring
58 4 ply1sca 
 |-  ( Q e. Ring -> Q = ( Scalar ` P ) )
59 57 58 ax-mp 
 |-  Q = ( Scalar ` P )
60 4 ply1lmod 
 |-  ( Q e. Ring -> P e. LMod )
61 47 60 syl 
 |-  ( T. -> P e. LMod )
62 1 qrngbas 
 |-  QQ = ( Base ` Q )
63 5 59 49 61 62 39 asclf 
 |-  ( T. -> K : QQ --> ( Base ` P ) )
64 2z 
 |-  2 e. ZZ
65 zq 
 |-  ( 2 e. ZZ -> 2 e. QQ )
66 64 65 mp1i 
 |-  ( T. -> 2 e. QQ )
67 63 66 ffvelcdmd 
 |-  ( T. -> ( K ` 2 ) e. ( Base ` P ) )
68 11 14 4 1 39 2 40 41 42 56 67 33 evls1subd 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` A ) = ( ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) - ( ( ( CCfld evalSub1 QQ ) ` ( K ` 2 ) ) ` A ) ) )
69 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
70 11 14 4 1 39 41 42 3 69 53 55 33 evls1expd 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) = ( 3 ( .g ` ( mulGrp ` CCfld ) ) ( ( ( CCfld evalSub1 QQ ) ` X ) ` A ) ) )
71 11 6 1 14 41 42 evls1var 
 |-  ( T. -> ( ( CCfld evalSub1 QQ ) ` X ) = ( _I |` CC ) )
72 71 fveq1d 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` X ) ` A ) = ( ( _I |` CC ) ` A ) )
73 fvresi 
 |-  ( A e. CC -> ( ( _I |` CC ) ` A ) = A )
74 32 73 mp1i 
 |-  ( T. -> ( ( _I |` CC ) ` A ) = A )
75 72 74 eqtrd 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` X ) ` A ) = A )
76 75 oveq2d 
 |-  ( T. -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) ( ( ( CCfld evalSub1 QQ ) ` X ) ` A ) ) = ( 3 ( .g ` ( mulGrp ` CCfld ) ) A ) )
77 cnfldexp 
 |-  ( ( A e. CC /\ 3 e. NN0 ) -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ 3 ) )
78 33 53 77 syl2anc 
 |-  ( T. -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) A ) = ( A ^ 3 ) )
79 70 76 78 3eqtrd 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) = ( A ^ 3 ) )
80 9 oveq1i 
 |-  ( A ^ 3 ) = ( ( 2 ^c ( 1 / 3 ) ) ^ 3 )
81 3nn 
 |-  3 e. NN
82 cxproot 
 |-  ( ( 2 e. CC /\ 3 e. NN ) -> ( ( 2 ^c ( 1 / 3 ) ) ^ 3 ) = 2 )
83 26 81 82 mp2an 
 |-  ( ( 2 ^c ( 1 / 3 ) ) ^ 3 ) = 2
84 80 83 eqtri 
 |-  ( A ^ 3 ) = 2
85 79 84 eqtrdi 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) = 2 )
86 11 4 1 14 5 41 42 66 33 evls1scafv 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` ( K ` 2 ) ) ` A ) = 2 )
87 85 86 oveq12d 
 |-  ( T. -> ( ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) - ( ( ( CCfld evalSub1 QQ ) ` ( K ` 2 ) ) ` A ) ) = ( 2 - 2 ) )
88 26 subidi 
 |-  ( 2 - 2 ) = 0
89 87 88 eqtrdi 
 |-  ( T. -> ( ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` A ) - ( ( ( CCfld evalSub1 QQ ) ` ( K ` 2 ) ) ` A ) ) = 0 )
90 38 68 89 3eqtrd 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` A ) = 0 )
91 1 qrng0 
 |-  0 = ( 0g ` Q )
92 eqid 
 |-  ( eval1 ` Q ) = ( eval1 ` Q )
93 fldsdrgfld 
 |-  ( ( CCfld e. Field /\ QQ e. ( SubDRing ` CCfld ) ) -> ( CCfld |`s QQ ) e. Field )
94 18 24 93 mp2an 
 |-  ( CCfld |`s QQ ) e. Field
95 1 94 eqeltri 
 |-  Q e. Field
96 95 a1i 
 |-  ( T. -> Q e. Field )
97 49 ringgrpd 
 |-  ( T. -> P e. Grp )
98 39 2 grpsubcl 
 |-  ( ( P e. Grp /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( K ` 2 ) e. ( Base ` P ) ) -> ( ( 3 .^ X ) .- ( K ` 2 ) ) e. ( Base ` P ) )
99 97 56 67 98 syl3anc 
 |-  ( T. -> ( ( 3 .^ X ) .- ( K ` 2 ) ) e. ( Base ` P ) )
100 8 99 eqeltrid 
 |-  ( T. -> F e. ( Base ` P ) )
101 96 fldcrngd 
 |-  ( T. -> Q e. CRing )
102 92 4 39 101 62 100 evl1fvf 
 |-  ( T. -> ( ( eval1 ` Q ) ` F ) : QQ --> QQ )
103 102 ffnd 
 |-  ( T. -> ( ( eval1 ` Q ) ` F ) Fn QQ )
104 fniniseg2 
 |-  ( ( ( eval1 ` Q ) ` F ) Fn QQ -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } )
105 103 104 syl 
 |-  ( T. -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } )
106 cnfldmul 
 |-  x. = ( .r ` CCfld )
107 1 106 ressmulr 
 |-  ( QQ e. ( SubRing ` CCfld ) -> x. = ( .r ` Q ) )
108 21 107 ax-mp 
 |-  x. = ( .r ` Q )
109 cnfldadd 
 |-  + = ( +g ` CCfld )
110 1 109 ressplusg 
 |-  ( QQ e. ( SubRing ` CCfld ) -> + = ( +g ` Q ) )
111 21 110 ax-mp 
 |-  + = ( +g ` Q )
112 eqid 
 |-  ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
113 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
114 8 fveq2i 
 |-  ( coe1 ` F ) = ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) )
115 114 a1i 
 |-  ( T. -> ( coe1 ` F ) = ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) )
116 8 fveq2i 
 |-  ( D ` F ) = ( D ` ( ( 3 .^ X ) .- ( K ` 2 ) ) )
117 116 a1i 
 |-  ( T. -> ( D ` F ) = ( D ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) )
118 3pos 
 |-  0 < 3
119 118 a1i 
 |-  ( T. -> 0 < 3 )
120 2ne0 
 |-  2 =/= 0
121 120 a1i 
 |-  ( T. -> 2 =/= 0 )
122 7 4 62 5 91 deg1scl 
 |-  ( ( Q e. Ring /\ 2 e. QQ /\ 2 =/= 0 ) -> ( D ` ( K ` 2 ) ) = 0 )
123 47 66 121 122 syl3anc 
 |-  ( T. -> ( D ` ( K ` 2 ) ) = 0 )
124 drngnzr 
 |-  ( Q e. DivRing -> Q e. NzRing )
125 45 124 mp1i 
 |-  ( T. -> Q e. NzRing )
126 7 4 6 43 3 deg1pw 
 |-  ( ( Q e. NzRing /\ 3 e. NN0 ) -> ( D ` ( 3 .^ X ) ) = 3 )
127 125 53 126 syl2anc 
 |-  ( T. -> ( D ` ( 3 .^ X ) ) = 3 )
128 119 123 127 3brtr4d 
 |-  ( T. -> ( D ` ( K ` 2 ) ) < ( D ` ( 3 .^ X ) ) )
129 4 7 47 39 2 56 67 128 deg1sub 
 |-  ( T. -> ( D ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) = ( D ` ( 3 .^ X ) ) )
130 117 129 127 3eqtrd 
 |-  ( T. -> ( D ` F ) = 3 )
131 115 130 fveq12d 
 |-  ( T. -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 3 ) )
132 eqid 
 |-  ( -g ` Q ) = ( -g ` Q )
133 4 39 2 132 coe1subfv 
 |-  ( ( ( Q e. Ring /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( K ` 2 ) e. ( Base ` P ) ) /\ 3 e. NN0 ) -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 3 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) )
134 47 56 67 53 133 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 3 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) )
135 subrgsubg 
 |-  ( QQ e. ( SubRing ` CCfld ) -> QQ e. ( SubGrp ` CCfld ) )
136 21 135 mp1i 
 |-  ( T. -> QQ e. ( SubGrp ` CCfld ) )
137 eqid 
 |-  ( coe1 ` ( 3 .^ X ) ) = ( coe1 ` ( 3 .^ X ) )
138 137 39 4 62 coe1fvalcl 
 |-  ( ( ( 3 .^ X ) e. ( Base ` P ) /\ 3 e. NN0 ) -> ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) e. QQ )
139 56 53 138 syl2anc 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) e. QQ )
140 eqid 
 |-  ( coe1 ` ( K ` 2 ) ) = ( coe1 ` ( K ` 2 ) )
141 140 39 4 62 coe1fvalcl 
 |-  ( ( ( K ` 2 ) e. ( Base ` P ) /\ 3 e. NN0 ) -> ( ( coe1 ` ( K ` 2 ) ) ` 3 ) e. QQ )
142 67 53 141 syl2anc 
 |-  ( T. -> ( ( coe1 ` ( K ` 2 ) ) ` 3 ) e. QQ )
143 40 1 132 subgsub 
 |-  ( ( QQ e. ( SubGrp ` CCfld ) /\ ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) e. QQ /\ ( ( coe1 ` ( K ` 2 ) ) ` 3 ) e. QQ ) -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) - ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) )
144 136 139 142 143 syl3anc 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) - ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) )
145 iftrue 
 |-  ( i = 3 -> if ( i = 3 , 1 , 0 ) = 1 )
146 1 qrng1 
 |-  1 = ( 1r ` Q )
147 4 6 3 47 53 91 146 coe1mon 
 |-  ( T. -> ( coe1 ` ( 3 .^ X ) ) = ( i e. NN0 |-> if ( i = 3 , 1 , 0 ) ) )
148 1cnd 
 |-  ( T. -> 1 e. CC )
149 145 147 53 148 fvmptd4 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) = 1 )
150 28 neii 
 |-  -. 3 = 0
151 eqeq1 
 |-  ( i = 3 -> ( i = 0 <-> 3 = 0 ) )
152 150 151 mtbiri 
 |-  ( i = 3 -> -. i = 0 )
153 152 iffalsed 
 |-  ( i = 3 -> if ( i = 0 , 2 , 0 ) = 0 )
154 4 5 62 91 coe1scl 
 |-  ( ( Q e. Ring /\ 2 e. QQ ) -> ( coe1 ` ( K ` 2 ) ) = ( i e. NN0 |-> if ( i = 0 , 2 , 0 ) ) )
155 47 66 154 syl2anc 
 |-  ( T. -> ( coe1 ` ( K ` 2 ) ) = ( i e. NN0 |-> if ( i = 0 , 2 , 0 ) ) )
156 0nn0 
 |-  0 e. NN0
157 156 a1i 
 |-  ( T. -> 0 e. NN0 )
158 153 155 53 157 fvmptd4 
 |-  ( T. -> ( ( coe1 ` ( K ` 2 ) ) ` 3 ) = 0 )
159 149 158 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) - ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) = ( 1 - 0 ) )
160 1m0e1 
 |-  ( 1 - 0 ) = 1
161 159 160 eqtrdi 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) - ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) = 1 )
162 144 161 eqtr3d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 3 ) ) = 1 )
163 131 134 162 3eqtrd 
 |-  ( T. -> ( ( coe1 ` F ) ` ( D ` F ) ) = 1 )
164 130 fveq2d 
 |-  ( T. -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( ( coe1 ` F ) ` 3 ) )
165 163 164 eqtr3d 
 |-  ( T. -> 1 = ( ( coe1 ` F ) ` 3 ) )
166 165 mptru 
 |-  1 = ( ( coe1 ` F ) ` 3 )
167 115 fveq1d 
 |-  ( T. -> ( ( coe1 ` F ) ` 2 ) = ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 2 ) )
168 2nn0 
 |-  2 e. NN0
169 168 a1i 
 |-  ( T. -> 2 e. NN0 )
170 4 39 2 132 coe1subfv 
 |-  ( ( ( Q e. Ring /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( K ` 2 ) e. ( Base ` P ) ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 2 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 2 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 2 ) ) )
171 47 56 67 169 170 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 2 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 2 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 2 ) ) )
172 2re 
 |-  2 e. RR
173 2lt3 
 |-  2 < 3
174 172 173 ltneii 
 |-  2 =/= 3
175 neeq1 
 |-  ( i = 2 -> ( i =/= 3 <-> 2 =/= 3 ) )
176 174 175 mpbiri 
 |-  ( i = 2 -> i =/= 3 )
177 176 adantl 
 |-  ( ( T. /\ i = 2 ) -> i =/= 3 )
178 177 neneqd 
 |-  ( ( T. /\ i = 2 ) -> -. i = 3 )
179 178 iffalsed 
 |-  ( ( T. /\ i = 2 ) -> if ( i = 3 , 1 , 0 ) = 0 )
180 147 179 169 157 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 2 ) = 0 )
181 neeq1 
 |-  ( i = 2 -> ( i =/= 0 <-> 2 =/= 0 ) )
182 120 181 mpbiri 
 |-  ( i = 2 -> i =/= 0 )
183 182 neneqd 
 |-  ( i = 2 -> -. i = 0 )
184 183 adantl 
 |-  ( ( T. /\ i = 2 ) -> -. i = 0 )
185 184 iffalsed 
 |-  ( ( T. /\ i = 2 ) -> if ( i = 0 , 2 , 0 ) = 0 )
186 155 185 169 157 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( K ` 2 ) ) ` 2 ) = 0 )
187 180 186 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 2 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 2 ) ) = ( 0 ( -g ` Q ) 0 ) )
188 171 187 eqtrd 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 2 ) = ( 0 ( -g ` Q ) 0 ) )
189 158 142 eqeltrrd 
 |-  ( T. -> 0 e. QQ )
190 40 1 132 subgsub 
 |-  ( ( QQ e. ( SubGrp ` CCfld ) /\ 0 e. QQ /\ 0 e. QQ ) -> ( 0 - 0 ) = ( 0 ( -g ` Q ) 0 ) )
191 136 189 189 190 syl3anc 
 |-  ( T. -> ( 0 - 0 ) = ( 0 ( -g ` Q ) 0 ) )
192 0m0e0 
 |-  ( 0 - 0 ) = 0
193 191 192 eqtr3di 
 |-  ( T. -> ( 0 ( -g ` Q ) 0 ) = 0 )
194 167 188 193 3eqtrrd 
 |-  ( T. -> 0 = ( ( coe1 ` F ) ` 2 ) )
195 194 mptru 
 |-  0 = ( ( coe1 ` F ) ` 2 )
196 115 fveq1d 
 |-  ( T. -> ( ( coe1 ` F ) ` 1 ) = ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 1 ) )
197 1nn0 
 |-  1 e. NN0
198 197 a1i 
 |-  ( T. -> 1 e. NN0 )
199 4 39 2 132 coe1subfv 
 |-  ( ( ( Q e. Ring /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( K ` 2 ) e. ( Base ` P ) ) /\ 1 e. NN0 ) -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 1 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 1 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 1 ) ) )
200 47 56 67 198 199 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 1 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 1 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 1 ) ) )
201 1re 
 |-  1 e. RR
202 1lt3 
 |-  1 < 3
203 201 202 ltneii 
 |-  1 =/= 3
204 neeq1 
 |-  ( i = 1 -> ( i =/= 3 <-> 1 =/= 3 ) )
205 203 204 mpbiri 
 |-  ( i = 1 -> i =/= 3 )
206 205 neneqd 
 |-  ( i = 1 -> -. i = 3 )
207 206 adantl 
 |-  ( ( T. /\ i = 1 ) -> -. i = 3 )
208 207 iffalsed 
 |-  ( ( T. /\ i = 1 ) -> if ( i = 3 , 1 , 0 ) = 0 )
209 147 208 198 157 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 1 ) = 0 )
210 ax-1ne0 
 |-  1 =/= 0
211 neeq1 
 |-  ( i = 1 -> ( i =/= 0 <-> 1 =/= 0 ) )
212 210 211 mpbiri 
 |-  ( i = 1 -> i =/= 0 )
213 212 neneqd 
 |-  ( i = 1 -> -. i = 0 )
214 213 adantl 
 |-  ( ( T. /\ i = 1 ) -> -. i = 0 )
215 214 iffalsed 
 |-  ( ( T. /\ i = 1 ) -> if ( i = 0 , 2 , 0 ) = 0 )
216 155 215 198 157 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( K ` 2 ) ) ` 1 ) = 0 )
217 209 216 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 1 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 1 ) ) = ( 0 ( -g ` Q ) 0 ) )
218 200 217 eqtrd 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 1 ) = ( 0 ( -g ` Q ) 0 ) )
219 196 218 193 3eqtrrd 
 |-  ( T. -> 0 = ( ( coe1 ` F ) ` 1 ) )
220 219 mptru 
 |-  0 = ( ( coe1 ` F ) ` 1 )
221 115 fveq1d 
 |-  ( T. -> ( ( coe1 ` F ) ` 0 ) = ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 0 ) )
222 4 39 2 132 coe1subfv 
 |-  ( ( ( Q e. Ring /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( K ` 2 ) e. ( Base ` P ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 0 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 0 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 0 ) ) )
223 47 56 67 157 222 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 0 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 0 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 0 ) ) )
224 28 necomi 
 |-  0 =/= 3
225 neeq1 
 |-  ( i = 0 -> ( i =/= 3 <-> 0 =/= 3 ) )
226 224 225 mpbiri 
 |-  ( i = 0 -> i =/= 3 )
227 226 neneqd 
 |-  ( i = 0 -> -. i = 3 )
228 227 adantl 
 |-  ( ( T. /\ i = 0 ) -> -. i = 3 )
229 228 iffalsed 
 |-  ( ( T. /\ i = 0 ) -> if ( i = 3 , 1 , 0 ) = 0 )
230 147 229 157 157 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 0 ) = 0 )
231 simpr 
 |-  ( ( T. /\ i = 0 ) -> i = 0 )
232 231 iftrued 
 |-  ( ( T. /\ i = 0 ) -> if ( i = 0 , 2 , 0 ) = 2 )
233 155 232 157 169 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( K ` 2 ) ) ` 0 ) = 2 )
234 230 233 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 0 ) ( -g ` Q ) ( ( coe1 ` ( K ` 2 ) ) ` 0 ) ) = ( 0 ( -g ` Q ) 2 ) )
235 223 234 eqtrd 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .- ( K ` 2 ) ) ) ` 0 ) = ( 0 ( -g ` Q ) 2 ) )
236 df-neg 
 |-  -u 2 = ( 0 - 2 )
237 40 1 132 subgsub 
 |-  ( ( QQ e. ( SubGrp ` CCfld ) /\ 0 e. QQ /\ 2 e. QQ ) -> ( 0 - 2 ) = ( 0 ( -g ` Q ) 2 ) )
238 136 189 66 237 syl3anc 
 |-  ( T. -> ( 0 - 2 ) = ( 0 ( -g ` Q ) 2 ) )
239 236 238 eqtr2id 
 |-  ( T. -> ( 0 ( -g ` Q ) 2 ) = -u 2 )
240 221 235 239 3eqtrrd 
 |-  ( T. -> -u 2 = ( ( coe1 ` F ) ` 0 ) )
241 240 mptru 
 |-  -u 2 = ( ( coe1 ` F ) ` 0 )
242 95 a1i 
 |-  ( x e. QQ -> Q e. Field )
243 242 fldcrngd 
 |-  ( x e. QQ -> Q e. CRing )
244 100 mptru 
 |-  F e. ( Base ` P )
245 244 a1i 
 |-  ( x e. QQ -> F e. ( Base ` P ) )
246 130 mptru 
 |-  ( D ` F ) = 3
247 246 a1i 
 |-  ( x e. QQ -> ( D ` F ) = 3 )
248 id 
 |-  ( x e. QQ -> x e. QQ )
249 4 92 62 39 108 111 112 113 7 166 195 220 241 243 245 247 248 evl1deg3 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) = ( ( ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) + ( 0 x. ( 2 ( .g ` ( mulGrp ` Q ) ) x ) ) ) + ( ( 0 x. x ) + -u 2 ) ) )
250 qsscn 
 |-  QQ C_ CC
251 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s QQ ) = ( ( mulGrp ` CCfld ) |`s QQ )
252 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
253 252 14 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
254 251 253 ressbas2 
 |-  ( QQ C_ CC -> QQ = ( Base ` ( ( mulGrp ` CCfld ) |`s QQ ) ) )
255 250 254 ax-mp 
 |-  QQ = ( Base ` ( ( mulGrp ` CCfld ) |`s QQ ) )
256 1 252 mgpress 
 |-  ( ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) ) -> ( ( mulGrp ` CCfld ) |`s QQ ) = ( mulGrp ` Q ) )
257 15 21 256 mp2an 
 |-  ( ( mulGrp ` CCfld ) |`s QQ ) = ( mulGrp ` Q )
258 257 fveq2i 
 |-  ( Base ` ( ( mulGrp ` CCfld ) |`s QQ ) ) = ( Base ` ( mulGrp ` Q ) )
259 255 258 eqtri 
 |-  QQ = ( Base ` ( mulGrp ` Q ) )
260 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
261 260 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
262 57 261 mp1i 
 |-  ( x e. QQ -> ( mulGrp ` Q ) e. Mnd )
263 52 a1i 
 |-  ( x e. QQ -> 3 e. NN0 )
264 259 112 262 263 248 mulgnn0cld 
 |-  ( x e. QQ -> ( 3 ( .g ` ( mulGrp ` Q ) ) x ) e. QQ )
265 250 264 sselid 
 |-  ( x e. QQ -> ( 3 ( .g ` ( mulGrp ` Q ) ) x ) e. CC )
266 265 mullidd 
 |-  ( x e. QQ -> ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) = ( 3 ( .g ` ( mulGrp ` Q ) ) x ) )
267 257 eqcomi 
 |-  ( mulGrp ` Q ) = ( ( mulGrp ` CCfld ) |`s QQ )
268 250 253 sseqtri 
 |-  QQ C_ ( Base ` ( mulGrp ` CCfld ) )
269 268 a1i 
 |-  ( x e. QQ -> QQ C_ ( Base ` ( mulGrp ` CCfld ) ) )
270 81 a1i 
 |-  ( x e. QQ -> 3 e. NN )
271 267 269 248 270 ressmulgnnd 
 |-  ( x e. QQ -> ( 3 ( .g ` ( mulGrp ` Q ) ) x ) = ( 3 ( .g ` ( mulGrp ` CCfld ) ) x ) )
272 qcn 
 |-  ( x e. QQ -> x e. CC )
273 cnfldexp 
 |-  ( ( x e. CC /\ 3 e. NN0 ) -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) x ) = ( x ^ 3 ) )
274 272 263 273 syl2anc 
 |-  ( x e. QQ -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) x ) = ( x ^ 3 ) )
275 266 271 274 3eqtrd 
 |-  ( x e. QQ -> ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) = ( x ^ 3 ) )
276 168 a1i 
 |-  ( x e. QQ -> 2 e. NN0 )
277 259 112 262 276 248 mulgnn0cld 
 |-  ( x e. QQ -> ( 2 ( .g ` ( mulGrp ` Q ) ) x ) e. QQ )
278 250 277 sselid 
 |-  ( x e. QQ -> ( 2 ( .g ` ( mulGrp ` Q ) ) x ) e. CC )
279 278 mul02d 
 |-  ( x e. QQ -> ( 0 x. ( 2 ( .g ` ( mulGrp ` Q ) ) x ) ) = 0 )
280 275 279 oveq12d 
 |-  ( x e. QQ -> ( ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) + ( 0 x. ( 2 ( .g ` ( mulGrp ` Q ) ) x ) ) ) = ( ( x ^ 3 ) + 0 ) )
281 272 263 expcld 
 |-  ( x e. QQ -> ( x ^ 3 ) e. CC )
282 281 addridd 
 |-  ( x e. QQ -> ( ( x ^ 3 ) + 0 ) = ( x ^ 3 ) )
283 280 282 eqtrd 
 |-  ( x e. QQ -> ( ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) + ( 0 x. ( 2 ( .g ` ( mulGrp ` Q ) ) x ) ) ) = ( x ^ 3 ) )
284 272 mul02d 
 |-  ( x e. QQ -> ( 0 x. x ) = 0 )
285 284 oveq1d 
 |-  ( x e. QQ -> ( ( 0 x. x ) + -u 2 ) = ( 0 + -u 2 ) )
286 26 a1i 
 |-  ( x e. QQ -> 2 e. CC )
287 286 negcld 
 |-  ( x e. QQ -> -u 2 e. CC )
288 287 addlidd 
 |-  ( x e. QQ -> ( 0 + -u 2 ) = -u 2 )
289 285 288 eqtrd 
 |-  ( x e. QQ -> ( ( 0 x. x ) + -u 2 ) = -u 2 )
290 283 289 oveq12d 
 |-  ( x e. QQ -> ( ( ( 1 x. ( 3 ( .g ` ( mulGrp ` Q ) ) x ) ) + ( 0 x. ( 2 ( .g ` ( mulGrp ` Q ) ) x ) ) ) + ( ( 0 x. x ) + -u 2 ) ) = ( ( x ^ 3 ) + -u 2 ) )
291 281 286 negsubd 
 |-  ( x e. QQ -> ( ( x ^ 3 ) + -u 2 ) = ( ( x ^ 3 ) - 2 ) )
292 249 290 291 3eqtrd 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) = ( ( x ^ 3 ) - 2 ) )
293 2prm 
 |-  2 e. Prime
294 3z 
 |-  3 e. ZZ
295 3re 
 |-  3 e. RR
296 172 295 173 ltleii 
 |-  2 <_ 3
297 64 eluz1i 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 3 e. ZZ /\ 2 <_ 3 ) )
298 294 296 297 mpbir2an 
 |-  3 e. ( ZZ>= ` 2 )
299 rtprmirr 
 |-  ( ( 2 e. Prime /\ 3 e. ( ZZ>= ` 2 ) ) -> ( 2 ^c ( 1 / 3 ) ) e. ( RR \ QQ ) )
300 293 298 299 mp2an 
 |-  ( 2 ^c ( 1 / 3 ) ) e. ( RR \ QQ )
301 eldifn 
 |-  ( ( 2 ^c ( 1 / 3 ) ) e. ( RR \ QQ ) -> -. ( 2 ^c ( 1 / 3 ) ) e. QQ )
302 300 301 ax-mp 
 |-  -. ( 2 ^c ( 1 / 3 ) ) e. QQ
303 nelne2 
 |-  ( ( x e. QQ /\ -. ( 2 ^c ( 1 / 3 ) ) e. QQ ) -> x =/= ( 2 ^c ( 1 / 3 ) ) )
304 302 303 mpan2 
 |-  ( x e. QQ -> x =/= ( 2 ^c ( 1 / 3 ) ) )
305 qre 
 |-  ( x e. QQ -> x e. RR )
306 305 adantr 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> x e. RR )
307 2pos 
 |-  0 < 2
308 281 286 subeq0ad 
 |-  ( x e. QQ -> ( ( ( x ^ 3 ) - 2 ) = 0 <-> ( x ^ 3 ) = 2 ) )
309 308 biimpa 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( x ^ 3 ) = 2 )
310 307 309 breqtrrid 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> 0 < ( x ^ 3 ) )
311 81 a1i 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> 3 e. NN )
312 n2dvds3 
 |-  -. 2 || 3
313 312 a1i 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> -. 2 || 3 )
314 306 311 313 expgt0b 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( 0 < x <-> 0 < ( x ^ 3 ) ) )
315 310 314 mpbird 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> 0 < x )
316 306 315 elrpd 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> x e. RR+ )
317 295 a1i 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> 3 e. RR )
318 29 a1i 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( 1 / 3 ) e. CC )
319 316 317 318 cxpmuld 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( x ^c ( 3 x. ( 1 / 3 ) ) ) = ( ( x ^c 3 ) ^c ( 1 / 3 ) ) )
320 27 a1i 
 |-  ( x e. QQ -> 3 e. CC )
321 28 a1i 
 |-  ( x e. QQ -> 3 =/= 0 )
322 320 321 recidd 
 |-  ( x e. QQ -> ( 3 x. ( 1 / 3 ) ) = 1 )
323 322 oveq2d 
 |-  ( x e. QQ -> ( x ^c ( 3 x. ( 1 / 3 ) ) ) = ( x ^c 1 ) )
324 272 cxp1d 
 |-  ( x e. QQ -> ( x ^c 1 ) = x )
325 323 324 eqtrd 
 |-  ( x e. QQ -> ( x ^c ( 3 x. ( 1 / 3 ) ) ) = x )
326 325 adantr 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( x ^c ( 3 x. ( 1 / 3 ) ) ) = x )
327 cxpexp 
 |-  ( ( x e. CC /\ 3 e. NN0 ) -> ( x ^c 3 ) = ( x ^ 3 ) )
328 272 263 327 syl2anc 
 |-  ( x e. QQ -> ( x ^c 3 ) = ( x ^ 3 ) )
329 328 oveq1d 
 |-  ( x e. QQ -> ( ( x ^c 3 ) ^c ( 1 / 3 ) ) = ( ( x ^ 3 ) ^c ( 1 / 3 ) ) )
330 329 adantr 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( ( x ^c 3 ) ^c ( 1 / 3 ) ) = ( ( x ^ 3 ) ^c ( 1 / 3 ) ) )
331 319 326 330 3eqtr3rd 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( ( x ^ 3 ) ^c ( 1 / 3 ) ) = x )
332 309 oveq1d 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> ( ( x ^ 3 ) ^c ( 1 / 3 ) ) = ( 2 ^c ( 1 / 3 ) ) )
333 331 332 eqtr3d 
 |-  ( ( x e. QQ /\ ( ( x ^ 3 ) - 2 ) = 0 ) -> x = ( 2 ^c ( 1 / 3 ) ) )
334 304 333 mteqand 
 |-  ( x e. QQ -> ( ( x ^ 3 ) - 2 ) =/= 0 )
335 292 334 eqnetrd 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) =/= 0 )
336 335 neneqd 
 |-  ( x e. QQ -> -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
337 336 rgen 
 |-  A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0
338 337 a1i 
 |-  ( T. -> A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
339 rabeq0 
 |-  ( { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } = (/) <-> A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
340 338 339 sylibr 
 |-  ( T. -> { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } = (/) )
341 105 340 eqtrd 
 |-  ( T. -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = (/) )
342 91 92 7 4 39 96 100 341 130 ply1dg3rt0irred 
 |-  ( T. -> F e. ( Irred ` P ) )
343 eqid 
 |-  ( Irred ` P ) = ( Irred ` P )
344 343 35 irredn0 
 |-  ( ( P e. Ring /\ F e. ( Irred ` P ) ) -> F =/= ( 0g ` P ) )
345 49 342 344 syl2anc 
 |-  ( T. -> F =/= ( 0g ` P ) )
346 1 fveq2i 
 |-  ( deg1 ` Q ) = ( deg1 ` ( CCfld |`s QQ ) )
347 7 346 eqtri 
 |-  D = ( deg1 ` ( CCfld |`s QQ ) )
348 eqid 
 |-  ( Monic1p ` ( CCfld |`s QQ ) ) = ( Monic1p ` ( CCfld |`s QQ ) )
349 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
350 349 qrng1 
 |-  1 = ( 1r ` ( CCfld |`s QQ ) )
351 13 39 35 347 348 350 ismon1p 
 |-  ( F e. ( Monic1p ` ( CCfld |`s QQ ) ) <-> ( F e. ( Base ` P ) /\ F =/= ( 0g ` P ) /\ ( ( coe1 ` F ) ` ( D ` F ) ) = 1 ) )
352 100 345 163 351 syl3anbrc 
 |-  ( T. -> F e. ( Monic1p ` ( CCfld |`s QQ ) ) )
353 11 13 14 19 25 33 34 10 35 90 342 352 irredminply 
 |-  ( T. -> F = ( M ` A ) )
354 353 130 jca 
 |-  ( T. -> ( F = ( M ` A ) /\ ( D ` F ) = 3 ) )
355 354 mptru 
 |-  ( F = ( M ` A ) /\ ( D ` F ) = 3 )