Proof of Theorem sincos6thpi
Step | Hyp | Ref
| Expression |
1 | | 2cn 11091 |
. . 3
⊢ 2 ∈
ℂ |
2 | | pire 24210 |
. . . . . 6
⊢ π
∈ ℝ |
3 | | 6re 11101 |
. . . . . 6
⊢ 6 ∈
ℝ |
4 | | 6pos 11119 |
. . . . . . 7
⊢ 0 <
6 |
5 | 3, 4 | gt0ne0ii 10564 |
. . . . . 6
⊢ 6 ≠
0 |
6 | 2, 3, 5 | redivcli 10792 |
. . . . 5
⊢ (π /
6) ∈ ℝ |
7 | 6 | recni 10052 |
. . . 4
⊢ (π /
6) ∈ ℂ |
8 | | sincl 14856 |
. . . 4
⊢ ((π /
6) ∈ ℂ → (sin‘(π / 6)) ∈
ℂ) |
9 | 7, 8 | ax-mp 5 |
. . 3
⊢
(sin‘(π / 6)) ∈ ℂ |
10 | | 2ne0 11113 |
. . 3
⊢ 2 ≠
0 |
11 | | recoscl 14871 |
. . . . . . . . . 10
⊢ ((π /
6) ∈ ℝ → (cos‘(π / 6)) ∈
ℝ) |
12 | 6, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(cos‘(π / 6)) ∈ ℝ |
13 | 12 | recni 10052 |
. . . . . . . 8
⊢
(cos‘(π / 6)) ∈ ℂ |
14 | 1, 9, 13 | mulassi 10049 |
. . . . . . 7
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (2 ·
((sin‘(π / 6)) · (cos‘(π / 6)))) |
15 | | sin2t 14907 |
. . . . . . . 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 2647 |
. . . . . 6
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) =
(sin‘(2 · (π / 6))) |
18 | | 3cn 11095 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
19 | | 3ne0 11115 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
20 | 1, 18, 19 | divcli 10767 |
. . . . . . . . 9
⊢ (2 / 3)
∈ ℂ |
21 | 18, 19 | reccli 10755 |
. . . . . . . . 9
⊢ (1 / 3)
∈ ℂ |
22 | | df-3 11080 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
23 | 22 | oveq1i 6660 |
. . . . . . . . . 10
⊢ (3 / 3) =
((2 + 1) / 3) |
24 | 18, 19 | dividi 10758 |
. . . . . . . . . 10
⊢ (3 / 3) =
1 |
25 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
26 | 1, 25, 18, 19 | divdiri 10782 |
. . . . . . . . . 10
⊢ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) |
27 | 23, 24, 26 | 3eqtr3ri 2653 |
. . . . . . . . 9
⊢ ((2 / 3)
+ (1 / 3)) = 1 |
28 | | sincosq1eq 24264 |
. . . . . . . . 9
⊢ (((2 / 3)
∈ ℂ ∧ (1 / 3) ∈ ℂ ∧ ((2 / 3) + (1 / 3)) = 1)
→ (sin‘((2 / 3) · (π / 2))) = (cos‘((1 / 3) ·
(π / 2)))) |
29 | 20, 21, 27, 28 | mp3an 1424 |
. . . . . . . 8
⊢
(sin‘((2 / 3) · (π / 2))) = (cos‘((1 / 3) ·
(π / 2))) |
30 | | picn 24211 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
31 | 1, 18, 30, 1, 19, 10 | divmuldivi 10785 |
. . . . . . . . . 10
⊢ ((2 / 3)
· (π / 2)) = ((2 · π) / (3 · 2)) |
32 | | 3t2e6 11179 |
. . . . . . . . . . 11
⊢ (3
· 2) = 6 |
33 | 32 | oveq2i 6661 |
. . . . . . . . . 10
⊢ ((2
· π) / (3 · 2)) = ((2 · π) / 6) |
34 | | 6cn 11102 |
. . . . . . . . . . 11
⊢ 6 ∈
ℂ |
35 | 1, 30, 34, 5 | divassi 10781 |
. . . . . . . . . 10
⊢ ((2
· π) / 6) = (2 · (π / 6)) |
36 | 31, 33, 35 | 3eqtri 2648 |
. . . . . . . . 9
⊢ ((2 / 3)
· (π / 2)) = (2 · (π / 6)) |
37 | 36 | fveq2i 6194 |
. . . . . . . 8
⊢
(sin‘((2 / 3) · (π / 2))) = (sin‘(2 · (π
/ 6))) |
38 | 29, 37 | eqtr3i 2646 |
. . . . . . 7
⊢
(cos‘((1 / 3) · (π / 2))) = (sin‘(2 · (π
/ 6))) |
39 | 25, 18, 30, 1, 19, 10 | divmuldivi 10785 |
. . . . . . . . 9
⊢ ((1 / 3)
· (π / 2)) = ((1 · π) / (3 · 2)) |
40 | 30 | mulid2i 10043 |
. . . . . . . . . 10
⊢ (1
· π) = π |
41 | 40, 32 | oveq12i 6662 |
. . . . . . . . 9
⊢ ((1
· π) / (3 · 2)) = (π / 6) |
42 | 39, 41 | eqtri 2644 |
. . . . . . . 8
⊢ ((1 / 3)
· (π / 2)) = (π / 6) |
43 | 42 | fveq2i 6194 |
. . . . . . 7
⊢
(cos‘((1 / 3) · (π / 2))) = (cos‘(π /
6)) |
44 | 38, 43 | eqtr3i 2646 |
. . . . . 6
⊢
(sin‘(2 · (π / 6))) = (cos‘(π /
6)) |
45 | 17, 44 | eqtri 2644 |
. . . . 5
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) =
(cos‘(π / 6)) |
46 | 13 | mulid2i 10043 |
. . . . 5
⊢ (1
· (cos‘(π / 6))) = (cos‘(π / 6)) |
47 | 45, 46 | eqtr4i 2647 |
. . . 4
⊢ ((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (1 ·
(cos‘(π / 6))) |
48 | 1, 9 | mulcli 10045 |
. . . . 5
⊢ (2
· (sin‘(π / 6))) ∈ ℂ |
49 | | pipos 24212 |
. . . . . . . . . . 11
⊢ 0 <
π |
50 | 2, 3, 49, 4 | divgt0ii 10941 |
. . . . . . . . . 10
⊢ 0 <
(π / 6) |
51 | | 2lt6 11207 |
. . . . . . . . . . 11
⊢ 2 <
6 |
52 | | 2re 11090 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
53 | | 2pos 11112 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
54 | 52, 53 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ ∧ 0 < 2) |
55 | 3, 4 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (6 ∈
ℝ ∧ 0 < 6) |
56 | 2, 49 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (π
∈ ℝ ∧ 0 < π) |
57 | | ltdiv2 10909 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℝ ∧ 0 < 2) ∧ (6 ∈ ℝ ∧ 0 < 6) ∧
(π ∈ ℝ ∧ 0 < π)) → (2 < 6 ↔ (π / 6)
< (π / 2))) |
58 | 54, 55, 56, 57 | mp3an 1424 |
. . . . . . . . . . 11
⊢ (2 < 6
↔ (π / 6) < (π / 2)) |
59 | 51, 58 | mpbi 220 |
. . . . . . . . . 10
⊢ (π /
6) < (π / 2) |
60 | | 0re 10040 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
61 | | halfpire 24216 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℝ |
62 | | rexr 10085 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ → 0 ∈ ℝ*) |
63 | | rexr 10085 |
. . . . . . . . . . . 12
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
64 | | elioo2 12216 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
((π / 6) ∈ (0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0
< (π / 6) ∧ (π / 6) < (π / 2)))) |
65 | 62, 63, 64 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (π / 2) ∈ ℝ) → ((π / 6) ∈
(0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π / 6)
∧ (π / 6) < (π / 2)))) |
66 | 60, 61, 65 | mp2an 708 |
. . . . . . . . . 10
⊢ ((π /
6) ∈ (0(,)(π / 2)) ↔ ((π / 6) ∈ ℝ ∧ 0 < (π
/ 6) ∧ (π / 6) < (π / 2))) |
67 | 6, 50, 59, 66 | mpbir3an 1244 |
. . . . . . . . 9
⊢ (π /
6) ∈ (0(,)(π / 2)) |
68 | | sincosq1sgn 24250 |
. . . . . . . . 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 478 |
. . . . . . 7
⊢ 0 <
(cos‘(π / 6)) |
71 | 12, 70 | gt0ne0ii 10564 |
. . . . . 6
⊢
(cos‘(π / 6)) ≠ 0 |
72 | 13, 71 | pm3.2i 471 |
. . . . 5
⊢
((cos‘(π / 6)) ∈ ℂ ∧ (cos‘(π / 6)) ≠
0) |
73 | | mulcan2 10665 |
. . . . 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 1424 |
. . . 4
⊢ (((2
· (sin‘(π / 6))) · (cos‘(π / 6))) = (1 ·
(cos‘(π / 6))) ↔ (2 · (sin‘(π / 6))) =
1) |
75 | 47, 74 | mpbi 220 |
. . 3
⊢ (2
· (sin‘(π / 6))) = 1 |
76 | 1, 9, 10, 75 | mvllmuli 10858 |
. 2
⊢
(sin‘(π / 6)) = (1 / 2) |
77 | | 3re 11094 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
78 | | 3pos 11114 |
. . . . . . . 8
⊢ 0 <
3 |
79 | 77, 78 | sqrtpclii 14122 |
. . . . . . 7
⊢
(√‘3) ∈ ℝ |
80 | 79 | recni 10052 |
. . . . . 6
⊢
(√‘3) ∈ ℂ |
81 | 80, 1, 10 | sqdivi 12948 |
. . . . 5
⊢
(((√‘3) / 2)↑2) = (((√‘3)↑2) /
(2↑2)) |
82 | 60, 77, 78 | ltleii 10160 |
. . . . . . 7
⊢ 0 ≤
3 |
83 | 77 | sqsqrti 14115 |
. . . . . . 7
⊢ (0 ≤ 3
→ ((√‘3)↑2) = 3) |
84 | 82, 83 | ax-mp 5 |
. . . . . 6
⊢
((√‘3)↑2) = 3 |
85 | | sq2 12960 |
. . . . . 6
⊢
(2↑2) = 4 |
86 | 84, 85 | oveq12i 6662 |
. . . . 5
⊢
(((√‘3)↑2) / (2↑2)) = (3 / 4) |
87 | 81, 86 | eqtri 2644 |
. . . 4
⊢
(((√‘3) / 2)↑2) = (3 / 4) |
88 | 87 | fveq2i 6194 |
. . 3
⊢
(√‘(((√‘3) / 2)↑2)) = (√‘(3 /
4)) |
89 | 77 | sqrtge0i 14116 |
. . . . . 6
⊢ (0 ≤ 3
→ 0 ≤ (√‘3)) |
90 | 82, 89 | ax-mp 5 |
. . . . 5
⊢ 0 ≤
(√‘3) |
91 | 79, 52 | divge0i 10933 |
. . . . 5
⊢ ((0 ≤
(√‘3) ∧ 0 < 2) → 0 ≤ ((√‘3) /
2)) |
92 | 90, 53, 91 | mp2an 708 |
. . . 4
⊢ 0 ≤
((√‘3) / 2) |
93 | 79, 52, 10 | redivcli 10792 |
. . . . 5
⊢
((√‘3) / 2) ∈ ℝ |
94 | 93 | sqrtsqi 14114 |
. . . 4
⊢ (0 ≤
((√‘3) / 2) → (√‘(((√‘3) / 2)↑2))
= ((√‘3) / 2)) |
95 | 92, 94 | ax-mp 5 |
. . 3
⊢
(√‘(((√‘3) / 2)↑2)) = ((√‘3) /
2) |
96 | | 4cn 11098 |
. . . . . . . 8
⊢ 4 ∈
ℂ |
97 | | 4ne0 11117 |
. . . . . . . 8
⊢ 4 ≠
0 |
98 | 96, 97 | dividi 10758 |
. . . . . . 7
⊢ (4 / 4) =
1 |
99 | 98 | oveq1i 6660 |
. . . . . 6
⊢ ((4 / 4)
− (1 / 4)) = (1 − (1 / 4)) |
100 | 96, 97 | pm3.2i 471 |
. . . . . . . 8
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
101 | | divsubdir 10721 |
. . . . . . . 8
⊢ ((4
∈ ℂ ∧ 1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0))
→ ((4 − 1) / 4) = ((4 / 4) − (1 / 4))) |
102 | 96, 25, 100, 101 | mp3an 1424 |
. . . . . . 7
⊢ ((4
− 1) / 4) = ((4 / 4) − (1 / 4)) |
103 | | 3p1e4 11153 |
. . . . . . . . 9
⊢ (3 + 1) =
4 |
104 | 96, 25, 18 | subadd2i 10369 |
. . . . . . . . 9
⊢ ((4
− 1) = 3 ↔ (3 + 1) = 4) |
105 | 103, 104 | mpbir 221 |
. . . . . . . 8
⊢ (4
− 1) = 3 |
106 | 105 | oveq1i 6660 |
. . . . . . 7
⊢ ((4
− 1) / 4) = (3 / 4) |
107 | 102, 106 | eqtr3i 2646 |
. . . . . 6
⊢ ((4 / 4)
− (1 / 4)) = (3 / 4) |
108 | 96, 97 | reccli 10755 |
. . . . . . 7
⊢ (1 / 4)
∈ ℂ |
109 | 13 | sqcli 12944 |
. . . . . . 7
⊢
((cos‘(π / 6))↑2) ∈ ℂ |
110 | 76 | oveq1i 6660 |
. . . . . . . . . 10
⊢
((sin‘(π / 6))↑2) = ((1 / 2)↑2) |
111 | 1, 10 | sqrecii 12946 |
. . . . . . . . . 10
⊢ ((1 /
2)↑2) = (1 / (2↑2)) |
112 | 85 | oveq2i 6661 |
. . . . . . . . . 10
⊢ (1 /
(2↑2)) = (1 / 4) |
113 | 110, 111,
112 | 3eqtri 2648 |
. . . . . . . . 9
⊢
((sin‘(π / 6))↑2) = (1 / 4) |
114 | 113 | oveq1i 6660 |
. . . . . . . 8
⊢
(((sin‘(π / 6))↑2) + ((cos‘(π / 6))↑2)) =
((1 / 4) + ((cos‘(π / 6))↑2)) |
115 | | sincossq 14906 |
. . . . . . . . 9
⊢ ((π /
6) ∈ ℂ → (((sin‘(π / 6))↑2) + ((cos‘(π /
6))↑2)) = 1) |
116 | 7, 115 | ax-mp 5 |
. . . . . . . 8
⊢
(((sin‘(π / 6))↑2) + ((cos‘(π / 6))↑2)) =
1 |
117 | 114, 116 | eqtr3i 2646 |
. . . . . . 7
⊢ ((1 / 4)
+ ((cos‘(π / 6))↑2)) = 1 |
118 | 25, 108, 109, 117 | subaddrii 10370 |
. . . . . 6
⊢ (1
− (1 / 4)) = ((cos‘(π / 6))↑2) |
119 | 99, 107, 118 | 3eqtr3ri 2653 |
. . . . 5
⊢
((cos‘(π / 6))↑2) = (3 / 4) |
120 | 119 | fveq2i 6194 |
. . . 4
⊢
(√‘((cos‘(π / 6))↑2)) = (√‘(3 /
4)) |
121 | 60, 12, 70 | ltleii 10160 |
. . . . 5
⊢ 0 ≤
(cos‘(π / 6)) |
122 | 12 | sqrtsqi 14114 |
. . . . 5
⊢ (0 ≤
(cos‘(π / 6)) → (√‘((cos‘(π / 6))↑2)) =
(cos‘(π / 6))) |
123 | 121, 122 | ax-mp 5 |
. . . 4
⊢
(√‘((cos‘(π / 6))↑2)) = (cos‘(π /
6)) |
124 | 120, 123 | eqtr3i 2646 |
. . 3
⊢
(√‘(3 / 4)) = (cos‘(π / 6)) |
125 | 88, 95, 124 | 3eqtr3ri 2653 |
. 2
⊢
(cos‘(π / 6)) = ((√‘3) / 2) |
126 | 76, 125 | pm3.2i 471 |
1
⊢
((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) =
((√‘3) / 2)) |