Proof of Theorem sin2h
Step | Hyp | Ref
| Expression |
1 | | 0re 10835 |
. . . . . 6
⊢ 0 ∈
ℝ |
2 | | 2re 11904 |
. . . . . . 7
⊢ 2 ∈
ℝ |
3 | | pire 25348 |
. . . . . . 7
⊢ π
∈ ℝ |
4 | 2, 3 | remulcli 10849 |
. . . . . 6
⊢ (2
· π) ∈ ℝ |
5 | | iccssre 13017 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ (2 · π) ∈ ℝ) → (0[,](2 ·
π)) ⊆ ℝ) |
6 | 1, 4, 5 | mp2an 692 |
. . . . 5
⊢ (0[,](2
· π)) ⊆ ℝ |
7 | 6 | sseli 3896 |
. . . 4
⊢ (𝐴 ∈ (0[,](2 · π))
→ 𝐴 ∈
ℝ) |
8 | 7 | rehalfcld 12077 |
. . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ (𝐴 / 2) ∈
ℝ) |
9 | 8 | resincld 15704 |
. 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ (sin‘(𝐴 / 2))
∈ ℝ) |
10 | | 1re 10833 |
. . . . . 6
⊢ 1 ∈
ℝ |
11 | | recoscl 15702 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) ∈
ℝ) |
12 | | resubcl 11142 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (1 −
(cos‘𝐴)) ∈
ℝ) |
13 | 10, 11, 12 | sylancr 590 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (1
− (cos‘𝐴))
∈ ℝ) |
14 | 13 | rehalfcld 12077 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((1
− (cos‘𝐴)) / 2)
∈ ℝ) |
15 | | cosbnd 15742 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (-1 ≤
(cos‘𝐴) ∧
(cos‘𝐴) ≤
1)) |
16 | 15 | simprd 499 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) ≤
1) |
17 | | subge0 11345 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (0 ≤ (1 −
(cos‘𝐴)) ↔
(cos‘𝐴) ≤
1)) |
18 | 10, 11, 17 | sylancr 590 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 ≤
(1 − (cos‘𝐴))
↔ (cos‘𝐴) ≤
1)) |
19 | | halfnneg2 12061 |
. . . . . . 7
⊢ ((1
− (cos‘𝐴))
∈ ℝ → (0 ≤ (1 − (cos‘𝐴)) ↔ 0 ≤ ((1 −
(cos‘𝐴)) /
2))) |
20 | 13, 19 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 ≤
(1 − (cos‘𝐴))
↔ 0 ≤ ((1 − (cos‘𝐴)) / 2))) |
21 | 18, 20 | bitr3d 284 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) ≤ 1
↔ 0 ≤ ((1 − (cos‘𝐴)) / 2))) |
22 | 16, 21 | mpbid 235 |
. . . 4
⊢ (𝐴 ∈ ℝ → 0 ≤
((1 − (cos‘𝐴))
/ 2)) |
23 | 14, 22 | resqrtcld 14981 |
. . 3
⊢ (𝐴 ∈ ℝ →
(√‘((1 − (cos‘𝐴)) / 2)) ∈ ℝ) |
24 | 7, 23 | syl 17 |
. 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ (√‘((1 − (cos‘𝐴)) / 2)) ∈ ℝ) |
25 | 1, 4 | elicc2i 13001 |
. . . 4
⊢ (𝐴 ∈ (0[,](2 · π))
↔ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ (2 ·
π))) |
26 | | halfnneg2 12061 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 ≤
𝐴 ↔ 0 ≤ (𝐴 / 2))) |
27 | | 2pos 11933 |
. . . . . . . . . . 11
⊢ 0 <
2 |
28 | 2, 27 | pm3.2i 474 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) |
29 | | ledivmul 11708 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐴 / 2) ≤ π ↔ 𝐴 ≤ (2 ·
π))) |
30 | 3, 28, 29 | mp3an23 1455 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ≤ π ↔ 𝐴 ≤ (2 ·
π))) |
31 | 30 | bicomd 226 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ (2 · π) ↔
(𝐴 / 2) ≤
π)) |
32 | 26, 31 | anbi12d 634 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) ↔ (0 ≤
(𝐴 / 2) ∧ (𝐴 / 2) ≤
π))) |
33 | | rehalfcl 12056 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
34 | 33 | rexrd 10883 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ*) |
35 | | 0xr 10880 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
36 | 3 | rexri 10891 |
. . . . . . . . 9
⊢ π
∈ ℝ* |
37 | | elicc4 13002 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝐴 / 2) ∈
ℝ*) → ((𝐴 / 2) ∈ (0[,]π) ↔ (0 ≤
(𝐴 / 2) ∧ (𝐴 / 2) ≤
π))) |
38 | 35, 36, 37 | mp3an12 1453 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ*
→ ((𝐴 / 2) ∈
(0[,]π) ↔ (0 ≤ (𝐴 / 2) ∧ (𝐴 / 2) ≤ π))) |
39 | 34, 38 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ∈ (0[,]π) ↔
(0 ≤ (𝐴 / 2) ∧
(𝐴 / 2) ≤
π))) |
40 | 32, 39 | bitr4d 285 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) ↔ (𝐴 / 2) ∈
(0[,]π))) |
41 | 40 | biimpd 232 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) → (𝐴 / 2) ∈
(0[,]π))) |
42 | 41 | 3impib 1118 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) → (𝐴 / 2) ∈
(0[,]π)) |
43 | 25, 42 | sylbi 220 |
. . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ (𝐴 / 2) ∈
(0[,]π)) |
44 | | sinq12ge0 25398 |
. . 3
⊢ ((𝐴 / 2) ∈ (0[,]π) → 0
≤ (sin‘(𝐴 /
2))) |
45 | 43, 44 | syl 17 |
. 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ 0 ≤ (sin‘(𝐴
/ 2))) |
46 | 14, 22 | sqrtge0d 14984 |
. . 3
⊢ (𝐴 ∈ ℝ → 0 ≤
(√‘((1 − (cos‘𝐴)) / 2))) |
47 | 7, 46 | syl 17 |
. 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ 0 ≤ (√‘((1 − (cos‘𝐴)) / 2))) |
48 | 7 | recnd 10861 |
. . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ 𝐴 ∈
ℂ) |
49 | | ax-1cn 10787 |
. . . . . . 7
⊢ 1 ∈
ℂ |
50 | | coscl 15688 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
51 | | subcl 11077 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 −
(cos‘𝐴)) ∈
ℂ) |
52 | 49, 50, 51 | sylancr 590 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1
− (cos‘𝐴))
∈ ℂ) |
53 | 52 | halfcld 12075 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((1
− (cos‘𝐴)) / 2)
∈ ℂ) |
54 | 53 | sqsqrtd 15003 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((√‘((1 − (cos‘𝐴)) / 2))↑2) = ((1 −
(cos‘𝐴)) /
2)) |
55 | | halfcl 12055 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈
ℂ) |
56 | | coscl 15688 |
. . . . . . . . . . . . 13
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(𝐴 / 2)) ∈
ℂ) |
57 | 56 | sqcld 13714 |
. . . . . . . . . . . 12
⊢ ((𝐴 / 2) ∈ ℂ →
((cos‘(𝐴 /
2))↑2) ∈ ℂ) |
58 | | 2cn 11905 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
59 | | mulcom 10815 |
. . . . . . . . . . . 12
⊢
((((cos‘(𝐴 /
2))↑2) ∈ ℂ ∧ 2 ∈ ℂ) → (((cos‘(𝐴 / 2))↑2) · 2) = (2
· ((cos‘(𝐴 /
2))↑2))) |
60 | 57, 58, 59 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
(((cos‘(𝐴 /
2))↑2) · 2) = (2 · ((cos‘(𝐴 / 2))↑2))) |
61 | 60 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ → ((1
· 2) − (((cos‘(𝐴 / 2))↑2) · 2)) = ((1 ·
2) − (2 · ((cos‘(𝐴 / 2))↑2)))) |
62 | 58 | mulid2i 10838 |
. . . . . . . . . . . 12
⊢ (1
· 2) = 2 |
63 | | df-2 11893 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
64 | 62, 63 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (1
· 2) = (1 + 1) |
65 | 64 | oveq1i 7223 |
. . . . . . . . . 10
⊢ ((1
· 2) − (2 · ((cos‘(𝐴 / 2))↑2))) = ((1 + 1) − (2
· ((cos‘(𝐴 /
2))↑2))) |
66 | 61, 65 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ → ((1
· 2) − (((cos‘(𝐴 / 2))↑2) · 2)) = ((1 + 1)
− (2 · ((cos‘(𝐴 / 2))↑2)))) |
67 | | subdir 11266 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℂ ∧ 2 ∈
ℂ) → ((1 − ((cos‘(𝐴 / 2))↑2)) · 2) = ((1 ·
2) − (((cos‘(𝐴
/ 2))↑2) · 2))) |
68 | 49, 58, 67 | mp3an13 1454 |
. . . . . . . . . 10
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → ((1 − ((cos‘(𝐴 / 2))↑2)) · 2) = ((1 ·
2) − (((cos‘(𝐴
/ 2))↑2) · 2))) |
69 | 57, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ → ((1
− ((cos‘(𝐴 /
2))↑2)) · 2) = ((1 · 2) − (((cos‘(𝐴 / 2))↑2) ·
2))) |
70 | | mulcl 10813 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℂ) → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ) |
71 | 58, 57, 70 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ) |
72 | | subsub3 11110 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (2 · ((cos‘(𝐴 / 2))↑2)) ∈ ℂ ∧ 1
∈ ℂ) → (1 − ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) = ((1 + 1)
− (2 · ((cos‘(𝐴 / 2))↑2)))) |
73 | 49, 49, 72 | mp3an13 1454 |
. . . . . . . . . 10
⊢ ((2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ → (1 − ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) =
((1 + 1) − (2 · ((cos‘(𝐴 / 2))↑2)))) |
74 | 71, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ → (1
− ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) = ((1 + 1)
− (2 · ((cos‘(𝐴 / 2))↑2)))) |
75 | 66, 69, 74 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ → ((1
− ((cos‘(𝐴 /
2))↑2)) · 2) = (1 − ((2 · ((cos‘(𝐴 / 2))↑2)) −
1))) |
76 | | sincl 15687 |
. . . . . . . . . . . 12
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(𝐴 / 2)) ∈
ℂ) |
77 | 76 | sqcld 13714 |
. . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
((sin‘(𝐴 /
2))↑2) ∈ ℂ) |
78 | 77, 57 | pncand 11190 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) − ((cos‘(𝐴 / 2))↑2)) =
((sin‘(𝐴 /
2))↑2)) |
79 | | sincossq 15737 |
. . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) = 1) |
80 | 79 | oveq1d 7228 |
. . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) − ((cos‘(𝐴 / 2))↑2)) = (1 −
((cos‘(𝐴 /
2))↑2))) |
81 | 78, 80 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ →
((sin‘(𝐴 /
2))↑2) = (1 − ((cos‘(𝐴 / 2))↑2))) |
82 | 81 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = ((1 − ((cos‘(𝐴 / 2))↑2)) ·
2)) |
83 | | cos2t 15739 |
. . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) |
84 | 83 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ → (1
− (cos‘(2 · (𝐴 / 2)))) = (1 − ((2 ·
((cos‘(𝐴 /
2))↑2)) − 1))) |
85 | 75, 82, 84 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = (1 − (cos‘(2 · (𝐴 / 2))))) |
86 | 55, 85 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = (1 − (cos‘(2 · (𝐴 / 2))))) |
87 | | 2ne0 11934 |
. . . . . . . . 9
⊢ 2 ≠
0 |
88 | | divcan2 11498 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐴 / 2)) = 𝐴) |
89 | 58, 87, 88 | mp3an23 1455 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) |
90 | 89 | fveq2d 6721 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = (cos‘𝐴)) |
91 | 90 | oveq2d 7229 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1
− (cos‘(2 · (𝐴 / 2)))) = (1 − (cos‘𝐴))) |
92 | 86, 91 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = (1 − (cos‘𝐴))) |
93 | 92 | oveq1d 7228 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) · 2) / 2) = ((1 − (cos‘𝐴)) / 2)) |
94 | 55 | sincld 15691 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(sin‘(𝐴 / 2)) ∈
ℂ) |
95 | 94 | sqcld 13714 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((sin‘(𝐴 /
2))↑2) ∈ ℂ) |
96 | | divcan4 11517 |
. . . . . 6
⊢
((((sin‘(𝐴 /
2))↑2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) →
((((sin‘(𝐴 /
2))↑2) · 2) / 2) = ((sin‘(𝐴 / 2))↑2)) |
97 | 58, 87, 96 | mp3an23 1455 |
. . . . 5
⊢
(((sin‘(𝐴 /
2))↑2) ∈ ℂ → ((((sin‘(𝐴 / 2))↑2) · 2) / 2) =
((sin‘(𝐴 /
2))↑2)) |
98 | 95, 97 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) · 2) / 2) = ((sin‘(𝐴 / 2))↑2)) |
99 | 54, 93, 98 | 3eqtr2rd 2784 |
. . 3
⊢ (𝐴 ∈ ℂ →
((sin‘(𝐴 /
2))↑2) = ((√‘((1 − (cos‘𝐴)) / 2))↑2)) |
100 | 48, 99 | syl 17 |
. 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ ((sin‘(𝐴 /
2))↑2) = ((√‘((1 − (cos‘𝐴)) / 2))↑2)) |
101 | 9, 24, 45, 47, 100 | sq11d 13827 |
1
⊢ (𝐴 ∈ (0[,](2 · π))
→ (sin‘(𝐴 / 2))
= (√‘((1 − (cos‘𝐴)) / 2))) |