Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2sqr3minply Structured version   Visualization version   GIF version

Theorem 2sqr3minply 33752
Description: The polynomial ((𝑋↑3) − 2) is the minimal polynomial for (2↑𝑐(1 / 3)) over , and its degree is 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)
Hypotheses
Ref Expression
2sqr3minply.q 𝑄 = (ℂflds ℚ)
2sqr3minply.1 = (-g𝑃)
2sqr3minply.2 = (.g‘(mulGrp‘𝑃))
2sqr3minply.p 𝑃 = (Poly1𝑄)
2sqr3minply.k 𝐾 = (algSc‘𝑃)
2sqr3minply.x 𝑋 = (var1𝑄)
2sqr3minply.d 𝐷 = (deg1𝑄)
2sqr3minply.f 𝐹 = ((3 𝑋) (𝐾‘2))
2sqr3minply.a 𝐴 = (2↑𝑐(1 / 3))
2sqr3minply.m 𝑀 = (ℂfld minPoly ℚ)
Assertion
Ref Expression
2sqr3minply (𝐹 = (𝑀𝐴) ∧ (𝐷𝐹) = 3)

Proof of Theorem 2sqr3minply
Dummy variables 𝑖 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2734 . . . 4 (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2 2sqr3minply.p . . . . 5 𝑃 = (Poly1𝑄)
3 2sqr3minply.q . . . . . 6 𝑄 = (ℂflds ℚ)
43fveq2i 6909 . . . . 5 (Poly1𝑄) = (Poly1‘(ℂflds ℚ))
52, 4eqtri 2762 . . . 4 𝑃 = (Poly1‘(ℂflds ℚ))
6 cnfldbas 21385 . . . 4 ℂ = (Base‘ℂfld)
7 cndrng 21428 . . . . . 6 fld ∈ DivRing
8 cncrng 21418 . . . . . 6 fld ∈ CRing
9 isfld 20756 . . . . . 6 (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
107, 8, 9mpbir2an 711 . . . . 5 fld ∈ Field
1110a1i 11 . . . 4 (⊤ → ℂfld ∈ Field)
12 qsubdrg 21454 . . . . . . 7 (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂflds ℚ) ∈ DivRing)
1312simpli 483 . . . . . 6 ℚ ∈ (SubRing‘ℂfld)
1412simpri 485 . . . . . 6 (ℂflds ℚ) ∈ DivRing
15 issdrg 20805 . . . . . 6 (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂflds ℚ) ∈ DivRing))
167, 13, 14, 15mpbir3an 1340 . . . . 5 ℚ ∈ (SubDRing‘ℂfld)
1716a1i 11 . . . 4 (⊤ → ℚ ∈ (SubDRing‘ℂfld))
18 2sqr3minply.a . . . . . 6 𝐴 = (2↑𝑐(1 / 3))
19 2cn 12338 . . . . . . 7 2 ∈ ℂ
20 3cn 12344 . . . . . . . 8 3 ∈ ℂ
21 3ne0 12369 . . . . . . . 8 3 ≠ 0
2220, 21reccli 11994 . . . . . . 7 (1 / 3) ∈ ℂ
23 cxpcl 26730 . . . . . . 7 ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
2419, 22, 23mp2an 692 . . . . . 6 (2↑𝑐(1 / 3)) ∈ ℂ
2518, 24eqeltri 2834 . . . . 5 𝐴 ∈ ℂ
2625a1i 11 . . . 4 (⊤ → 𝐴 ∈ ℂ)
27 cnfld0 21422 . . . 4 0 = (0g‘ℂfld)
28 2sqr3minply.m . . . 4 𝑀 = (ℂfld minPoly ℚ)
29 eqid 2734 . . . 4 (0g𝑃) = (0g𝑃)
30 2sqr3minply.f . . . . . . . 8 𝐹 = ((3 𝑋) (𝐾‘2))
3130fveq2i 6909 . . . . . . 7 ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 𝑋) (𝐾‘2)))
3231fveq1i 6907 . . . . . 6 (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 𝑋) (𝐾‘2)))‘𝐴)
3332a1i 11 . . . . 5 (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 𝑋) (𝐾‘2)))‘𝐴))
34 eqid 2734 . . . . . 6 (Base‘𝑃) = (Base‘𝑃)
35 2sqr3minply.1 . . . . . 6 = (-g𝑃)
36 cnfldsub 21427 . . . . . 6 − = (-g‘ℂfld)
378a1i 11 . . . . . 6 (⊤ → ℂfld ∈ CRing)
3813a1i 11 . . . . . 6 (⊤ → ℚ ∈ (SubRing‘ℂfld))
39 eqid 2734 . . . . . . . 8 (mulGrp‘𝑃) = (mulGrp‘𝑃)
4039, 34mgpbas 20157 . . . . . . 7 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41 2sqr3minply.2 . . . . . . 7 = (.g‘(mulGrp‘𝑃))
423qdrng 27678 . . . . . . . . . . 11 𝑄 ∈ DivRing
4342a1i 11 . . . . . . . . . 10 (⊤ → 𝑄 ∈ DivRing)
4443drngringd 20753 . . . . . . . . 9 (⊤ → 𝑄 ∈ Ring)
452ply1ring 22264 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑃 ∈ Ring)
4644, 45syl 17 . . . . . . . 8 (⊤ → 𝑃 ∈ Ring)
4739ringmgp 20256 . . . . . . . 8 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
4846, 47syl 17 . . . . . . 7 (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49 3nn0 12541 . . . . . . . 8 3 ∈ ℕ0
5049a1i 11 . . . . . . 7 (⊤ → 3 ∈ ℕ0)
51 2sqr3minply.x . . . . . . . . 9 𝑋 = (var1𝑄)
5251, 2, 34vr1cl 22234 . . . . . . . 8 (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
5344, 52syl 17 . . . . . . 7 (⊤ → 𝑋 ∈ (Base‘𝑃))
5440, 41, 48, 50, 53mulgnn0cld 19125 . . . . . 6 (⊤ → (3 𝑋) ∈ (Base‘𝑃))
55 2sqr3minply.k . . . . . . . 8 𝐾 = (algSc‘𝑃)
5644mptru 1543 . . . . . . . . 9 𝑄 ∈ Ring
572ply1sca 22269 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
5856, 57ax-mp 5 . . . . . . . 8 𝑄 = (Scalar‘𝑃)
592ply1lmod 22268 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑃 ∈ LMod)
6044, 59syl 17 . . . . . . . 8 (⊤ → 𝑃 ∈ LMod)
613qrngbas 27677 . . . . . . . 8 ℚ = (Base‘𝑄)
6255, 58, 46, 60, 61, 34asclf 21919 . . . . . . 7 (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63 2z 12646 . . . . . . . 8 2 ∈ ℤ
64 zq 12993 . . . . . . . 8 (2 ∈ ℤ → 2 ∈ ℚ)
6563, 64mp1i 13 . . . . . . 7 (⊤ → 2 ∈ ℚ)
6662, 65ffvelcdmd 7104 . . . . . 6 (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
671, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26evls1subd 33576 . . . . 5 (⊤ → (((ℂfld evalSub1 ℚ)‘((3 𝑋) (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68 eqid 2734 . . . . . . . . . 10 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
691, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26evls1expd 22386 . . . . . . . . 9 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
701, 51, 3, 6, 37, 38evls1var 22357 . . . . . . . . . . . 12 (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
7170fveq1d 6908 . . . . . . . . . . 11 (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72 fvresi 7192 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
7325, 72mp1i 13 . . . . . . . . . . 11 (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
7471, 73eqtrd 2774 . . . . . . . . . 10 (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
7574oveq2d 7446 . . . . . . . . 9 (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76 cnfldexp 21434 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
7726, 50, 76syl2anc 584 . . . . . . . . 9 (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
7869, 75, 773eqtrd 2778 . . . . . . . 8 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = (𝐴↑3))
7918oveq1i 7440 . . . . . . . . 9 (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80 3nn 12342 . . . . . . . . . 10 3 ∈ ℕ
81 cxproot 26746 . . . . . . . . . 10 ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
8219, 80, 81mp2an 692 . . . . . . . . 9 ((2↑𝑐(1 / 3))↑3) = 2
8379, 82eqtri 2762 . . . . . . . 8 (𝐴↑3) = 2
8478, 83eqtrdi 2790 . . . . . . 7 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = 2)
851, 2, 3, 6, 55, 37, 38, 65, 26evls1scafv 22385 . . . . . . 7 (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
8684, 85oveq12d 7448 . . . . . 6 (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
8719subidi 11577 . . . . . 6 (2 − 2) = 0
8886, 87eqtrdi 2790 . . . . 5 (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
8933, 67, 883eqtrd 2778 . . . 4 (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
903qrng0 27679 . . . . 5 0 = (0g𝑄)
91 eqid 2734 . . . . 5 (eval1𝑄) = (eval1𝑄)
92 2sqr3minply.d . . . . 5 𝐷 = (deg1𝑄)
93 fldsdrgfld 20815 . . . . . . . 8 ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂflds ℚ) ∈ Field)
9410, 16, 93mp2an 692 . . . . . . 7 (ℂflds ℚ) ∈ Field
953, 94eqeltri 2834 . . . . . 6 𝑄 ∈ Field
9695a1i 11 . . . . 5 (⊤ → 𝑄 ∈ Field)
9746ringgrpd 20259 . . . . . . 7 (⊤ → 𝑃 ∈ Grp)
9834, 35grpsubcl 19050 . . . . . . 7 ((𝑃 ∈ Grp ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 𝑋) (𝐾‘2)) ∈ (Base‘𝑃))
9997, 54, 66, 98syl3anc 1370 . . . . . 6 (⊤ → ((3 𝑋) (𝐾‘2)) ∈ (Base‘𝑃))
10030, 99eqeltrid 2842 . . . . 5 (⊤ → 𝐹 ∈ (Base‘𝑃))
10196fldcrngd 20758 . . . . . . . . 9 (⊤ → 𝑄 ∈ CRing)
10291, 2, 34, 101, 61, 100evl1fvf 33568 . . . . . . . 8 (⊤ → ((eval1𝑄)‘𝐹):ℚ⟶ℚ)
103102ffnd 6737 . . . . . . 7 (⊤ → ((eval1𝑄)‘𝐹) Fn ℚ)
104 fniniseg2 7081 . . . . . . 7 (((eval1𝑄)‘𝐹) Fn ℚ → (((eval1𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0})
105103, 104syl 17 . . . . . 6 (⊤ → (((eval1𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0})
106 cnfldmul 21389 . . . . . . . . . . . . . . 15 · = (.r‘ℂfld)
1073, 106ressmulr 17352 . . . . . . . . . . . . . 14 (ℚ ∈ (SubRing‘ℂfld) → · = (.r𝑄))
10813, 107ax-mp 5 . . . . . . . . . . . . 13 · = (.r𝑄)
109 cnfldadd 21387 . . . . . . . . . . . . . . 15 + = (+g‘ℂfld)
1103, 109ressplusg 17335 . . . . . . . . . . . . . 14 (ℚ ∈ (SubRing‘ℂfld) → + = (+g𝑄))
11113, 110ax-mp 5 . . . . . . . . . . . . 13 + = (+g𝑄)
112 eqid 2734 . . . . . . . . . . . . 13 (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113 eqid 2734 . . . . . . . . . . . . 13 (coe1𝐹) = (coe1𝐹)
11430fveq2i 6909 . . . . . . . . . . . . . . . . . 18 (coe1𝐹) = (coe1‘((3 𝑋) (𝐾‘2)))
115114a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (coe1𝐹) = (coe1‘((3 𝑋) (𝐾‘2))))
11630fveq2i 6909 . . . . . . . . . . . . . . . . . . 19 (𝐷𝐹) = (𝐷‘((3 𝑋) (𝐾‘2)))
117116a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → (𝐷𝐹) = (𝐷‘((3 𝑋) (𝐾‘2))))
118 3pos 12368 . . . . . . . . . . . . . . . . . . . . 21 0 < 3
119118a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 0 < 3)
120 2ne0 12367 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
121120a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → 2 ≠ 0)
12292, 2, 61, 55, 90deg1scl 26166 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
12344, 65, 121, 122syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝐷‘(𝐾‘2)) = 0)
124 drngnzr 20764 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
12542, 124mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → 𝑄 ∈ NzRing)
12692, 2, 51, 39, 41deg1pw 26174 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 𝑋)) = 3)
127125, 50, 126syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝐷‘(3 𝑋)) = 3)
128119, 123, 1273brtr4d 5179 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 𝑋)))
1292, 92, 44, 34, 35, 54, 66, 128deg1sub 26161 . . . . . . . . . . . . . . . . . 18 (⊤ → (𝐷‘((3 𝑋) (𝐾‘2))) = (𝐷‘(3 𝑋)))
130117, 129, 1273eqtrd 2778 . . . . . . . . . . . . . . . . 17 (⊤ → (𝐷𝐹) = 3)
131115, 130fveq12d 6913 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = ((coe1‘((3 𝑋) (𝐾‘2)))‘3))
132 eqid 2734 . . . . . . . . . . . . . . . . . 18 (-g𝑄) = (-g𝑄)
1332, 34, 35, 132coe1subfv 22284 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 3 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘3) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
13444, 54, 66, 50, 133syl31anc 1372 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘3) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
135 subrgsubg 20593 . . . . . . . . . . . . . . . . . . 19 (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
13613, 135mp1i 13 . . . . . . . . . . . . . . . . . 18 (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (coe1‘(3 𝑋)) = (coe1‘(3 𝑋))
138137, 34, 2, 61coe1fvalcl 22229 . . . . . . . . . . . . . . . . . . 19 (((3 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 𝑋))‘3) ∈ ℚ)
13954, 50, 138syl2anc 584 . . . . . . . . . . . . . . . . . 18 (⊤ → ((coe1‘(3 𝑋))‘3) ∈ ℚ)
140 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141140, 34, 2, 61coe1fvalcl 22229 . . . . . . . . . . . . . . . . . . 19 (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
14266, 50, 141syl2anc 584 . . . . . . . . . . . . . . . . . 18 (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
14336, 3, 132subgsub 19168 . . . . . . . . . . . . . . . . . 18 ((ℚ ∈ (SubGrp‘ℂfld) ∧ ((coe1‘(3 𝑋))‘3) ∈ ℚ ∧ ((coe1‘(𝐾‘2))‘3) ∈ ℚ) → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
144136, 139, 142, 143syl3anc 1370 . . . . . . . . . . . . . . . . 17 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
145 iftrue 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
1463qrng1 27680 . . . . . . . . . . . . . . . . . . . . 21 1 = (1r𝑄)
1472, 51, 41, 44, 50, 90, 146coe1mon 33589 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (coe1‘(3 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148 1cnd 11253 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 1 ∈ ℂ)
149145, 147, 50, 148fvmptd4 7039 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((coe1‘(3 𝑋))‘3) = 1)
15021neii 2939 . . . . . . . . . . . . . . . . . . . . . 22 ¬ 3 = 0
151 eqeq1 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152150, 151mtbiri 327 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 3 → ¬ 𝑖 = 0)
153152iffalsed 4541 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
1542, 55, 61, 90coe1scl 22305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
15544, 65, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156 0nn0 12538 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℕ0
157156a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 0 ∈ ℕ0)
158153, 155, 50, 157fvmptd4 7039 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159149, 158oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160 1m0e1 12384 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
161159, 160eqtrdi 2790 . . . . . . . . . . . . . . . . 17 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162144, 161eqtr3d 2776 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163131, 134, 1623eqtrd 2778 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = 1)
164130fveq2d 6910 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = ((coe1𝐹)‘3))
165163, 164eqtr3d 2776 . . . . . . . . . . . . . 14 (⊤ → 1 = ((coe1𝐹)‘3))
166165mptru 1543 . . . . . . . . . . . . 13 1 = ((coe1𝐹)‘3)
167115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘2) = ((coe1‘((3 𝑋) (𝐾‘2)))‘2))
168 2nn0 12540 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
169168a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 2 ∈ ℕ0)
1702, 34, 35, 132coe1subfv 22284 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)))
17144, 54, 66, 169, 170syl31anc 1372 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)))
172 2re 12337 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
173 2lt3 12435 . . . . . . . . . . . . . . . . . . . . . . 23 2 < 3
174172, 173ltneii 11371 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 3
175 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176174, 175mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 2 → 𝑖 ≠ 3)
177176adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178177neneqd 2942 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179178iffalsed 4541 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180147, 179, 169, 157fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘2) = 0)
181 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182120, 181mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 2 → 𝑖 ≠ 0)
183182neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 2 → ¬ 𝑖 = 0)
184183adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185184iffalsed 4541 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186155, 185, 169, 157fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187180, 186oveq12d 7448 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g𝑄)0))
188171, 187eqtrd 2774 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (0(-g𝑄)0))
189158, 142eqeltrrd 2839 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ℚ)
19036, 3, 132subgsub 19168 . . . . . . . . . . . . . . . . 17 ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g𝑄)0))
191136, 189, 189, 190syl3anc 1370 . . . . . . . . . . . . . . . 16 (⊤ → (0 − 0) = (0(-g𝑄)0))
192 0m0e0 12383 . . . . . . . . . . . . . . . 16 (0 − 0) = 0
193191, 192eqtr3di 2789 . . . . . . . . . . . . . . 15 (⊤ → (0(-g𝑄)0) = 0)
194167, 188, 1933eqtrrd 2779 . . . . . . . . . . . . . 14 (⊤ → 0 = ((coe1𝐹)‘2))
195194mptru 1543 . . . . . . . . . . . . 13 0 = ((coe1𝐹)‘2)
196115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘1) = ((coe1‘((3 𝑋) (𝐾‘2)))‘1))
197 1nn0 12539 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
198197a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℕ0)
1992, 34, 35, 132coe1subfv 22284 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)))
20044, 54, 66, 198, 199syl31anc 1372 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)))
201 1re 11258 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
202 1lt3 12436 . . . . . . . . . . . . . . . . . . . . . . 23 1 < 3
203201, 202ltneii 11371 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 3
204 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205203, 204mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 1 → 𝑖 ≠ 3)
206205neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 1 → ¬ 𝑖 = 3)
207206adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208207iffalsed 4541 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209147, 208, 198, 157fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘1) = 0)
210 ax-1ne0 11221 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 0
211 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212210, 211mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 1 → 𝑖 ≠ 0)
213212neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 1 → ¬ 𝑖 = 0)
214213adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215214iffalsed 4541 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216155, 215, 198, 157fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217209, 216oveq12d 7448 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g𝑄)0))
218200, 217eqtrd 2774 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (0(-g𝑄)0))
219196, 218, 1933eqtrrd 2779 . . . . . . . . . . . . . 14 (⊤ → 0 = ((coe1𝐹)‘1))
220219mptru 1543 . . . . . . . . . . . . 13 0 = ((coe1𝐹)‘1)
221115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘0) = ((coe1‘((3 𝑋) (𝐾‘2)))‘0))
2222, 34, 35, 132coe1subfv 22284 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)))
22344, 54, 66, 157, 222syl31anc 1372 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)))
22421necomi 2992 . . . . . . . . . . . . . . . . . . . . . 22 0 ≠ 3
225 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226224, 225mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → 𝑖 ≠ 3)
227226neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ¬ 𝑖 = 3)
228227adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229228iffalsed 4541 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230147, 229, 157, 157fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘0) = 0)
231 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232231iftrued 4538 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233155, 232, 157, 169fvmptd 7022 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234230, 233oveq12d 7448 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g𝑄)2))
235223, 234eqtrd 2774 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (0(-g𝑄)2))
236 df-neg 11492 . . . . . . . . . . . . . . . 16 -2 = (0 − 2)
23736, 3, 132subgsub 19168 . . . . . . . . . . . . . . . . 17 ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g𝑄)2))
238136, 189, 65, 237syl3anc 1370 . . . . . . . . . . . . . . . 16 (⊤ → (0 − 2) = (0(-g𝑄)2))
239236, 238eqtr2id 2787 . . . . . . . . . . . . . . 15 (⊤ → (0(-g𝑄)2) = -2)
240221, 235, 2393eqtrrd 2779 . . . . . . . . . . . . . 14 (⊤ → -2 = ((coe1𝐹)‘0))
241240mptru 1543 . . . . . . . . . . . . 13 -2 = ((coe1𝐹)‘0)
24295a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243242fldcrngd 20758 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → 𝑄 ∈ CRing)
244100mptru 1543 . . . . . . . . . . . . . 14 𝐹 ∈ (Base‘𝑃)
245244a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃))
246130mptru 1543 . . . . . . . . . . . . . 14 (𝐷𝐹) = 3
247246a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → (𝐷𝐹) = 3)
248 id 22 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → 𝑥 ∈ ℚ)
2492, 91, 61, 34, 108, 111, 112, 113, 92, 166, 195, 220, 241, 243, 245, 247, 248evl1deg3 33582 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250 qsscn 12999 . . . . . . . . . . . . . . . . . 18 ℚ ⊆ ℂ
251 eqid 2734 . . . . . . . . . . . . . . . . . . . . . 22 ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . 23 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253252, 6mgpbas 20157 . . . . . . . . . . . . . . . . . . . . . 22 ℂ = (Base‘(mulGrp‘ℂfld))
254251, 253ressbas2 17282 . . . . . . . . . . . . . . . . . . . . 21 (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255250, 254ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
2563, 252mgpress 20166 . . . . . . . . . . . . . . . . . . . . . 22 ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
2577, 13, 256mp2an 692 . . . . . . . . . . . . . . . . . . . . 21 ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258257fveq2i 6909 . . . . . . . . . . . . . . . . . . . 20 (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259255, 258eqtri 2762 . . . . . . . . . . . . . . . . . . 19 ℚ = (Base‘(mulGrp‘𝑄))
260 eqid 2734 . . . . . . . . . . . . . . . . . . . . 21 (mulGrp‘𝑄) = (mulGrp‘𝑄)
261260ringmgp 20256 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
26256, 261mp1i 13 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → (mulGrp‘𝑄) ∈ Mnd)
26349a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → 3 ∈ ℕ0)
264259, 112, 262, 263, 248mulgnn0cld 19125 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265250, 264sselid 3992 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266265mullidd 11276 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267257eqcomi 2743 . . . . . . . . . . . . . . . . 17 (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268250, 253sseqtri 4031 . . . . . . . . . . . . . . . . . 18 ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269268a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
27080a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 3 ∈ ℕ)
271267, 269, 248, 270ressmulgnnd 19108 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272 qcn 13002 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273 cnfldexp 21434 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274272, 263, 273syl2anc 584 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275266, 271, 2743eqtrd 2778 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276168a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277259, 112, 262, 276, 248mulgnn0cld 19125 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278250, 277sselid 3992 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279278mul02d 11456 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280275, 279oveq12d 7448 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281272, 263expcld 14182 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282281addridd 11458 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283280, 282eqtrd 2774 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284272mul02d 11456 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285284oveq1d 7445 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
28619a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → 2 ∈ ℂ)
287286negcld 11604 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → -2 ∈ ℂ)
288287addlidd 11459 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → (0 + -2) = -2)
289285, 288eqtrd 2774 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290283, 289oveq12d 7448 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291281, 286negsubd 11623 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292249, 290, 2913eqtrd 2778 . . . . . . . . . . 11 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293 2prm 16725 . . . . . . . . . . . . . . 15 2 ∈ ℙ
294 3z 12647 . . . . . . . . . . . . . . . 16 3 ∈ ℤ
295 3re 12343 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
296172, 295, 173ltleii 11381 . . . . . . . . . . . . . . . 16 2 ≤ 3
29763eluz1i 12883 . . . . . . . . . . . . . . . 16 (3 ∈ (ℤ‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298294, 296, 297mpbir2an 711 . . . . . . . . . . . . . . 15 3 ∈ (ℤ‘2)
299 rtprmirr 26817 . . . . . . . . . . . . . . 15 ((2 ∈ ℙ ∧ 3 ∈ (ℤ‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300293, 298, 299mp2an 692 . . . . . . . . . . . . . 14 (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301 eldifn 4141 . . . . . . . . . . . . . 14 ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302300, 301ax-mp 5 . . . . . . . . . . . . 13 ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303 nelne2 3037 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304302, 303mpan2 691 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305 qre 12992 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306305adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307 2pos 12366 . . . . . . . . . . . . . . . . . 18 0 < 2
308281, 286subeq0ad 11627 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309308biimpa 476 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310307, 309breqtrrid 5185 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
31180a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312 n2dvds3 16404 . . . . . . . . . . . . . . . . . . 19 ¬ 2 ∥ 3
313312a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314306, 311, 313expgt0b 32822 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315310, 314mpbird 257 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316306, 315elrpd 13071 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ+)
317295a1i 11 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℝ)
31822a1i 11 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (1 / 3) ∈ ℂ)
319316, 317, 318cxpmuld 26793 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥𝑐(3 · (1 / 3))) = ((𝑥𝑐3)↑𝑐(1 / 3)))
32020a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 3 ∈ ℂ)
32121a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 3 ≠ 0)
322320, 321recidd 12035 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323322oveq2d 7446 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐(3 · (1 / 3))) = (𝑥𝑐1))
324272cxp1d 26762 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐1) = 𝑥)
325323, 324eqtrd 2774 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (𝑥𝑐(3 · (1 / 3))) = 𝑥)
326325adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥𝑐(3 · (1 / 3))) = 𝑥)
327 cxpexp 26724 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥𝑐3) = (𝑥↑3))
328272, 263, 327syl2anc 584 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐3) = (𝑥↑3))
329328oveq1d 7445 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → ((𝑥𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330329adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331319, 326, 3303eqtr3rd 2783 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332309oveq1d 7445 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333331, 332eqtr3d 2776 . . . . . . . . . . . 12 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334304, 333mteqand 3030 . . . . . . . . . . 11 (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335292, 334eqnetrd 3005 . . . . . . . . . 10 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) ≠ 0)
336335neneqd 2942 . . . . . . . . 9 (𝑥 ∈ ℚ → ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
337336rgen 3060 . . . . . . . 8 𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0
338337a1i 11 . . . . . . 7 (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
339 rabeq0 4393 . . . . . . 7 ({𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
340338, 339sylibr 234 . . . . . 6 (⊤ → {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341105, 340eqtrd 2774 . . . . 5 (⊤ → (((eval1𝑄)‘𝐹) “ {0}) = ∅)
34290, 91, 92, 2, 34, 96, 100, 341, 130ply1dg3rt0irred 33586 . . . 4 (⊤ → 𝐹 ∈ (Irred‘𝑃))
343 eqid 2734 . . . . . . 7 (Irred‘𝑃) = (Irred‘𝑃)
344343, 29irredn0 20439 . . . . . 6 ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g𝑃))
34546, 342, 344syl2anc 584 . . . . 5 (⊤ → 𝐹 ≠ (0g𝑃))
3463fveq2i 6909 . . . . . . 7 (deg1𝑄) = (deg1‘(ℂflds ℚ))
34792, 346eqtri 2762 . . . . . 6 𝐷 = (deg1‘(ℂflds ℚ))
348 eqid 2734 . . . . . 6 (Monic1p‘(ℂflds ℚ)) = (Monic1p‘(ℂflds ℚ))
349 eqid 2734 . . . . . . 7 (ℂflds ℚ) = (ℂflds ℚ)
350349qrng1 27680 . . . . . 6 1 = (1r‘(ℂflds ℚ))
3515, 34, 29, 347, 348, 350ismon1p 26196 . . . . 5 (𝐹 ∈ (Monic1p‘(ℂflds ℚ)) ↔ (𝐹 ∈ (Base‘𝑃) ∧ 𝐹 ≠ (0g𝑃) ∧ ((coe1𝐹)‘(𝐷𝐹)) = 1))
352100, 345, 163, 351syl3anbrc 1342 . . . 4 (⊤ → 𝐹 ∈ (Monic1p‘(ℂflds ℚ)))
3531, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352irredminply 33721 . . 3 (⊤ → 𝐹 = (𝑀𝐴))
354353, 130jca 511 . 2 (⊤ → (𝐹 = (𝑀𝐴) ∧ (𝐷𝐹) = 3))
355354mptru 1543 1 (𝐹 = (𝑀𝐴) ∧ (𝐷𝐹) = 3)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1536  wtru 1537  wcel 2105  wne 2937  wral 3058  {crab 3432  cdif 3959  wss 3962  c0 4338  ifcif 4530  {csn 4630   class class class wbr 5147  cmpt 5230   I cid 5581  ccnv 5687  cres 5690  cima 5691   Fn wfn 6557  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489  -cneg 11490   / cdiv 11917  cn 12263  2c2 12318  3c3 12319  0cn0 12523  cz 12610  cuz 12875  cq 12987  cexp 14098  cdvds 16286  cprime 16704  Basecbs 17244  s cress 17273  +gcplusg 17297  .rcmulr 17298  Scalarcsca 17300  0gc0g 17485  Mndcmnd 18759  Grpcgrp 18963  -gcsg 18965  .gcmg 19097  SubGrpcsubg 19150  mulGrpcmgp 20151  Ringcrg 20250  CRingccrg 20251  Irredcir 20372  NzRingcnzr 20528  SubRingcsubrg 20585  DivRingcdr 20745  Fieldcfield 20746  SubDRingcsdrg 20803  LModclmod 20874  fldccnfld 21381  algSccascl 21889  var1cv1 22192  Poly1cpl1 22193  coe1cco1 22194   evalSub1 ces1 22332  eval1ce1 22333  deg1cdg1 26107  Monic1pcmn1 26179  𝑐ccxp 26611   minPoly cminply 33706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231  ax-mulf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-ofr 7697  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-dvds 16287  df-gcd 16528  df-prm 16705  df-numer 16768  df-denom 16769  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-pws 17495  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-mulg 19098  df-subg 19153  df-ghm 19243  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-srg 20204  df-ring 20252  df-cring 20253  df-oppr 20350  df-dvdsr 20373  df-unit 20374  df-irred 20375  df-invr 20404  df-dvr 20417  df-rhm 20488  df-nzr 20529  df-subrng 20562  df-subrg 20586  df-rlreg 20710  df-domn 20711  df-idom 20712  df-drng 20747  df-field 20748  df-sdrg 20804  df-lmod 20876  df-lss 20947  df-lsp 20987  df-sra 21189  df-rgmod 21190  df-lidl 21235  df-rsp 21236  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-assa 21890  df-asp 21891  df-ascl 21892  df-psr 21946  df-mvr 21947  df-mpl 21948  df-opsr 21950  df-evls 22115  df-evl 22116  df-psr1 22196  df-vr1 22197  df-ply1 22198  df-coe1 22199  df-evls1 22334  df-evl1 22335  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916  df-mdeg 26108  df-deg1 26109  df-mon1 26184  df-uc1p 26185  df-q1p 26186  df-r1p 26187  df-ig1p 26188  df-log 26612  df-cxp 26613  df-irng 33698  df-minply 33707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator