Proof of Theorem sincos6thpi
| Step | Hyp | Ref
| Expression |
| 1 | | 2cn 12341 |
. . 3
⊢ 2 ∈
ℂ |
| 2 | | pire 26500 |
. . . . . 6
⊢ π
∈ ℝ |
| 3 | | 6re 12356 |
. . . . . 6
⊢ 6 ∈
ℝ |
| 4 | | 6pos 12376 |
. . . . . . 7
⊢ 0 <
6 |
| 5 | 3, 4 | gt0ne0ii 11799 |
. . . . . 6
⊢ 6 ≠
0 |
| 6 | 2, 3, 5 | redivcli 12034 |
. . . . 5
⊢ (π /
6) ∈ ℝ |
| 7 | 6 | recni 11275 |
. . . 4
⊢ (π /
6) ∈ ℂ |
| 8 | | sincl 16162 |
. . . 4
⊢ ((π /
6) ∈ ℂ → (sin‘(π / 6)) ∈
ℂ) |
| 9 | 7, 8 | ax-mp 5 |
. . 3
⊢
(sin‘(π / 6)) ∈ ℂ |
| 10 | | 2ne0 12370 |
. . 3
⊢ 2 ≠
0 |
| 11 | | recoscl 16177 |
. . . . . . . . . 10
⊢ ((π /
6) ∈ ℝ → (cos‘(π / 6)) ∈
ℝ) |
| 12 | 6, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(cos‘(π / 6)) ∈ ℝ |
| 13 | 12 | recni 11275 |
. . . . . . . 8
⊢
(cos‘(π / 6)) ∈ ℂ |
| 14 | 1, 9, 13 | mulassi 11272 |
. . . . . . 7
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (2 ·
((sin‘(π / 6)) · (cos‘(π / 6)))) |
| 15 | | sin2t 16213 |
. . . . . . . 8
⊢ ((π /
6) ∈ ℂ → (sin‘(2 · (π / 6))) = (2 ·
((sin‘(π / 6)) · (cos‘(π / 6))))) |
| 16 | 7, 15 | ax-mp 5 |
. . . . . . 7
⊢
(sin‘(2 · (π / 6))) = (2 · ((sin‘(π /
6)) · (cos‘(π / 6)))) |
| 17 | 14, 16 | eqtr4i 2768 |
. . . . . 6
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) =
(sin‘(2 · (π / 6))) |
| 18 | | 3cn 12347 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
| 19 | | 3ne0 12372 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
| 20 | 1, 18, 19 | divcli 12009 |
. . . . . . . . 9
⊢ (2 / 3)
∈ ℂ |
| 21 | 18, 19 | reccli 11997 |
. . . . . . . . 9
⊢ (1 / 3)
∈ ℂ |
| 22 | | df-3 12330 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
| 23 | 22 | oveq1i 7441 |
. . . . . . . . . 10
⊢ (3 / 3) =
((2 + 1) / 3) |
| 24 | 18, 19 | dividi 12000 |
. . . . . . . . . 10
⊢ (3 / 3) =
1 |
| 25 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 26 | 1, 25, 18, 19 | divdiri 12024 |
. . . . . . . . . 10
⊢ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) |
| 27 | 23, 24, 26 | 3eqtr3ri 2774 |
. . . . . . . . 9
⊢ ((2 / 3)
+ (1 / 3)) = 1 |
| 28 | | sincosq1eq 26554 |
. . . . . . . . 9
⊢ (((2 / 3)
∈ ℂ ∧ (1 / 3) ∈ ℂ ∧ ((2 / 3) + (1 / 3)) = 1)
→ (sin‘((2 / 3) · (π / 2))) = (cos‘((1 / 3) ·
(π / 2)))) |
| 29 | 20, 21, 27, 28 | mp3an 1463 |
. . . . . . . 8
⊢
(sin‘((2 / 3) · (π / 2))) = (cos‘((1 / 3) ·
(π / 2))) |
| 30 | | picn 26501 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
| 31 | 1, 18, 30, 1, 19, 10 | divmuldivi 12027 |
. . . . . . . . . 10
⊢ ((2 / 3)
· (π / 2)) = ((2 · π) / (3 · 2)) |
| 32 | | 3t2e6 12432 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
| 33 | 32 | oveq2i 7442 |
. . . . . . . . . 10
⊢ ((2
· π) / (3 · 2)) = ((2 · π) / 6) |
| 34 | | 6cn 12357 |
. . . . . . . . . . 11
⊢ 6 ∈
ℂ |
| 35 | 1, 30, 34, 5 | divassi 12023 |
. . . . . . . . . 10
⊢ ((2
· π) / 6) = (2 · (π / 6)) |
| 36 | 31, 33, 35 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((2 / 3)
· (π / 2)) = (2 · (π / 6)) |
| 37 | 36 | fveq2i 6909 |
. . . . . . . 8
⊢
(sin‘((2 / 3) · (π / 2))) = (sin‘(2 · (π
/ 6))) |
| 38 | 29, 37 | eqtr3i 2767 |
. . . . . . 7
⊢
(cos‘((1 / 3) · (π / 2))) = (sin‘(2 · (π
/ 6))) |
| 39 | 25, 18, 30, 1, 19, 10 | divmuldivi 12027 |
. . . . . . . . 9
⊢ ((1 / 3)
· (π / 2)) = ((1 · π) / (3 · 2)) |
| 40 | 30 | mullidi 11266 |
. . . . . . . . . 10
⊢ (1
· π) = π |
| 41 | 40, 32 | oveq12i 7443 |
. . . . . . . . 9
⊢ ((1
· π) / (3 · 2)) = (π / 6) |
| 42 | 39, 41 | eqtri 2765 |
. . . . . . . 8
⊢ ((1 / 3)
· (π / 2)) = (π / 6) |
| 43 | 42 | fveq2i 6909 |
. . . . . . 7
⊢
(cos‘((1 / 3) · (π / 2))) = (cos‘(π /
6)) |
| 44 | 38, 43 | eqtr3i 2767 |
. . . . . 6
⊢
(sin‘(2 · (π / 6))) = (cos‘(π /
6)) |
| 45 | 17, 44 | eqtri 2765 |
. . . . 5
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) =
(cos‘(π / 6)) |
| 46 | 13 | mullidi 11266 |
. . . . 5
⊢ (1
· (cos‘(π / 6))) = (cos‘(π / 6)) |
| 47 | 45, 46 | eqtr4i 2768 |
. . . 4
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (1 ·
(cos‘(π / 6))) |
| 48 | 1, 9 | mulcli 11268 |
. . . . 5
⊢ (2
· (sin‘(π / 6))) ∈ ℂ |
| 49 | | pipos 26502 |
. . . . . . . . . . 11
⊢ 0 <
π |
| 50 | 2, 3, 49, 4 | divgt0ii 12185 |
. . . . . . . . . 10
⊢ 0 <
(π / 6) |
| 51 | | 2lt6 12450 |
. . . . . . . . . . 11
⊢ 2 <
6 |
| 52 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 53 | | 2pos 12369 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
| 54 | 52, 53 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 55 | 3, 4 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (6 ∈
ℝ ∧ 0 < 6) |
| 56 | 2, 49 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (π
∈ ℝ ∧ 0 < π) |
| 57 | | ltdiv2 12154 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℝ ∧ 0 < 2) ∧ (6 ∈ ℝ ∧ 0 < 6) ∧
(π ∈ ℝ ∧ 0 < π)) → (2 < 6 ↔ (π / 6)
< (π / 2))) |
| 58 | 54, 55, 56, 57 | mp3an 1463 |
. . . . . . . . . . 11
⊢ (2 < 6
↔ (π / 6) < (π / 2)) |
| 59 | 51, 58 | mpbi 230 |
. . . . . . . . . 10
⊢ (π /
6) < (π / 2) |
| 60 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 61 | | halfpire 26506 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℝ |
| 62 | | rexr 11307 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ → 0 ∈ ℝ*) |
| 63 | | rexr 11307 |
. . . . . . . . . . . 12
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
| 64 | | elioo2 13428 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
((π / 6) ∈ (0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0
< (π / 6) ∧ (π / 6) < (π / 2)))) |
| 65 | 62, 63, 64 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ) → ((π / 6) ∈
(0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6)
∧ (π / 6) < (π / 2)))) |
| 66 | 60, 61, 65 | mp2an 692 |
. . . . . . . . . 10
⊢ ((π /
6) ∈ (0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π
/ 6) ∧ (π / 6) < (π / 2))) |
| 67 | 6, 50, 59, 66 | mpbir3an 1342 |
. . . . . . . . 9
⊢ (π /
6) ∈ (0(,)(π / 2)) |
| 68 | | sincosq1sgn 26540 |
. . . . . . . . 9
⊢ ((π /
6) ∈ (0(,)(π / 2)) → (0 < (sin‘(π / 6)) ∧ 0 <
(cos‘(π / 6)))) |
| 69 | 67, 68 | ax-mp 5 |
. . . . . . . 8
⊢ (0 <
(sin‘(π / 6)) ∧ 0 < (cos‘(π / 6))) |
| 70 | 69 | simpri 485 |
. . . . . . 7
⊢ 0 <
(cos‘(π / 6)) |
| 71 | 12, 70 | gt0ne0ii 11799 |
. . . . . 6
⊢
(cos‘(π / 6)) ≠ 0 |
| 72 | 13, 71 | pm3.2i 470 |
. . . . 5
⊢
((cos‘(π / 6)) ∈ ℂ ∧ (cos‘(π / 6)) ≠
0) |
| 73 | | mulcan2 11901 |
. . . . 5
⊢ (((2
· (sin‘(π / 6))) ∈ ℂ ∧ 1 ∈ ℂ ∧
((cos‘(π / 6)) ∈ ℂ ∧ (cos‘(π / 6)) ≠ 0))
→ (((2 · (sin‘(π / 6))) · (cos‘(π / 6))) =
(1 · (cos‘(π / 6))) ↔ (2 · (sin‘(π / 6)))
= 1)) |
| 74 | 48, 25, 72, 73 | mp3an 1463 |
. . . 4
⊢ (((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (1 ·
(cos‘(π / 6))) ↔ (2 · (sin‘(π / 6))) =
1) |
| 75 | 47, 74 | mpbi 230 |
. . 3
⊢ (2
· (sin‘(π / 6))) = 1 |
| 76 | 1, 9, 10, 75 | mvllmuli 12100 |
. 2
⊢
(sin‘(π / 6)) = (1 / 2) |
| 77 | | 3re 12346 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
| 78 | | 3pos 12371 |
. . . . . . . 8
⊢ 0 <
3 |
| 79 | 77, 78 | sqrtpclii 15421 |
. . . . . . 7
⊢
(√‘3) ∈ ℝ |
| 80 | 79 | recni 11275 |
. . . . . 6
⊢
(√‘3) ∈ ℂ |
| 81 | 80, 1, 10 | sqdivi 14224 |
. . . . 5
⊢
(((√‘3) / 2)↑2) = (((√‘3)↑2) /
(2↑2)) |
| 82 | 60, 77, 78 | ltleii 11384 |
. . . . . . 7
⊢ 0 ≤
3 |
| 83 | 77 | sqsqrti 15414 |
. . . . . . 7
⊢ (0 ≤ 3
→ ((√‘3)↑2) = 3) |
| 84 | 82, 83 | ax-mp 5 |
. . . . . 6
⊢
((√‘3)↑2) = 3 |
| 85 | | sq2 14236 |
. . . . . 6
⊢
(2↑2) = 4 |
| 86 | 84, 85 | oveq12i 7443 |
. . . . 5
⊢
(((√‘3)↑2) / (2↑2)) = (3 / 4) |
| 87 | 81, 86 | eqtri 2765 |
. . . 4
⊢
(((√‘3) / 2)↑2) = (3 / 4) |
| 88 | 87 | fveq2i 6909 |
. . 3
⊢
(√‘(((√‘3) / 2)↑2)) = (√‘(3 /
4)) |
| 89 | 77 | sqrtge0i 15415 |
. . . . . 6
⊢ (0 ≤ 3
→ 0 ≤ (√‘3)) |
| 90 | 82, 89 | ax-mp 5 |
. . . . 5
⊢ 0 ≤
(√‘3) |
| 91 | 79, 52 | divge0i 12177 |
. . . . 5
⊢ ((0 ≤
(√‘3) ∧ 0 < 2) → 0 ≤ ((√‘3) /
2)) |
| 92 | 90, 53, 91 | mp2an 692 |
. . . 4
⊢ 0 ≤
((√‘3) / 2) |
| 93 | 79, 52, 10 | redivcli 12034 |
. . . . 5
⊢
((√‘3) / 2) ∈ ℝ |
| 94 | 93 | sqrtsqi 15413 |
. . . 4
⊢ (0 ≤
((√‘3) / 2) → (√‘(((√‘3) / 2)↑2))
= ((√‘3) / 2)) |
| 95 | 92, 94 | ax-mp 5 |
. . 3
⊢
(√‘(((√‘3) / 2)↑2)) = ((√‘3) /
2) |
| 96 | | 4cn 12351 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
| 97 | | 4ne0 12374 |
. . . . . . . 8
⊢ 4 ≠
0 |
| 98 | 96, 97 | dividi 12000 |
. . . . . . 7
⊢ (4 / 4) =
1 |
| 99 | 98 | oveq1i 7441 |
. . . . . 6
⊢ ((4 / 4)
− (1 / 4)) = (1 − (1 / 4)) |
| 100 | 96, 97 | pm3.2i 470 |
. . . . . . . 8
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
| 101 | | divsubdir 11961 |
. . . . . . . 8
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0))
→ ((4 − 1) / 4) = ((4 / 4) − (1 / 4))) |
| 102 | 96, 25, 100, 101 | mp3an 1463 |
. . . . . . 7
⊢ ((4
− 1) / 4) = ((4 / 4) − (1 / 4)) |
| 103 | | 4m1e3 12395 |
. . . . . . . 8
⊢ (4
− 1) = 3 |
| 104 | 103 | oveq1i 7441 |
. . . . . . 7
⊢ ((4
− 1) / 4) = (3 / 4) |
| 105 | 102, 104 | eqtr3i 2767 |
. . . . . 6
⊢ ((4 / 4)
− (1 / 4)) = (3 / 4) |
| 106 | 96, 97 | reccli 11997 |
. . . . . . 7
⊢ (1 / 4)
∈ ℂ |
| 107 | 13 | sqcli 14220 |
. . . . . . 7
⊢
((cos‘(π / 6))↑2) ∈ ℂ |
| 108 | 76 | oveq1i 7441 |
. . . . . . . . . 10
⊢
((sin‘(π / 6))↑2) = ((1 / 2)↑2) |
| 109 | 1, 10 | sqrecii 14222 |
. . . . . . . . . 10
⊢ ((1 /
2)↑2) = (1 / (2↑2)) |
| 110 | 85 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (1 /
(2↑2)) = (1 / 4) |
| 111 | 108, 109,
110 | 3eqtri 2769 |
. . . . . . . . 9
⊢
((sin‘(π / 6))↑2) = (1 / 4) |
| 112 | 111 | oveq1i 7441 |
. . . . . . . 8
⊢
(((sin‘(π / 6))↑2) + ((cos‘(π / 6))↑2)) =
((1 / 4) + ((cos‘(π / 6))↑2)) |
| 113 | | sincossq 16212 |
. . . . . . . . 9
⊢ ((π /
6) ∈ ℂ → (((sin‘(π / 6))↑2) + ((cos‘(π /
6))↑2)) = 1) |
| 114 | 7, 113 | ax-mp 5 |
. . . . . . . 8
⊢
(((sin‘(π / 6))↑2) + ((cos‘(π / 6))↑2)) =
1 |
| 115 | 112, 114 | eqtr3i 2767 |
. . . . . . 7
⊢ ((1 / 4)
+ ((cos‘(π / 6))↑2)) = 1 |
| 116 | 25, 106, 107, 115 | subaddrii 11598 |
. . . . . 6
⊢ (1
− (1 / 4)) = ((cos‘(π / 6))↑2) |
| 117 | 99, 105, 116 | 3eqtr3ri 2774 |
. . . . 5
⊢
((cos‘(π / 6))↑2) = (3 / 4) |
| 118 | 117 | fveq2i 6909 |
. . . 4
⊢
(√‘((cos‘(π / 6))↑2)) = (√‘(3 /
4)) |
| 119 | 60, 12, 70 | ltleii 11384 |
. . . . 5
⊢ 0 ≤
(cos‘(π / 6)) |
| 120 | 12 | sqrtsqi 15413 |
. . . . 5
⊢ (0 ≤
(cos‘(π / 6)) → (√‘((cos‘(π / 6))↑2)) =
(cos‘(π / 6))) |
| 121 | 119, 120 | ax-mp 5 |
. . . 4
⊢
(√‘((cos‘(π / 6))↑2)) = (cos‘(π /
6)) |
| 122 | 118, 121 | eqtr3i 2767 |
. . 3
⊢
(√‘(3 / 4)) = (cos‘(π / 6)) |
| 123 | 88, 95, 122 | 3eqtr3ri 2774 |
. 2
⊢
(cos‘(π / 6)) = ((√‘3) / 2) |
| 124 | 76, 123 | pm3.2i 470 |
1
⊢
((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) =
((√‘3) / 2)) |