Proof of Theorem 1cubrlem
| Step | Hyp | Ref
| Expression |
| 1 | | neg1cn 12380 |
. . . 4
⊢ -1 ∈
ℂ |
| 2 | | neg1ne0 12382 |
. . . 4
⊢ -1 ≠
0 |
| 3 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 4 | | 3nn 12345 |
. . . . . 6
⊢ 3 ∈
ℕ |
| 5 | | nndivre 12307 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ 3 ∈ ℕ) → (2 / 3) ∈
ℝ) |
| 6 | 3, 4, 5 | mp2an 692 |
. . . . 5
⊢ (2 / 3)
∈ ℝ |
| 7 | 6 | recni 11275 |
. . . 4
⊢ (2 / 3)
∈ ℂ |
| 8 | | cxpef 26707 |
. . . 4
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ (2 / 3) ∈ ℂ) →
(-1↑𝑐(2 / 3)) = (exp‘((2 / 3) ·
(log‘-1)))) |
| 9 | 1, 2, 7, 8 | mp3an 1463 |
. . 3
⊢
(-1↑𝑐(2 / 3)) = (exp‘((2 / 3) ·
(log‘-1))) |
| 10 | | logm1 26631 |
. . . . . 6
⊢
(log‘-1) = (i · π) |
| 11 | 10 | oveq2i 7442 |
. . . . 5
⊢ ((2 / 3)
· (log‘-1)) = ((2 / 3) · (i ·
π)) |
| 12 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 13 | | pire 26500 |
. . . . . . 7
⊢ π
∈ ℝ |
| 14 | 13 | recni 11275 |
. . . . . 6
⊢ π
∈ ℂ |
| 15 | 7, 12, 14 | mul12i 11456 |
. . . . 5
⊢ ((2 / 3)
· (i · π)) = (i · ((2 / 3) ·
π)) |
| 16 | 11, 15 | eqtri 2765 |
. . . 4
⊢ ((2 / 3)
· (log‘-1)) = (i · ((2 / 3) ·
π)) |
| 17 | 16 | fveq2i 6909 |
. . 3
⊢
(exp‘((2 / 3) · (log‘-1))) = (exp‘(i ·
((2 / 3) · π))) |
| 18 | | 6nn 12355 |
. . . . . . . . 9
⊢ 6 ∈
ℕ |
| 19 | | nndivre 12307 |
. . . . . . . . 9
⊢ ((π
∈ ℝ ∧ 6 ∈ ℕ) → (π / 6) ∈
ℝ) |
| 20 | 13, 18, 19 | mp2an 692 |
. . . . . . . 8
⊢ (π /
6) ∈ ℝ |
| 21 | 20 | recni 11275 |
. . . . . . 7
⊢ (π /
6) ∈ ℂ |
| 22 | | coshalfpip 26536 |
. . . . . . 7
⊢ ((π /
6) ∈ ℂ → (cos‘((π / 2) + (π / 6))) =
-(sin‘(π / 6))) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . 6
⊢
(cos‘((π / 2) + (π / 6))) = -(sin‘(π /
6)) |
| 24 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 25 | | 2ne0 12370 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
| 26 | | divrec2 11939 |
. . . . . . . . . 10
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (π / 2) = ((1 /
2) · π)) |
| 27 | 14, 24, 25, 26 | mp3an 1463 |
. . . . . . . . 9
⊢ (π /
2) = ((1 / 2) · π) |
| 28 | | 6cn 12357 |
. . . . . . . . . 10
⊢ 6 ∈
ℂ |
| 29 | 18 | nnne0i 12306 |
. . . . . . . . . 10
⊢ 6 ≠
0 |
| 30 | | divrec2 11939 |
. . . . . . . . . 10
⊢ ((π
∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → (π / 6) = ((1 /
6) · π)) |
| 31 | 14, 28, 29, 30 | mp3an 1463 |
. . . . . . . . 9
⊢ (π /
6) = ((1 / 6) · π) |
| 32 | 27, 31 | oveq12i 7443 |
. . . . . . . 8
⊢ ((π /
2) + (π / 6)) = (((1 / 2) · π) + ((1 / 6) ·
π)) |
| 33 | 24, 25 | reccli 11997 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℂ |
| 34 | 28, 29 | reccli 11997 |
. . . . . . . . 9
⊢ (1 / 6)
∈ ℂ |
| 35 | 33, 34, 14 | adddiri 11274 |
. . . . . . . 8
⊢ (((1 / 2)
+ (1 / 6)) · π) = (((1 / 2) · π) + ((1 / 6) ·
π)) |
| 36 | | halfpm6th 12487 |
. . . . . . . . . 10
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |
| 37 | 36 | simpri 485 |
. . . . . . . . 9
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
| 38 | 37 | oveq1i 7441 |
. . . . . . . 8
⊢ (((1 / 2)
+ (1 / 6)) · π) = ((2 / 3) · π) |
| 39 | 32, 35, 38 | 3eqtr2i 2771 |
. . . . . . 7
⊢ ((π /
2) + (π / 6)) = ((2 / 3) · π) |
| 40 | 39 | fveq2i 6909 |
. . . . . 6
⊢
(cos‘((π / 2) + (π / 6))) = (cos‘((2 / 3) ·
π)) |
| 41 | | sincos6thpi 26558 |
. . . . . . . . 9
⊢
((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) =
((√‘3) / 2)) |
| 42 | 41 | simpli 483 |
. . . . . . . 8
⊢
(sin‘(π / 6)) = (1 / 2) |
| 43 | 42 | negeqi 11501 |
. . . . . . 7
⊢
-(sin‘(π / 6)) = -(1 / 2) |
| 44 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 45 | | divneg 11959 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 /
2)) |
| 46 | 44, 24, 25, 45 | mp3an 1463 |
. . . . . . 7
⊢ -(1 / 2)
= (-1 / 2) |
| 47 | 43, 46 | eqtri 2765 |
. . . . . 6
⊢
-(sin‘(π / 6)) = (-1 / 2) |
| 48 | 23, 40, 47 | 3eqtr3i 2773 |
. . . . 5
⊢
(cos‘((2 / 3) · π)) = (-1 / 2) |
| 49 | | sinhalfpip 26534 |
. . . . . . . . 9
⊢ ((π /
6) ∈ ℂ → (sin‘((π / 2) + (π / 6))) =
(cos‘(π / 6))) |
| 50 | 21, 49 | ax-mp 5 |
. . . . . . . 8
⊢
(sin‘((π / 2) + (π / 6))) = (cos‘(π /
6)) |
| 51 | 39 | fveq2i 6909 |
. . . . . . . 8
⊢
(sin‘((π / 2) + (π / 6))) = (sin‘((2 / 3) ·
π)) |
| 52 | 41 | simpri 485 |
. . . . . . . 8
⊢
(cos‘(π / 6)) = ((√‘3) / 2) |
| 53 | 50, 51, 52 | 3eqtr3i 2773 |
. . . . . . 7
⊢
(sin‘((2 / 3) · π)) = ((√‘3) /
2) |
| 54 | 53 | oveq2i 7442 |
. . . . . 6
⊢ (i
· (sin‘((2 / 3) · π))) = (i · ((√‘3)
/ 2)) |
| 55 | | 3re 12346 |
. . . . . . . . 9
⊢ 3 ∈
ℝ |
| 56 | | 3nn0 12544 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
| 57 | 56 | nn0ge0i 12553 |
. . . . . . . . 9
⊢ 0 ≤
3 |
| 58 | | resqrtcl 15292 |
. . . . . . . . 9
⊢ ((3
∈ ℝ ∧ 0 ≤ 3) → (√‘3) ∈
ℝ) |
| 59 | 55, 57, 58 | mp2an 692 |
. . . . . . . 8
⊢
(√‘3) ∈ ℝ |
| 60 | 59 | recni 11275 |
. . . . . . 7
⊢
(√‘3) ∈ ℂ |
| 61 | 12, 60, 24, 25 | divassi 12023 |
. . . . . 6
⊢ ((i
· (√‘3)) / 2) = (i · ((√‘3) /
2)) |
| 62 | 54, 61 | eqtr4i 2768 |
. . . . 5
⊢ (i
· (sin‘((2 / 3) · π))) = ((i · (√‘3))
/ 2) |
| 63 | 48, 62 | oveq12i 7443 |
. . . 4
⊢
((cos‘((2 / 3) · π)) + (i · (sin‘((2 / 3)
· π)))) = ((-1 / 2) + ((i · (√‘3)) /
2)) |
| 64 | 7, 14 | mulcli 11268 |
. . . . 5
⊢ ((2 / 3)
· π) ∈ ℂ |
| 65 | | efival 16188 |
. . . . 5
⊢ (((2 / 3)
· π) ∈ ℂ → (exp‘(i · ((2 / 3) ·
π))) = ((cos‘((2 / 3) · π)) + (i · (sin‘((2 /
3) · π))))) |
| 66 | 64, 65 | ax-mp 5 |
. . . 4
⊢
(exp‘(i · ((2 / 3) · π))) = ((cos‘((2 / 3)
· π)) + (i · (sin‘((2 / 3) ·
π)))) |
| 67 | 12, 60 | mulcli 11268 |
. . . . 5
⊢ (i
· (√‘3)) ∈ ℂ |
| 68 | 1, 67, 24, 25 | divdiri 12024 |
. . . 4
⊢ ((-1 + (i
· (√‘3))) / 2) = ((-1 / 2) + ((i · (√‘3))
/ 2)) |
| 69 | 63, 66, 68 | 3eqtr4i 2775 |
. . 3
⊢
(exp‘(i · ((2 / 3) · π))) = ((-1 + (i ·
(√‘3))) / 2) |
| 70 | 9, 17, 69 | 3eqtri 2769 |
. 2
⊢
(-1↑𝑐(2 / 3)) = ((-1 + (i ·
(√‘3))) / 2) |
| 71 | | 1z 12647 |
. . . 4
⊢ 1 ∈
ℤ |
| 72 | | root1cj 26799 |
. . . 4
⊢ ((3
∈ ℕ ∧ 1 ∈ ℤ) →
(∗‘((-1↑𝑐(2 / 3))↑1)) =
((-1↑𝑐(2 / 3))↑(3 − 1))) |
| 73 | 4, 71, 72 | mp2an 692 |
. . 3
⊢
(∗‘((-1↑𝑐(2 / 3))↑1)) =
((-1↑𝑐(2 / 3))↑(3 − 1)) |
| 74 | | cxpcl 26716 |
. . . . . . . 8
⊢ ((-1
∈ ℂ ∧ (2 / 3) ∈ ℂ) →
(-1↑𝑐(2 / 3)) ∈ ℂ) |
| 75 | 1, 7, 74 | mp2an 692 |
. . . . . . 7
⊢
(-1↑𝑐(2 / 3)) ∈ ℂ |
| 76 | | exp1 14108 |
. . . . . . 7
⊢
((-1↑𝑐(2 / 3)) ∈ ℂ →
((-1↑𝑐(2 / 3))↑1) =
(-1↑𝑐(2 / 3))) |
| 77 | 75, 76 | ax-mp 5 |
. . . . . 6
⊢
((-1↑𝑐(2 / 3))↑1) =
(-1↑𝑐(2 / 3)) |
| 78 | 77, 70 | eqtri 2765 |
. . . . 5
⊢
((-1↑𝑐(2 / 3))↑1) = ((-1 + (i ·
(√‘3))) / 2) |
| 79 | 78 | fveq2i 6909 |
. . . 4
⊢
(∗‘((-1↑𝑐(2 / 3))↑1)) =
(∗‘((-1 + (i · (√‘3))) / 2)) |
| 80 | 1, 67 | addcli 11267 |
. . . . . 6
⊢ (-1 + (i
· (√‘3))) ∈ ℂ |
| 81 | 80, 24 | cjdivi 15230 |
. . . . 5
⊢ (2 ≠ 0
→ (∗‘((-1 + (i · (√‘3))) / 2)) =
((∗‘(-1 + (i · (√‘3)))) /
(∗‘2))) |
| 82 | 25, 81 | ax-mp 5 |
. . . 4
⊢
(∗‘((-1 + (i · (√‘3))) / 2)) =
((∗‘(-1 + (i · (√‘3)))) /
(∗‘2)) |
| 83 | 1, 67 | cjaddi 15227 |
. . . . . 6
⊢
(∗‘(-1 + (i · (√‘3)))) =
((∗‘-1) + (∗‘(i ·
(√‘3)))) |
| 84 | | neg1rr 12381 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
| 85 | | cjre 15178 |
. . . . . . . 8
⊢ (-1
∈ ℝ → (∗‘-1) = -1) |
| 86 | 84, 85 | ax-mp 5 |
. . . . . . 7
⊢
(∗‘-1) = -1 |
| 87 | 12, 60 | cjmuli 15228 |
. . . . . . . 8
⊢
(∗‘(i · (√‘3))) = ((∗‘i)
· (∗‘(√‘3))) |
| 88 | | cji 15198 |
. . . . . . . . 9
⊢
(∗‘i) = -i |
| 89 | | cjre 15178 |
. . . . . . . . . 10
⊢
((√‘3) ∈ ℝ →
(∗‘(√‘3)) = (√‘3)) |
| 90 | 59, 89 | ax-mp 5 |
. . . . . . . . 9
⊢
(∗‘(√‘3)) = (√‘3) |
| 91 | 88, 90 | oveq12i 7443 |
. . . . . . . 8
⊢
((∗‘i) · (∗‘(√‘3))) = (-i
· (√‘3)) |
| 92 | 12, 60 | mulneg1i 11709 |
. . . . . . . 8
⊢ (-i
· (√‘3)) = -(i · (√‘3)) |
| 93 | 87, 91, 92 | 3eqtri 2769 |
. . . . . . 7
⊢
(∗‘(i · (√‘3))) = -(i ·
(√‘3)) |
| 94 | 86, 93 | oveq12i 7443 |
. . . . . 6
⊢
((∗‘-1) + (∗‘(i · (√‘3))))
= (-1 + -(i · (√‘3))) |
| 95 | 1, 67 | negsubi 11587 |
. . . . . 6
⊢ (-1 + -(i
· (√‘3))) = (-1 − (i ·
(√‘3))) |
| 96 | 83, 94, 95 | 3eqtri 2769 |
. . . . 5
⊢
(∗‘(-1 + (i · (√‘3)))) = (-1 − (i
· (√‘3))) |
| 97 | | cjre 15178 |
. . . . . 6
⊢ (2 ∈
ℝ → (∗‘2) = 2) |
| 98 | 3, 97 | ax-mp 5 |
. . . . 5
⊢
(∗‘2) = 2 |
| 99 | 96, 98 | oveq12i 7443 |
. . . 4
⊢
((∗‘(-1 + (i · (√‘3)))) /
(∗‘2)) = ((-1 − (i · (√‘3))) /
2) |
| 100 | 79, 82, 99 | 3eqtri 2769 |
. . 3
⊢
(∗‘((-1↑𝑐(2 / 3))↑1)) = ((-1
− (i · (√‘3))) / 2) |
| 101 | | 3m1e2 12394 |
. . . 4
⊢ (3
− 1) = 2 |
| 102 | 101 | oveq2i 7442 |
. . 3
⊢
((-1↑𝑐(2 / 3))↑(3 − 1)) =
((-1↑𝑐(2 / 3))↑2) |
| 103 | 73, 100, 102 | 3eqtr3ri 2774 |
. 2
⊢
((-1↑𝑐(2 / 3))↑2) = ((-1 − (i
· (√‘3))) / 2) |
| 104 | 70, 103 | pm3.2i 470 |
1
⊢
((-1↑𝑐(2 / 3)) = ((-1 + (i ·
(√‘3))) / 2) ∧ ((-1↑𝑐(2 / 3))↑2) =
((-1 − (i · (√‘3))) / 2)) |