| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(ℂfld evalSub1 ℚ) =
(ℂfld evalSub1 ℚ) |
| 2 | | 2sqr3minply.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑄) |
| 3 | | 2sqr3minply.q |
. . . . . 6
⊢ 𝑄 = (ℂfld
↾s ℚ) |
| 4 | 3 | fveq2i 6909 |
. . . . 5
⊢
(Poly1‘𝑄) =
(Poly1‘(ℂfld ↾s
ℚ)) |
| 5 | 2, 4 | eqtri 2765 |
. . . 4
⊢ 𝑃 =
(Poly1‘(ℂfld ↾s
ℚ)) |
| 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)) |
| 10 | 7, 8, 9 | mpbir2an 711 |
. . . . 5
⊢
ℂfld ∈ Field |
| 11 | 10 | a1i 11 |
. . . 4
⊢ (⊤
→ ℂfld ∈ Field) |
| 12 | | qsubdrg 21437 |
. . . . . . 7
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) |
| 13 | 12 | simpli 483 |
. . . . . 6
⊢ ℚ
∈ (SubRing‘ℂfld) |
| 14 | 12 | simpri 485 |
. . . . . 6
⊢
(ℂfld ↾s ℚ) ∈
DivRing |
| 15 | | issdrg 20789 |
. . . . . 6
⊢ (ℚ
∈ (SubDRing‘ℂfld) ↔ (ℂfld
∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧
(ℂfld ↾s ℚ) ∈
DivRing)) |
| 16 | 7, 13, 14, 15 | mpbir3an 1342 |
. . . . 5
⊢ ℚ
∈ (SubDRing‘ℂfld) |
| 17 | 16 | a1i 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 |
| 22 | 20, 21 | reccli 11997 |
. . . . . . 7
⊢ (1 / 3)
∈ ℂ |
| 23 | | cxpcl 26716 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ (1 / 3) ∈ ℂ) →
(2↑𝑐(1 / 3)) ∈ ℂ) |
| 24 | 19, 22, 23 | mp2an 692 |
. . . . . 6
⊢
(2↑𝑐(1 / 3)) ∈ ℂ |
| 25 | 18, 24 | eqeltri 2837 |
. . . . 5
⊢ 𝐴 ∈ ℂ |
| 26 | 25 | a1i 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)) |
| 31 | 30 | fveq2i 6909 |
. . . . . . 7
⊢
((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld
evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2))) |
| 32 | 31 | fveq1i 6907 |
. . . . . 6
⊢
(((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld
evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) |
| 33 | 32 | a1i 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) |
| 37 | 8 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℂfld ∈ CRing) |
| 38 | 13 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℚ ∈ (SubRing‘ℂfld)) |
| 39 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 40 | 39, 34 | mgpbas 20142 |
. . . . . . 7
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
| 41 | | 2sqr3minply.2 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑃)) |
| 42 | 3 | qdrng 27664 |
. . . . . . . . . . 11
⊢ 𝑄 ∈ DivRing |
| 43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 𝑄 ∈
DivRing) |
| 44 | 43 | drngringd 20737 |
. . . . . . . . 9
⊢ (⊤
→ 𝑄 ∈
Ring) |
| 45 | 2 | ply1ring 22249 |
. . . . . . . . 9
⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring) |
| 46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ (⊤
→ 𝑃 ∈
Ring) |
| 47 | 39 | ringmgp 20236 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ (⊤
→ (mulGrp‘𝑃)
∈ Mnd) |
| 49 | | 3nn0 12544 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
| 50 | 49 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 3 ∈ ℕ0) |
| 51 | | 2sqr3minply.x |
. . . . . . . . 9
⊢ 𝑋 = (var1‘𝑄) |
| 52 | 51, 2, 34 | vr1cl 22219 |
. . . . . . . 8
⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
| 53 | 44, 52 | syl 17 |
. . . . . . 7
⊢ (⊤
→ 𝑋 ∈
(Base‘𝑃)) |
| 54 | 40, 41, 48, 50, 53 | mulgnn0cld 19113 |
. . . . . 6
⊢ (⊤
→ (3 ↑ 𝑋) ∈ (Base‘𝑃)) |
| 55 | | 2sqr3minply.k |
. . . . . . . 8
⊢ 𝐾 = (algSc‘𝑃) |
| 56 | 44 | mptru 1547 |
. . . . . . . . 9
⊢ 𝑄 ∈ Ring |
| 57 | 2 | ply1sca 22254 |
. . . . . . . . 9
⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃)) |
| 58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢ 𝑄 = (Scalar‘𝑃) |
| 59 | 2 | ply1lmod 22253 |
. . . . . . . . 9
⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod) |
| 60 | 44, 59 | syl 17 |
. . . . . . . 8
⊢ (⊤
→ 𝑃 ∈
LMod) |
| 61 | 3 | qrngbas 27663 |
. . . . . . . 8
⊢ ℚ =
(Base‘𝑄) |
| 62 | 55, 58, 46, 60, 61, 34 | asclf 21902 |
. . . . . . 7
⊢ (⊤
→ 𝐾:ℚ⟶(Base‘𝑃)) |
| 63 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 64 | | zq 12996 |
. . . . . . . 8
⊢ (2 ∈
ℤ → 2 ∈ ℚ) |
| 65 | 63, 64 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ 2 ∈ ℚ) |
| 66 | 62, 65 | ffvelcdmd 7105 |
. . . . . 6
⊢ (⊤
→ (𝐾‘2) ∈
(Base‘𝑃)) |
| 67 | 1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26 | evls1subd 33597 |
. . . . 5
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) = ((((ℂfld
evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld
evalSub1 ℚ)‘(𝐾‘2))‘𝐴))) |
| 68 | | eqid 2737 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
| 69 | 1, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26 | evls1expd 22371 |
. . . . . . . . 9
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) =
(3(.g‘(mulGrp‘ℂfld))(((ℂfld
evalSub1 ℚ)‘𝑋)‘𝐴))) |
| 70 | 1, 51, 3, 6, 37, 38 | evls1var 22342 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾
ℂ)) |
| 71 | 70 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴)) |
| 72 | | fvresi 7193 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (( I
↾ ℂ)‘𝐴) =
𝐴) |
| 73 | 25, 72 | mp1i 13 |
. . . . . . . . . . 11
⊢ (⊤
→ (( I ↾ ℂ)‘𝐴) = 𝐴) |
| 74 | 71, 73 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴) |
| 75 | 74 | oveq2d 7447 |
. . . . . . . . 9
⊢ (⊤
→
(3(.g‘(mulGrp‘ℂfld))(((ℂfld
evalSub1 ℚ)‘𝑋)‘𝐴)) =
(3(.g‘(mulGrp‘ℂfld))𝐴)) |
| 76 | | cnfldexp 21417 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 3 ∈
ℕ0) →
(3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3)) |
| 77 | 26, 50, 76 | syl2anc 584 |
. . . . . . . . 9
⊢ (⊤
→ (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3)) |
| 78 | 69, 75, 77 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3)) |
| 79 | 18 | oveq1i 7441 |
. . . . . . . . 9
⊢ (𝐴↑3) =
((2↑𝑐(1 / 3))↑3) |
| 80 | | 3nn 12345 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
| 81 | | cxproot 26732 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 /
3))↑3) = 2) |
| 82 | 19, 80, 81 | mp2an 692 |
. . . . . . . . 9
⊢
((2↑𝑐(1 / 3))↑3) = 2 |
| 83 | 79, 82 | eqtri 2765 |
. . . . . . . 8
⊢ (𝐴↑3) = 2 |
| 84 | 78, 83 | eqtrdi 2793 |
. . . . . . 7
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = 2) |
| 85 | 1, 2, 3, 6, 55, 37, 38, 65, 26 | evls1scafv 22370 |
. . . . . . 7
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2) |
| 86 | 84, 85 | oveq12d 7449 |
. . . . . 6
⊢ (⊤
→ ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld
evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2)) |
| 87 | 19 | subidi 11580 |
. . . . . 6
⊢ (2
− 2) = 0 |
| 88 | 86, 87 | eqtrdi 2793 |
. . . . 5
⊢ (⊤
→ ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld
evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0) |
| 89 | 33, 67, 88 | 3eqtrd 2781 |
. . . 4
⊢ (⊤
→ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0) |
| 90 | 3 | qrng0 27665 |
. . . . 5
⊢ 0 =
(0g‘𝑄) |
| 91 | | eqid 2737 |
. . . . 5
⊢
(eval1‘𝑄) = (eval1‘𝑄) |
| 92 | | 2sqr3minply.d |
. . . . 5
⊢ 𝐷 = (deg1‘𝑄) |
| 93 | | fldsdrgfld 20799 |
. . . . . . . 8
⊢
((ℂfld ∈ Field ∧ ℚ ∈
(SubDRing‘ℂfld)) → (ℂfld
↾s ℚ) ∈ Field) |
| 94 | 10, 16, 93 | mp2an 692 |
. . . . . . 7
⊢
(ℂfld ↾s ℚ) ∈
Field |
| 95 | 3, 94 | eqeltri 2837 |
. . . . . 6
⊢ 𝑄 ∈ Field |
| 96 | 95 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑄 ∈
Field) |
| 97 | 46 | ringgrpd 20239 |
. . . . . . 7
⊢ (⊤
→ 𝑃 ∈
Grp) |
| 98 | 34, 35 | grpsubcl 19038 |
. . . . . . 7
⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃)) |
| 99 | 97, 54, 66, 98 | syl3anc 1373 |
. . . . . 6
⊢ (⊤
→ ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃)) |
| 100 | 30, 99 | eqeltrid 2845 |
. . . . 5
⊢ (⊤
→ 𝐹 ∈
(Base‘𝑃)) |
| 101 | 96 | fldcrngd 20742 |
. . . . . . . . 9
⊢ (⊤
→ 𝑄 ∈
CRing) |
| 102 | 91, 2, 34, 101, 61, 100 | evl1fvf 33589 |
. . . . . . . 8
⊢ (⊤
→ ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ) |
| 103 | 102 | ffnd 6737 |
. . . . . . 7
⊢ (⊤
→ ((eval1‘𝑄)‘𝐹) Fn ℚ) |
| 104 | | fniniseg2 7082 |
. . . . . . 7
⊢
(((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣
(((eval1‘𝑄)‘𝐹)‘𝑥) = 0}) |
| 105 | 103, 104 | syl 17 |
. . . . . 6
⊢ (⊤
→ (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣
(((eval1‘𝑄)‘𝐹)‘𝑥) = 0}) |
| 106 | | cnfldmul 21372 |
. . . . . . . . . . . . . . 15
⊢ ·
= (.r‘ℂfld) |
| 107 | 3, 106 | ressmulr 17351 |
. . . . . . . . . . . . . 14
⊢ (ℚ
∈ (SubRing‘ℂfld) → · =
(.r‘𝑄)) |
| 108 | 13, 107 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ·
= (.r‘𝑄) |
| 109 | | cnfldadd 21370 |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘ℂfld) |
| 110 | 3, 109 | ressplusg 17334 |
. . . . . . . . . . . . . 14
⊢ (ℚ
∈ (SubRing‘ℂfld) → + =
(+g‘𝑄)) |
| 111 | 13, 110 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑄) |
| 112 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.g‘(mulGrp‘𝑄)) =
(.g‘(mulGrp‘𝑄)) |
| 113 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(coe1‘𝐹) = (coe1‘𝐹) |
| 114 | 30 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . 18
⊢
(coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))) |
| 115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))) |
| 116 | 30 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) |
| 117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))) |
| 118 | | 3pos 12371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
3 |
| 119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ 0 < 3) |
| 120 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
0 |
| 121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⊤
→ 2 ≠ 0) |
| 122 | 92, 2, 61, 55, 90 | deg1scl 26152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ Ring ∧ 2 ∈
ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0) |
| 123 | 44, 65, 121, 122 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ (𝐷‘(𝐾‘2)) = 0) |
| 124 | | drngnzr 20748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing) |
| 125 | 42, 124 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⊤
→ 𝑄 ∈
NzRing) |
| 126 | 92, 2, 51, 39, 41 | deg1pw 26160 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ NzRing ∧ 3 ∈
ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3) |
| 127 | 125, 50, 126 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ (𝐷‘(3 ↑ 𝑋)) = 3) |
| 128 | 119, 123,
127 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋))) |
| 129 | 2, 92, 44, 34, 35, 54, 66, 128 | deg1sub 26147 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋))) |
| 130 | 117, 129,
127 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (𝐷‘𝐹) = 3) |
| 131 | 115, 130 | fveq12d 6913 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3)) |
| 132 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(-g‘𝑄) = (-g‘𝑄) |
| 133 | 2, 34, 35, 132 | coe1subfv 22269 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 3 ∈
ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) =
(((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3))) |
| 134 | 44, 54, 66, 50, 133 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) =
(((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3))) |
| 135 | | subrgsubg 20577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℚ
∈ (SubRing‘ℂfld) → ℚ ∈
(SubGrp‘ℂfld)) |
| 136 | 13, 135 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ ℚ ∈ (SubGrp‘ℂfld)) |
| 137 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(coe1‘(3 ↑ 𝑋)) = (coe1‘(3 ↑ 𝑋)) |
| 138 | 137, 34, 2, 61 | coe1fvalcl 22214 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((3
↑
𝑋) ∈ (Base‘𝑃) ∧ 3 ∈
ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ) |
| 139 | 54, 50, 138 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ) |
| 140 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2)) |
| 141 | 140, 34, 2, 61 | coe1fvalcl 22214 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾‘2) ∈
(Base‘𝑃) ∧ 3
∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈
ℚ) |
| 142 | 66, 50, 141 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ ((coe1‘(𝐾‘2))‘3) ∈
ℚ) |
| 143 | 36, 3, 132 | subgsub 19156 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℚ
∈ (SubGrp‘ℂfld) ∧ ((coe1‘(3
↑
𝑋))‘3) ∈ ℚ
∧ ((coe1‘(𝐾‘2))‘3) ∈ ℚ) →
(((coe1‘(3 ↑ 𝑋))‘3) −
((coe1‘(𝐾‘2))‘3)) =
(((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3))) |
| 144 | 136, 139,
142, 143 | syl3anc 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) |
| 146 | 3 | qrng1 27666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 =
(1r‘𝑄) |
| 147 | 2, 51, 41, 44, 50, 90, 146 | coe1mon 33610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0))) |
| 148 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ 1 ∈ ℂ) |
| 149 | 145, 147,
50, 148 | fvmptd4 7040 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ ((coe1‘(3 ↑ 𝑋))‘3) = 1) |
| 150 | 21 | neii 2942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ¬ 3
= 0 |
| 151 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0)) |
| 152 | 150, 151 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 3 → ¬ 𝑖 = 0) |
| 153 | 152 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) =
0) |
| 154 | 2, 55, 61, 90 | coe1scl 22290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ Ring ∧ 2 ∈
ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0))) |
| 155 | 44, 65, 154 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0))) |
| 156 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℕ0 |
| 157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ 0 ∈ ℕ0) |
| 158 | 153, 155,
50, 157 | fvmptd4 7040 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ ((coe1‘(𝐾‘2))‘3) = 0) |
| 159 | 149, 158 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘3) −
((coe1‘(𝐾‘2))‘3)) = (1 −
0)) |
| 160 | | 1m0e1 12387 |
. . . . . . . . . . . . . . . . . 18
⊢ (1
− 0) = 1 |
| 161 | 159, 160 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘3) −
((coe1‘(𝐾‘2))‘3)) = 1) |
| 162 | 144, 161 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)) =
1) |
| 163 | 131, 134,
162 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1) |
| 164 | 130 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3)) |
| 165 | 163, 164 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 1 = ((coe1‘𝐹)‘3)) |
| 166 | 165 | mptru 1547 |
. . . . . . . . . . . . 13
⊢ 1 =
((coe1‘𝐹)‘3) |
| 167 | 115 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘𝐹)‘2) = ((coe1‘((3
↑
𝑋) − (𝐾‘2)))‘2)) |
| 168 | | 2nn0 12543 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ0 |
| 169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 2 ∈ ℕ0) |
| 170 | 2, 34, 35, 132 | coe1subfv 22269 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 2 ∈
ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) =
(((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2))) |
| 171 | 44, 54, 66, 169, 170 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) =
(((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2))) |
| 172 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
| 173 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 <
3 |
| 174 | 172, 173 | ltneii 11374 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≠
3 |
| 175 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3)) |
| 176 | 174, 175 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 2 → 𝑖 ≠ 3) |
| 177 | 176 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑖 =
2) → 𝑖 ≠
3) |
| 178 | 177 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
2) → ¬ 𝑖 =
3) |
| 179 | 178 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
2) → if(𝑖 = 3, 1, 0) =
0) |
| 180 | 147, 179,
169, 157 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(3 ↑ 𝑋))‘2) = 0) |
| 181 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0)) |
| 182 | 120, 181 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 2 → 𝑖 ≠ 0) |
| 183 | 182 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 2 → ¬ 𝑖 = 0) |
| 184 | 183 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
2) → ¬ 𝑖 =
0) |
| 185 | 184 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
2) → if(𝑖 = 0, 2, 0) =
0) |
| 186 | 155, 185,
169, 157 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(𝐾‘2))‘2) = 0) |
| 187 | 180, 186 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)) =
(0(-g‘𝑄)0)) |
| 188 | 171, 187 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) =
(0(-g‘𝑄)0)) |
| 189 | 158, 142 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 0 ∈ ℚ) |
| 190 | 36, 3, 132 | subgsub 19156 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℚ
∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0
∈ ℚ) → (0 − 0) = (0(-g‘𝑄)0)) |
| 191 | 136, 189,
189, 190 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (0 − 0) = (0(-g‘𝑄)0)) |
| 192 | | 0m0e0 12386 |
. . . . . . . . . . . . . . . 16
⊢ (0
− 0) = 0 |
| 193 | 191, 192 | eqtr3di 2792 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (0(-g‘𝑄)0) = 0) |
| 194 | 167, 188,
193 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 0 = ((coe1‘𝐹)‘2)) |
| 195 | 194 | mptru 1547 |
. . . . . . . . . . . . 13
⊢ 0 =
((coe1‘𝐹)‘2) |
| 196 | 115 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘𝐹)‘1) = ((coe1‘((3
↑
𝑋) − (𝐾‘2)))‘1)) |
| 197 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 |
| 198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 1 ∈ ℕ0) |
| 199 | 2, 34, 35, 132 | coe1subfv 22269 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 1 ∈
ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) =
(((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1))) |
| 200 | 44, 54, 66, 198, 199 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) =
(((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1))) |
| 201 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
| 202 | | 1lt3 12439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 <
3 |
| 203 | 201, 202 | ltneii 11374 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≠
3 |
| 204 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3)) |
| 205 | 203, 204 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 1 → 𝑖 ≠ 3) |
| 206 | 205 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 1 → ¬ 𝑖 = 3) |
| 207 | 206 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
1) → ¬ 𝑖 =
3) |
| 208 | 207 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
1) → if(𝑖 = 3, 1, 0) =
0) |
| 209 | 147, 208,
198, 157 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(3 ↑ 𝑋))‘1) = 0) |
| 210 | | ax-1ne0 11224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≠
0 |
| 211 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0)) |
| 212 | 210, 211 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 1 → 𝑖 ≠ 0) |
| 213 | 212 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 1 → ¬ 𝑖 = 0) |
| 214 | 213 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
1) → ¬ 𝑖 =
0) |
| 215 | 214 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
1) → if(𝑖 = 0, 2, 0) =
0) |
| 216 | 155, 215,
198, 157 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(𝐾‘2))‘1) = 0) |
| 217 | 209, 216 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)) =
(0(-g‘𝑄)0)) |
| 218 | 200, 217 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) =
(0(-g‘𝑄)0)) |
| 219 | 196, 218,
193 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 0 = ((coe1‘𝐹)‘1)) |
| 220 | 219 | mptru 1547 |
. . . . . . . . . . . . 13
⊢ 0 =
((coe1‘𝐹)‘1) |
| 221 | 115 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘𝐹)‘0) = ((coe1‘((3
↑
𝑋) − (𝐾‘2)))‘0)) |
| 222 | 2, 34, 35, 132 | coe1subfv 22269 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 0 ∈
ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) =
(((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0))) |
| 223 | 44, 54, 66, 157, 222 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) =
(((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0))) |
| 224 | 21 | necomi 2995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ≠
3 |
| 225 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3)) |
| 226 | 224, 225 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 0 → 𝑖 ≠ 3) |
| 227 | 226 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 0 → ¬ 𝑖 = 3) |
| 228 | 227 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
0) → ¬ 𝑖 =
3) |
| 229 | 228 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
0) → if(𝑖 = 3, 1, 0) =
0) |
| 230 | 147, 229,
157, 157 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(3 ↑ 𝑋))‘0) = 0) |
| 231 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑖 =
0) → 𝑖 =
0) |
| 232 | 231 | iftrued 4533 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑖 =
0) → if(𝑖 = 0, 2, 0) =
2) |
| 233 | 155, 232,
157, 169 | fvmptd 7023 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ ((coe1‘(𝐾‘2))‘0) = 2) |
| 234 | 230, 233 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)) =
(0(-g‘𝑄)2)) |
| 235 | 223, 234 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) =
(0(-g‘𝑄)2)) |
| 236 | | df-neg 11495 |
. . . . . . . . . . . . . . . 16
⊢ -2 = (0
− 2) |
| 237 | 36, 3, 132 | subgsub 19156 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℚ
∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2
∈ ℚ) → (0 − 2) = (0(-g‘𝑄)2)) |
| 238 | 136, 189,
65, 237 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (0 − 2) = (0(-g‘𝑄)2)) |
| 239 | 236, 238 | eqtr2id 2790 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (0(-g‘𝑄)2) = -2) |
| 240 | 221, 235,
239 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ -2 = ((coe1‘𝐹)‘0)) |
| 241 | 240 | mptru 1547 |
. . . . . . . . . . . . 13
⊢ -2 =
((coe1‘𝐹)‘0) |
| 242 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → 𝑄 ∈ Field) |
| 243 | 242 | fldcrngd 20742 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → 𝑄 ∈ CRing) |
| 244 | 100 | mptru 1547 |
. . . . . . . . . . . . . 14
⊢ 𝐹 ∈ (Base‘𝑃) |
| 245 | 244 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃)) |
| 246 | 130 | mptru 1547 |
. . . . . . . . . . . . . 14
⊢ (𝐷‘𝐹) = 3 |
| 247 | 246 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → (𝐷‘𝐹) = 3) |
| 248 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℚ) |
| 249 | 2, 91, 61, 34, 108, 111, 112, 113, 92, 166, 195, 220, 241, 243, 245, 247, 248 | evl1deg3 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) |
| 253 | 252, 6 | mgpbas 20142 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
| 254 | 251, 253 | ressbas2 17283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℚ
⊆ ℂ → ℚ =
(Base‘((mulGrp‘ℂfld) ↾s
ℚ))) |
| 255 | 250, 254 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℚ =
(Base‘((mulGrp‘ℂfld) ↾s
ℚ)) |
| 256 | 3, 252 | mgpress 20147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℂfld ∈ DivRing ∧ ℚ ∈
(SubRing‘ℂfld)) →
((mulGrp‘ℂfld) ↾s ℚ) =
(mulGrp‘𝑄)) |
| 257 | 7, 13, 256 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((mulGrp‘ℂfld) ↾s ℚ) =
(mulGrp‘𝑄) |
| 258 | 257 | fveq2i 6909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘((mulGrp‘ℂfld) ↾s
ℚ)) = (Base‘(mulGrp‘𝑄)) |
| 259 | 255, 258 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℚ =
(Base‘(mulGrp‘𝑄)) |
| 260 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) |
| 261 | 260 | ringmgp 20236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄 ∈ Ring →
(mulGrp‘𝑄) ∈
Mnd) |
| 262 | 56, 261 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℚ →
(mulGrp‘𝑄) ∈
Mnd) |
| 263 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℚ → 3 ∈
ℕ0) |
| 264 | 259, 112,
262, 263, 248 | mulgnn0cld 19113 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℚ →
(3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ) |
| 265 | 250, 264 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ →
(3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ) |
| 266 | 265 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ → (1
· (3(.g‘(mulGrp‘𝑄))𝑥)) =
(3(.g‘(mulGrp‘𝑄))𝑥)) |
| 267 | 257 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
⊢
(mulGrp‘𝑄) =
((mulGrp‘ℂfld) ↾s
ℚ) |
| 268 | 250, 253 | sseqtri 4032 |
. . . . . . . . . . . . . . . . . 18
⊢ ℚ
⊆ (Base‘(mulGrp‘ℂfld)) |
| 269 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ → ℚ
⊆ (Base‘(mulGrp‘ℂfld))) |
| 270 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ → 3 ∈
ℕ) |
| 271 | 267, 269,
248, 270 | ressmulgnnd 19096 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ →
(3(.g‘(mulGrp‘𝑄))𝑥) =
(3(.g‘(mulGrp‘ℂfld))𝑥)) |
| 272 | | qcn 13005 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℂ) |
| 273 | | cnfldexp 21417 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 3 ∈
ℕ0) →
(3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3)) |
| 274 | 272, 263,
273 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ →
(3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3)) |
| 275 | 266, 271,
274 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → (1
· (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3)) |
| 276 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℚ → 2 ∈
ℕ0) |
| 277 | 259, 112,
262, 276, 248 | mulgnn0cld 19113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ →
(2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ) |
| 278 | 250, 277 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ →
(2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ) |
| 279 | 278 | mul02d 11459 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → (0
· (2(.g‘(mulGrp‘𝑄))𝑥)) = 0) |
| 280 | 275, 279 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → ((1
· (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 ·
(2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0)) |
| 281 | 272, 263 | expcld 14186 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈
ℂ) |
| 282 | 281 | addridd 11461 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3)) |
| 283 | 280, 282 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → ((1
· (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 ·
(2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3)) |
| 284 | 272 | mul02d 11459 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → (0
· 𝑥) =
0) |
| 285 | 284 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → ((0
· 𝑥) + -2) = (0 +
-2)) |
| 286 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ → 2 ∈
ℂ) |
| 287 | 286 | negcld 11607 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → -2 ∈
ℂ) |
| 288 | 287 | addlidd 11462 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℚ → (0 + -2)
= -2) |
| 289 | 285, 288 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℚ → ((0
· 𝑥) + -2) =
-2) |
| 290 | 283, 289 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → (((1
· (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 ·
(2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2)) |
| 291 | 281, 286 | negsubd 11626 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) −
2)) |
| 292 | 249, 290,
291 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ →
(((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2)) |
| 293 | | 2prm 16729 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℙ |
| 294 | | 3z 12650 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℤ |
| 295 | | 3re 12346 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℝ |
| 296 | 172, 295,
173 | ltleii 11384 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≤
3 |
| 297 | 63 | eluz1i 12886 |
. . . . . . . . . . . . . . . 16
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤
3)) |
| 298 | 294, 296,
297 | mpbir2an 711 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
(ℤ≥‘2) |
| 299 | | rtprmirr 26803 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) →
(2↑𝑐(1 / 3)) ∈ (ℝ ∖
ℚ)) |
| 300 | 293, 298,
299 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
(2↑𝑐(1 / 3)) ∈ (ℝ ∖
ℚ) |
| 301 | | eldifn 4132 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
→ ¬ (2↑𝑐(1 / 3)) ∈
ℚ) |
| 302 | 300, 301 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ¬
(2↑𝑐(1 / 3)) ∈ ℚ |
| 303 | | nelne2 3040 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℚ ∧ ¬
(2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 /
3))) |
| 304 | 302, 303 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℚ → 𝑥 ≠
(2↑𝑐(1 / 3))) |
| 305 | | qre 12995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ → 𝑥 ∈
ℝ) |
| 306 | 305 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
𝑥 ∈
ℝ) |
| 307 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
| 308 | 281, 286 | subeq0ad 11630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔
(𝑥↑3) =
2)) |
| 309 | 308 | biimpa 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
(𝑥↑3) =
2) |
| 310 | 307, 309 | breqtrrid 5181 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
0 < (𝑥↑3)) |
| 311 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
3 ∈ ℕ) |
| 312 | | n2dvds3 16408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬ 2
∥ 3 |
| 313 | 312 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
¬ 2 ∥ 3) |
| 314 | 306, 311,
313 | expgt0b 32818 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
(0 < 𝑥 ↔ 0 <
(𝑥↑3))) |
| 315 | 310, 314 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
0 < 𝑥) |
| 316 | 306, 315 | elrpd 13074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
𝑥 ∈
ℝ+) |
| 317 | 295 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
3 ∈ ℝ) |
| 318 | 22 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
(1 / 3) ∈ ℂ) |
| 319 | 316, 317,
318 | cxpmuld 26779 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
(𝑥↑𝑐(3 · (1 /
3))) = ((𝑥↑𝑐3)↑𝑐(1
/ 3))) |
| 320 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℚ → 3 ∈
ℂ) |
| 321 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℚ → 3 ≠
0) |
| 322 | 320, 321 | recidd 12038 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℚ → (3
· (1 / 3)) = 1) |
| 323 | 322 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3
· (1 / 3))) = (𝑥↑𝑐1)) |
| 324 | 272 | cxp1d 26748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) =
𝑥) |
| 325 | 323, 324 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3
· (1 / 3))) = 𝑥) |
| 326 | 325 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
(𝑥↑𝑐(3 · (1 /
3))) = 𝑥) |
| 327 | | cxpexp 26710 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑥↑𝑐3) = (𝑥↑3)) |
| 328 | 272, 263,
327 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) =
(𝑥↑3)) |
| 329 | 328 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1
/ 3)) = ((𝑥↑3)↑𝑐(1 /
3))) |
| 330 | 329 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
((𝑥↑𝑐3)↑𝑐(1
/ 3)) = ((𝑥↑3)↑𝑐(1 /
3))) |
| 331 | 319, 326,
330 | 3eqtr3rd 2786 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
((𝑥↑3)↑𝑐(1 / 3)) =
𝑥) |
| 332 | 309 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
((𝑥↑3)↑𝑐(1 / 3)) =
(2↑𝑐(1 / 3))) |
| 333 | 331, 332 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) →
𝑥 =
(2↑𝑐(1 / 3))) |
| 334 | 304, 333 | mteqand 3033 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠
0) |
| 335 | 292, 334 | eqnetrd 3008 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℚ →
(((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0) |
| 336 | 335 | neneqd 2945 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℚ → ¬
(((eval1‘𝑄)‘𝐹)‘𝑥) = 0) |
| 337 | 336 | rgen 3063 |
. . . . . . . 8
⊢
∀𝑥 ∈
ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0 |
| 338 | 337 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ∀𝑥 ∈
ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0) |
| 339 | | rabeq0 4388 |
. . . . . . 7
⊢ ({𝑥 ∈ ℚ ∣
(((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬
(((eval1‘𝑄)‘𝐹)‘𝑥) = 0) |
| 340 | 338, 339 | sylibr 234 |
. . . . . 6
⊢ (⊤
→ {𝑥 ∈ ℚ
∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅) |
| 341 | 105, 340 | eqtrd 2777 |
. . . . 5
⊢ (⊤
→ (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅) |
| 342 | 90, 91, 92, 2, 34, 96, 100, 341, 130 | ply1dg3rt0irred 33607 |
. . . 4
⊢ (⊤
→ 𝐹 ∈
(Irred‘𝑃)) |
| 343 | | eqid 2737 |
. . . . . . 7
⊢
(Irred‘𝑃) =
(Irred‘𝑃) |
| 344 | 343, 29 | irredn0 20423 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃)) |
| 345 | 46, 342, 344 | syl2anc 584 |
. . . . 5
⊢ (⊤
→ 𝐹 ≠
(0g‘𝑃)) |
| 346 | 3 | fveq2i 6909 |
. . . . . . 7
⊢
(deg1‘𝑄) =
(deg1‘(ℂfld ↾s
ℚ)) |
| 347 | 92, 346 | eqtri 2765 |
. . . . . 6
⊢ 𝐷 =
(deg1‘(ℂfld ↾s
ℚ)) |
| 348 | | eqid 2737 |
. . . . . 6
⊢
(Monic1p‘(ℂfld ↾s
ℚ)) = (Monic1p‘(ℂfld
↾s ℚ)) |
| 349 | | eqid 2737 |
. . . . . . 7
⊢
(ℂfld ↾s ℚ) =
(ℂfld ↾s ℚ) |
| 350 | 349 | qrng1 27666 |
. . . . . 6
⊢ 1 =
(1r‘(ℂfld ↾s
ℚ)) |
| 351 | 5, 34, 29, 347, 348, 350 | ismon1p 26182 |
. . . . 5
⊢ (𝐹 ∈
(Monic1p‘(ℂfld ↾s ℚ))
↔ (𝐹 ∈
(Base‘𝑃) ∧ 𝐹 ≠ (0g‘𝑃) ∧
((coe1‘𝐹)‘(𝐷‘𝐹)) = 1)) |
| 352 | 100, 345,
163, 351 | syl3anbrc 1344 |
. . . 4
⊢ (⊤
→ 𝐹 ∈
(Monic1p‘(ℂfld ↾s
ℚ))) |
| 353 | 1, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352 | irredminply 33757 |
. . 3
⊢ (⊤
→ 𝐹 = (𝑀‘𝐴)) |
| 354 | 353, 130 | jca 511 |
. 2
⊢ (⊤
→ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)) |
| 355 | 354 | mptru 1547 |
1
⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3) |