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 33791
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 2737 . . . 4 (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2 2sqr3minply.p . . . . 5 𝑃 = (Poly1𝑄)
3 2sqr3minply.q . . . . . 6 𝑄 = (ℂflds ℚ)
43fveq2i 6909 . . . . 5 (Poly1𝑄) = (Poly1‘(ℂflds ℚ))
52, 4eqtri 2765 . . . 4 𝑃 = (Poly1‘(ℂflds ℚ))
6 cnfldbas 21368 . . . 4 ℂ = (Base‘ℂfld)
7 cndrng 21411 . . . . . 6 fld ∈ DivRing
8 cncrng 21401 . . . . . 6 fld ∈ CRing
9 isfld 20740 . . . . . 6 (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
107, 8, 9mpbir2an 711 . . . . 5 fld ∈ Field
1110a1i 11 . . . 4 (⊤ → ℂfld ∈ Field)
12 qsubdrg 21437 . . . . . . 7 (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂflds ℚ) ∈ DivRing)
1312simpli 483 . . . . . 6 ℚ ∈ (SubRing‘ℂfld)
1412simpri 485 . . . . . 6 (ℂflds ℚ) ∈ DivRing
15 issdrg 20789 . . . . . 6 (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂflds ℚ) ∈ DivRing))
167, 13, 14, 15mpbir3an 1342 . . . . 5 ℚ ∈ (SubDRing‘ℂfld)
1716a1i 11 . . . 4 (⊤ → ℚ ∈ (SubDRing‘ℂfld))
18 2sqr3minply.a . . . . . 6 𝐴 = (2↑𝑐(1 / 3))
19 2cn 12341 . . . . . . 7 2 ∈ ℂ
20 3cn 12347 . . . . . . . 8 3 ∈ ℂ
21 3ne0 12372 . . . . . . . 8 3 ≠ 0
2220, 21reccli 11997 . . . . . . 7 (1 / 3) ∈ ℂ
23 cxpcl 26716 . . . . . . 7 ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
2419, 22, 23mp2an 692 . . . . . 6 (2↑𝑐(1 / 3)) ∈ ℂ
2518, 24eqeltri 2837 . . . . 5 𝐴 ∈ ℂ
2625a1i 11 . . . 4 (⊤ → 𝐴 ∈ ℂ)
27 cnfld0 21405 . . . 4 0 = (0g‘ℂfld)
28 2sqr3minply.m . . . 4 𝑀 = (ℂfld minPoly ℚ)
29 eqid 2737 . . . 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 2737 . . . . . 6 (Base‘𝑃) = (Base‘𝑃)
35 2sqr3minply.1 . . . . . 6 = (-g𝑃)
36 cnfldsub 21410 . . . . . 6 − = (-g‘ℂfld)
378a1i 11 . . . . . 6 (⊤ → ℂfld ∈ CRing)
3813a1i 11 . . . . . 6 (⊤ → ℚ ∈ (SubRing‘ℂfld))
39 eqid 2737 . . . . . . . 8 (mulGrp‘𝑃) = (mulGrp‘𝑃)
4039, 34mgpbas 20142 . . . . . . 7 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41 2sqr3minply.2 . . . . . . 7 = (.g‘(mulGrp‘𝑃))
423qdrng 27664 . . . . . . . . . . 11 𝑄 ∈ DivRing
4342a1i 11 . . . . . . . . . 10 (⊤ → 𝑄 ∈ DivRing)
4443drngringd 20737 . . . . . . . . 9 (⊤ → 𝑄 ∈ Ring)
452ply1ring 22249 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑃 ∈ Ring)
4644, 45syl 17 . . . . . . . 8 (⊤ → 𝑃 ∈ Ring)
4739ringmgp 20236 . . . . . . . 8 (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
4846, 47syl 17 . . . . . . 7 (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49 3nn0 12544 . . . . . . . 8 3 ∈ ℕ0
5049a1i 11 . . . . . . 7 (⊤ → 3 ∈ ℕ0)
51 2sqr3minply.x . . . . . . . . 9 𝑋 = (var1𝑄)
5251, 2, 34vr1cl 22219 . . . . . . . 8 (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
5344, 52syl 17 . . . . . . 7 (⊤ → 𝑋 ∈ (Base‘𝑃))
5440, 41, 48, 50, 53mulgnn0cld 19113 . . . . . 6 (⊤ → (3 𝑋) ∈ (Base‘𝑃))
55 2sqr3minply.k . . . . . . . 8 𝐾 = (algSc‘𝑃)
5644mptru 1547 . . . . . . . . 9 𝑄 ∈ Ring
572ply1sca 22254 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
5856, 57ax-mp 5 . . . . . . . 8 𝑄 = (Scalar‘𝑃)
592ply1lmod 22253 . . . . . . . . 9 (𝑄 ∈ Ring → 𝑃 ∈ LMod)
6044, 59syl 17 . . . . . . . 8 (⊤ → 𝑃 ∈ LMod)
613qrngbas 27663 . . . . . . . 8 ℚ = (Base‘𝑄)
6255, 58, 46, 60, 61, 34asclf 21902 . . . . . . 7 (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63 2z 12649 . . . . . . . 8 2 ∈ ℤ
64 zq 12996 . . . . . . . 8 (2 ∈ ℤ → 2 ∈ ℚ)
6563, 64mp1i 13 . . . . . . 7 (⊤ → 2 ∈ ℚ)
6662, 65ffvelcdmd 7105 . . . . . 6 (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
671, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26evls1subd 33597 . . . . 5 (⊤ → (((ℂfld evalSub1 ℚ)‘((3 𝑋) (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68 eqid 2737 . . . . . . . . . 10 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
691, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26evls1expd 22371 . . . . . . . . 9 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
701, 51, 3, 6, 37, 38evls1var 22342 . . . . . . . . . . . 12 (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
7170fveq1d 6908 . . . . . . . . . . 11 (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72 fvresi 7193 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
7325, 72mp1i 13 . . . . . . . . . . 11 (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
7471, 73eqtrd 2777 . . . . . . . . . 10 (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
7574oveq2d 7447 . . . . . . . . 9 (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76 cnfldexp 21417 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
7726, 50, 76syl2anc 584 . . . . . . . . 9 (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
7869, 75, 773eqtrd 2781 . . . . . . . 8 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = (𝐴↑3))
7918oveq1i 7441 . . . . . . . . 9 (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80 3nn 12345 . . . . . . . . . 10 3 ∈ ℕ
81 cxproot 26732 . . . . . . . . . 10 ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
8219, 80, 81mp2an 692 . . . . . . . . 9 ((2↑𝑐(1 / 3))↑3) = 2
8379, 82eqtri 2765 . . . . . . . 8 (𝐴↑3) = 2
8478, 83eqtrdi 2793 . . . . . . 7 (⊤ → (((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) = 2)
851, 2, 3, 6, 55, 37, 38, 65, 26evls1scafv 22370 . . . . . . 7 (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
8684, 85oveq12d 7449 . . . . . 6 (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
8719subidi 11580 . . . . . 6 (2 − 2) = 0
8886, 87eqtrdi 2793 . . . . 5 (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
8933, 67, 883eqtrd 2781 . . . 4 (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
903qrng0 27665 . . . . 5 0 = (0g𝑄)
91 eqid 2737 . . . . 5 (eval1𝑄) = (eval1𝑄)
92 2sqr3minply.d . . . . 5 𝐷 = (deg1𝑄)
93 fldsdrgfld 20799 . . . . . . . 8 ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂflds ℚ) ∈ Field)
9410, 16, 93mp2an 692 . . . . . . 7 (ℂflds ℚ) ∈ Field
953, 94eqeltri 2837 . . . . . 6 𝑄 ∈ Field
9695a1i 11 . . . . 5 (⊤ → 𝑄 ∈ Field)
9746ringgrpd 20239 . . . . . . 7 (⊤ → 𝑃 ∈ Grp)
9834, 35grpsubcl 19038 . . . . . . 7 ((𝑃 ∈ Grp ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 𝑋) (𝐾‘2)) ∈ (Base‘𝑃))
9997, 54, 66, 98syl3anc 1373 . . . . . 6 (⊤ → ((3 𝑋) (𝐾‘2)) ∈ (Base‘𝑃))
10030, 99eqeltrid 2845 . . . . 5 (⊤ → 𝐹 ∈ (Base‘𝑃))
10196fldcrngd 20742 . . . . . . . . 9 (⊤ → 𝑄 ∈ CRing)
10291, 2, 34, 101, 61, 100evl1fvf 33589 . . . . . . . 8 (⊤ → ((eval1𝑄)‘𝐹):ℚ⟶ℚ)
103102ffnd 6737 . . . . . . 7 (⊤ → ((eval1𝑄)‘𝐹) Fn ℚ)
104 fniniseg2 7082 . . . . . . 7 (((eval1𝑄)‘𝐹) Fn ℚ → (((eval1𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0})
105103, 104syl 17 . . . . . 6 (⊤ → (((eval1𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0})
106 cnfldmul 21372 . . . . . . . . . . . . . . 15 · = (.r‘ℂfld)
1073, 106ressmulr 17351 . . . . . . . . . . . . . 14 (ℚ ∈ (SubRing‘ℂfld) → · = (.r𝑄))
10813, 107ax-mp 5 . . . . . . . . . . . . 13 · = (.r𝑄)
109 cnfldadd 21370 . . . . . . . . . . . . . . 15 + = (+g‘ℂfld)
1103, 109ressplusg 17334 . . . . . . . . . . . . . 14 (ℚ ∈ (SubRing‘ℂfld) → + = (+g𝑄))
11113, 110ax-mp 5 . . . . . . . . . . . . 13 + = (+g𝑄)
112 eqid 2737 . . . . . . . . . . . . 13 (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113 eqid 2737 . . . . . . . . . . . . 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 12371 . . . . . . . . . . . . . . . . . . . . 21 0 < 3
119118a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 0 < 3)
120 2ne0 12370 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
121120a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → 2 ≠ 0)
12292, 2, 61, 55, 90deg1scl 26152 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
12344, 65, 121, 122syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝐷‘(𝐾‘2)) = 0)
124 drngnzr 20748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
12542, 124mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → 𝑄 ∈ NzRing)
12692, 2, 51, 39, 41deg1pw 26160 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 𝑋)) = 3)
127125, 50, 126syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝐷‘(3 𝑋)) = 3)
128119, 123, 1273brtr4d 5175 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 𝑋)))
1292, 92, 44, 34, 35, 54, 66, 128deg1sub 26147 . . . . . . . . . . . . . . . . . 18 (⊤ → (𝐷‘((3 𝑋) (𝐾‘2))) = (𝐷‘(3 𝑋)))
130117, 129, 1273eqtrd 2781 . . . . . . . . . . . . . . . . 17 (⊤ → (𝐷𝐹) = 3)
131115, 130fveq12d 6913 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = ((coe1‘((3 𝑋) (𝐾‘2)))‘3))
132 eqid 2737 . . . . . . . . . . . . . . . . . 18 (-g𝑄) = (-g𝑄)
1332, 34, 35, 132coe1subfv 22269 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 3 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘3) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
13444, 54, 66, 50, 133syl31anc 1375 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘3) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
135 subrgsubg 20577 . . . . . . . . . . . . . . . . . . 19 (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
13613, 135mp1i 13 . . . . . . . . . . . . . . . . . 18 (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (coe1‘(3 𝑋)) = (coe1‘(3 𝑋))
138137, 34, 2, 61coe1fvalcl 22214 . . . . . . . . . . . . . . . . . . 19 (((3 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 𝑋))‘3) ∈ ℚ)
13954, 50, 138syl2anc 584 . . . . . . . . . . . . . . . . . 18 (⊤ → ((coe1‘(3 𝑋))‘3) ∈ ℚ)
140 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141140, 34, 2, 61coe1fvalcl 22214 . . . . . . . . . . . . . . . . . . 19 (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
14266, 50, 141syl2anc 584 . . . . . . . . . . . . . . . . . 18 (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
14336, 3, 132subgsub 19156 . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . 17 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)))
145 iftrue 4531 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
1463qrng1 27666 . . . . . . . . . . . . . . . . . . . . 21 1 = (1r𝑄)
1472, 51, 41, 44, 50, 90, 146coe1mon 33610 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (coe1‘(3 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148 1cnd 11256 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 1 ∈ ℂ)
149145, 147, 50, 148fvmptd4 7040 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((coe1‘(3 𝑋))‘3) = 1)
15021neii 2942 . . . . . . . . . . . . . . . . . . . . . 22 ¬ 3 = 0
151 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152150, 151mtbiri 327 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 3 → ¬ 𝑖 = 0)
153152iffalsed 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
1542, 55, 61, 90coe1scl 22290 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
15544, 65, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156 0nn0 12541 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℕ0
157156a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 0 ∈ ℕ0)
158153, 155, 50, 157fvmptd4 7040 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159149, 158oveq12d 7449 . . . . . . . . . . . . . . . . . 18 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160 1m0e1 12387 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
161159, 160eqtrdi 2793 . . . . . . . . . . . . . . . . 17 (⊤ → (((coe1‘(3 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162144, 161eqtr3d 2779 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘3)(-g𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163131, 134, 1623eqtrd 2781 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = 1)
164130fveq2d 6910 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘(𝐷𝐹)) = ((coe1𝐹)‘3))
165163, 164eqtr3d 2779 . . . . . . . . . . . . . 14 (⊤ → 1 = ((coe1𝐹)‘3))
166165mptru 1547 . . . . . . . . . . . . 13 1 = ((coe1𝐹)‘3)
167115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘2) = ((coe1‘((3 𝑋) (𝐾‘2)))‘2))
168 2nn0 12543 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
169168a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 2 ∈ ℕ0)
1702, 34, 35, 132coe1subfv 22269 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)))
17144, 54, 66, 169, 170syl31anc 1375 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)))
172 2re 12340 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
173 2lt3 12438 . . . . . . . . . . . . . . . . . . . . . . 23 2 < 3
174172, 173ltneii 11374 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 3
175 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176174, 175mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 2 → 𝑖 ≠ 3)
177176adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178177neneqd 2945 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179178iffalsed 4536 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180147, 179, 169, 157fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘2) = 0)
181 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182120, 181mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 2 → 𝑖 ≠ 0)
183182neneqd 2945 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 2 → ¬ 𝑖 = 0)
184183adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185184iffalsed 4536 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186155, 185, 169, 157fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187180, 186oveq12d 7449 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘2)(-g𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g𝑄)0))
188171, 187eqtrd 2777 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘2) = (0(-g𝑄)0))
189158, 142eqeltrrd 2842 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ℚ)
19036, 3, 132subgsub 19156 . . . . . . . . . . . . . . . . 17 ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g𝑄)0))
191136, 189, 189, 190syl3anc 1373 . . . . . . . . . . . . . . . 16 (⊤ → (0 − 0) = (0(-g𝑄)0))
192 0m0e0 12386 . . . . . . . . . . . . . . . 16 (0 − 0) = 0
193191, 192eqtr3di 2792 . . . . . . . . . . . . . . 15 (⊤ → (0(-g𝑄)0) = 0)
194167, 188, 1933eqtrrd 2782 . . . . . . . . . . . . . 14 (⊤ → 0 = ((coe1𝐹)‘2))
195194mptru 1547 . . . . . . . . . . . . 13 0 = ((coe1𝐹)‘2)
196115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘1) = ((coe1‘((3 𝑋) (𝐾‘2)))‘1))
197 1nn0 12542 . . . . . . . . . . . . . . . . . 18 1 ∈ ℕ0
198197a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ℕ0)
1992, 34, 35, 132coe1subfv 22269 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)))
20044, 54, 66, 198, 199syl31anc 1375 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)))
201 1re 11261 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
202 1lt3 12439 . . . . . . . . . . . . . . . . . . . . . . 23 1 < 3
203201, 202ltneii 11374 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 3
204 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205203, 204mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 1 → 𝑖 ≠ 3)
206205neneqd 2945 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 1 → ¬ 𝑖 = 3)
207206adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208207iffalsed 4536 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209147, 208, 198, 157fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘1) = 0)
210 ax-1ne0 11224 . . . . . . . . . . . . . . . . . . . . . 22 1 ≠ 0
211 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212210, 211mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 1 → 𝑖 ≠ 0)
213212neneqd 2945 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 1 → ¬ 𝑖 = 0)
214213adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215214iffalsed 4536 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216155, 215, 198, 157fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217209, 216oveq12d 7449 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘1)(-g𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g𝑄)0))
218200, 217eqtrd 2777 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘1) = (0(-g𝑄)0))
219196, 218, 1933eqtrrd 2782 . . . . . . . . . . . . . 14 (⊤ → 0 = ((coe1𝐹)‘1))
220219mptru 1547 . . . . . . . . . . . . 13 0 = ((coe1𝐹)‘1)
221115fveq1d 6908 . . . . . . . . . . . . . . 15 (⊤ → ((coe1𝐹)‘0) = ((coe1‘((3 𝑋) (𝐾‘2)))‘0))
2222, 34, 35, 132coe1subfv 22269 . . . . . . . . . . . . . . . . 17 (((𝑄 ∈ Ring ∧ (3 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)))
22344, 54, 66, 157, 222syl31anc 1375 . . . . . . . . . . . . . . . 16 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)))
22421necomi 2995 . . . . . . . . . . . . . . . . . . . . . 22 0 ≠ 3
225 neeq1 3003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226224, 225mpbiri 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → 𝑖 ≠ 3)
227226neneqd 2945 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ¬ 𝑖 = 3)
228227adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229228iffalsed 4536 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230147, 229, 157, 157fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(3 𝑋))‘0) = 0)
231 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232231iftrued 4533 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233155, 232, 157, 169fvmptd 7023 . . . . . . . . . . . . . . . . 17 (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234230, 233oveq12d 7449 . . . . . . . . . . . . . . . 16 (⊤ → (((coe1‘(3 𝑋))‘0)(-g𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g𝑄)2))
235223, 234eqtrd 2777 . . . . . . . . . . . . . . 15 (⊤ → ((coe1‘((3 𝑋) (𝐾‘2)))‘0) = (0(-g𝑄)2))
236 df-neg 11495 . . . . . . . . . . . . . . . 16 -2 = (0 − 2)
23736, 3, 132subgsub 19156 . . . . . . . . . . . . . . . . 17 ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g𝑄)2))
238136, 189, 65, 237syl3anc 1373 . . . . . . . . . . . . . . . 16 (⊤ → (0 − 2) = (0(-g𝑄)2))
239236, 238eqtr2id 2790 . . . . . . . . . . . . . . 15 (⊤ → (0(-g𝑄)2) = -2)
240221, 235, 2393eqtrrd 2782 . . . . . . . . . . . . . 14 (⊤ → -2 = ((coe1𝐹)‘0))
241240mptru 1547 . . . . . . . . . . . . 13 -2 = ((coe1𝐹)‘0)
24295a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243242fldcrngd 20742 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → 𝑄 ∈ CRing)
244100mptru 1547 . . . . . . . . . . . . . 14 𝐹 ∈ (Base‘𝑃)
245244a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃))
246130mptru 1547 . . . . . . . . . . . . . 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 33603 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250 qsscn 13002 . . . . . . . . . . . . . . . . . 18 ℚ ⊆ ℂ
251 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253252, 6mgpbas 20142 . . . . . . . . . . . . . . . . . . . . . 22 ℂ = (Base‘(mulGrp‘ℂfld))
254251, 253ressbas2 17283 . . . . . . . . . . . . . . . . . . . . 21 (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255250, 254ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
2563, 252mgpress 20147 . . . . . . . . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . . . . . . . . . 19 ℚ = (Base‘(mulGrp‘𝑄))
260 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (mulGrp‘𝑄) = (mulGrp‘𝑄)
261260ringmgp 20236 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
26256, 261mp1i 13 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → (mulGrp‘𝑄) ∈ Mnd)
26349a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → 3 ∈ ℕ0)
264259, 112, 262, 263, 248mulgnn0cld 19113 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265250, 264sselid 3981 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266265mullidd 11279 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267257eqcomi 2746 . . . . . . . . . . . . . . . . 17 (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268250, 253sseqtri 4032 . . . . . . . . . . . . . . . . . 18 ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269268a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
27080a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 3 ∈ ℕ)
271267, 269, 248, 270ressmulgnnd 19096 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272 qcn 13005 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273 cnfldexp 21417 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274272, 263, 273syl2anc 584 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275266, 271, 2743eqtrd 2781 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276168a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277259, 112, 262, 276, 248mulgnn0cld 19113 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278250, 277sselid 3981 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279278mul02d 11459 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280275, 279oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281272, 263expcld 14186 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282281addridd 11461 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283280, 282eqtrd 2777 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284272mul02d 11459 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285284oveq1d 7446 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
28619a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → 2 ∈ ℂ)
287286negcld 11607 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → -2 ∈ ℂ)
288287addlidd 11462 . . . . . . . . . . . . . 14 (𝑥 ∈ ℚ → (0 + -2) = -2)
289285, 288eqtrd 2777 . . . . . . . . . . . . 13 (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290283, 289oveq12d 7449 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291281, 286negsubd 11626 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292249, 290, 2913eqtrd 2781 . . . . . . . . . . 11 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293 2prm 16729 . . . . . . . . . . . . . . 15 2 ∈ ℙ
294 3z 12650 . . . . . . . . . . . . . . . 16 3 ∈ ℤ
295 3re 12346 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
296172, 295, 173ltleii 11384 . . . . . . . . . . . . . . . 16 2 ≤ 3
29763eluz1i 12886 . . . . . . . . . . . . . . . 16 (3 ∈ (ℤ‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298294, 296, 297mpbir2an 711 . . . . . . . . . . . . . . 15 3 ∈ (ℤ‘2)
299 rtprmirr 26803 . . . . . . . . . . . . . . 15 ((2 ∈ ℙ ∧ 3 ∈ (ℤ‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300293, 298, 299mp2an 692 . . . . . . . . . . . . . 14 (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301 eldifn 4132 . . . . . . . . . . . . . 14 ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302300, 301ax-mp 5 . . . . . . . . . . . . 13 ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303 nelne2 3040 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304302, 303mpan2 691 . . . . . . . . . . . 12 (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305 qre 12995 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306305adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307 2pos 12369 . . . . . . . . . . . . . . . . . 18 0 < 2
308281, 286subeq0ad 11630 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309308biimpa 476 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310307, 309breqtrrid 5181 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
31180a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312 n2dvds3 16408 . . . . . . . . . . . . . . . . . . 19 ¬ 2 ∥ 3
313312a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314306, 311, 313expgt0b 32818 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315310, 314mpbird 257 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316306, 315elrpd 13074 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ+)
317295a1i 11 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℝ)
31822a1i 11 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (1 / 3) ∈ ℂ)
319316, 317, 318cxpmuld 26779 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥𝑐(3 · (1 / 3))) = ((𝑥𝑐3)↑𝑐(1 / 3)))
32020a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 3 ∈ ℂ)
32121a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℚ → 3 ≠ 0)
322320, 321recidd 12038 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323322oveq2d 7447 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐(3 · (1 / 3))) = (𝑥𝑐1))
324272cxp1d 26748 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐1) = 𝑥)
325323, 324eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → (𝑥𝑐(3 · (1 / 3))) = 𝑥)
326325adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥𝑐(3 · (1 / 3))) = 𝑥)
327 cxpexp 26710 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥𝑐3) = (𝑥↑3))
328272, 263, 327syl2anc 584 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℚ → (𝑥𝑐3) = (𝑥↑3))
329328oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℚ → ((𝑥𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330329adantr 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331319, 326, 3303eqtr3rd 2786 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332309oveq1d 7446 . . . . . . . . . . . . 13 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333331, 332eqtr3d 2779 . . . . . . . . . . . 12 ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334304, 333mteqand 3033 . . . . . . . . . . 11 (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335292, 334eqnetrd 3008 . . . . . . . . . 10 (𝑥 ∈ ℚ → (((eval1𝑄)‘𝐹)‘𝑥) ≠ 0)
336335neneqd 2945 . . . . . . . . 9 (𝑥 ∈ ℚ → ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
337336rgen 3063 . . . . . . . 8 𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0
338337a1i 11 . . . . . . 7 (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
339 rabeq0 4388 . . . . . . 7 ({𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1𝑄)‘𝐹)‘𝑥) = 0)
340338, 339sylibr 234 . . . . . 6 (⊤ → {𝑥 ∈ ℚ ∣ (((eval1𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341105, 340eqtrd 2777 . . . . 5 (⊤ → (((eval1𝑄)‘𝐹) “ {0}) = ∅)
34290, 91, 92, 2, 34, 96, 100, 341, 130ply1dg3rt0irred 33607 . . . 4 (⊤ → 𝐹 ∈ (Irred‘𝑃))
343 eqid 2737 . . . . . . 7 (Irred‘𝑃) = (Irred‘𝑃)
344343, 29irredn0 20423 . . . . . 6 ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g𝑃))
34546, 342, 344syl2anc 584 . . . . 5 (⊤ → 𝐹 ≠ (0g𝑃))
3463fveq2i 6909 . . . . . . 7 (deg1𝑄) = (deg1‘(ℂflds ℚ))
34792, 346eqtri 2765 . . . . . 6 𝐷 = (deg1‘(ℂflds ℚ))
348 eqid 2737 . . . . . 6 (Monic1p‘(ℂflds ℚ)) = (Monic1p‘(ℂflds ℚ))
349 eqid 2737 . . . . . . 7 (ℂflds ℚ) = (ℂflds ℚ)
350349qrng1 27666 . . . . . 6 1 = (1r‘(ℂflds ℚ))
3515, 34, 29, 347, 348, 350ismon1p 26182 . . . . 5 (𝐹 ∈ (Monic1p‘(ℂflds ℚ)) ↔ (𝐹 ∈ (Base‘𝑃) ∧ 𝐹 ≠ (0g𝑃) ∧ ((coe1𝐹)‘(𝐷𝐹)) = 1))
352100, 345, 163, 351syl3anbrc 1344 . . . 4 (⊤ → 𝐹 ∈ (Monic1p‘(ℂflds ℚ)))
3531, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352irredminply 33757 . . 3 (⊤ → 𝐹 = (𝑀𝐴))
354353, 130jca 511 . 2 (⊤ → (𝐹 = (𝑀𝐴) ∧ (𝐷𝐹) = 3))
355354mptru 1547 1 (𝐹 = (𝑀𝐴) ∧ (𝐷𝐹) = 3)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1540  wtru 1541  wcel 2108  wne 2940  wral 3061  {crab 3436  cdif 3948  wss 3951  c0 4333  ifcif 4525  {csn 4626   class class class wbr 5143  cmpt 5225   I cid 5577  ccnv 5684  cres 5687  cima 5688   Fn wfn 6556  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492  -cneg 11493   / cdiv 11920  cn 12266  2c2 12321  3c3 12322  0cn0 12526  cz 12613  cuz 12878  cq 12990  cexp 14102  cdvds 16290  cprime 16708  Basecbs 17247  s cress 17274  +gcplusg 17297  .rcmulr 17298  Scalarcsca 17300  0gc0g 17484  Mndcmnd 18747  Grpcgrp 18951  -gcsg 18953  .gcmg 19085  SubGrpcsubg 19138  mulGrpcmgp 20137  Ringcrg 20230  CRingccrg 20231  Irredcir 20356  NzRingcnzr 20512  SubRingcsubrg 20569  DivRingcdr 20729  Fieldcfield 20730  SubDRingcsdrg 20787  LModclmod 20858  fldccnfld 21364  algSccascl 21872  var1cv1 22177  Poly1cpl1 22178  coe1cco1 22179   evalSub1 ces1 22317  eval1ce1 22318  deg1cdg1 26093  Monic1pcmn1 26165  𝑐ccxp 26597   minPoly cminply 33742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234  ax-mulf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-numer 16772  df-denom 16773  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  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 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-pws 17494  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-srg 20184  df-ring 20232  df-cring 20233  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-irred 20359  df-invr 20388  df-dvr 20401  df-rhm 20472  df-nzr 20513  df-subrng 20546  df-subrg 20570  df-rlreg 20694  df-domn 20695  df-idom 20696  df-drng 20731  df-field 20732  df-sdrg 20788  df-lmod 20860  df-lss 20930  df-lsp 20970  df-sra 21172  df-rgmod 21173  df-lidl 21218  df-rsp 21219  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-assa 21873  df-asp 21874  df-ascl 21875  df-psr 21929  df-mvr 21930  df-mpl 21931  df-opsr 21933  df-evls 22098  df-evl 22099  df-psr1 22181  df-vr1 22182  df-ply1 22183  df-coe1 22184  df-evls1 22319  df-evl1 22320  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-mdeg 26094  df-deg1 26095  df-mon1 26170  df-uc1p 26171  df-q1p 26172  df-r1p 26173  df-ig1p 26174  df-log 26598  df-cxp 26599  df-irng 33734  df-minply 33743
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator