Proof of Theorem sin2h
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0re 11264 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 2 |  | 2re 12341 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 3 |  | pire 26501 | . . . . . . 7
⊢ π
∈ ℝ | 
| 4 | 2, 3 | remulcli 11278 | . . . . . 6
⊢ (2
· π) ∈ ℝ | 
| 5 |  | iccssre 13470 | . . . . . 6
⊢ ((0
∈ ℝ ∧ (2 · π) ∈ ℝ) → (0[,](2 ·
π)) ⊆ ℝ) | 
| 6 | 1, 4, 5 | mp2an 692 | . . . . 5
⊢ (0[,](2
· π)) ⊆ ℝ | 
| 7 | 6 | sseli 3978 | . . . 4
⊢ (𝐴 ∈ (0[,](2 · π))
→ 𝐴 ∈
ℝ) | 
| 8 | 7 | rehalfcld 12515 | . . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ (𝐴 / 2) ∈
ℝ) | 
| 9 | 8 | resincld 16180 | . 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ (sin‘(𝐴 / 2))
∈ ℝ) | 
| 10 |  | 1re 11262 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 11 |  | recoscl 16178 | . . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) ∈
ℝ) | 
| 12 |  | resubcl 11574 | . . . . . 6
⊢ ((1
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (1 −
(cos‘𝐴)) ∈
ℝ) | 
| 13 | 10, 11, 12 | sylancr 587 | . . . . 5
⊢ (𝐴 ∈ ℝ → (1
− (cos‘𝐴))
∈ ℝ) | 
| 14 | 13 | rehalfcld 12515 | . . . 4
⊢ (𝐴 ∈ ℝ → ((1
− (cos‘𝐴)) / 2)
∈ ℝ) | 
| 15 |  | cosbnd 16218 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (-1 ≤
(cos‘𝐴) ∧
(cos‘𝐴) ≤
1)) | 
| 16 | 15 | simprd 495 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) ≤
1) | 
| 17 |  | subge0 11777 | . . . . . . 7
⊢ ((1
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (0 ≤ (1 −
(cos‘𝐴)) ↔
(cos‘𝐴) ≤
1)) | 
| 18 | 10, 11, 17 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (0 ≤
(1 − (cos‘𝐴))
↔ (cos‘𝐴) ≤
1)) | 
| 19 |  | halfnneg2 12499 | . . . . . . 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 281 | . . . . 5
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) ≤ 1
↔ 0 ≤ ((1 − (cos‘𝐴)) / 2))) | 
| 22 | 16, 21 | mpbid 232 | . . . 4
⊢ (𝐴 ∈ ℝ → 0 ≤
((1 − (cos‘𝐴))
/ 2)) | 
| 23 | 14, 22 | resqrtcld 15457 | . . 3
⊢ (𝐴 ∈ ℝ →
(√‘((1 − (cos‘𝐴)) / 2)) ∈ ℝ) | 
| 24 | 7, 23 | syl 17 | . 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ (√‘((1 − (cos‘𝐴)) / 2)) ∈ ℝ) | 
| 25 | 1, 4 | elicc2i 13454 | . . . 4
⊢ (𝐴 ∈ (0[,](2 · π))
↔ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ (2 ·
π))) | 
| 26 |  | halfnneg2 12499 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 ≤
𝐴 ↔ 0 ≤ (𝐴 / 2))) | 
| 27 |  | 2pos 12370 | . . . . . . . . . . 11
⊢ 0 <
2 | 
| 28 | 2, 27 | pm3.2i 470 | . . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 29 |  | ledivmul 12145 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝐴 / 2) ≤ π ↔ 𝐴 ≤ (2 ·
π))) | 
| 30 | 3, 28, 29 | mp3an23 1454 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ≤ π ↔ 𝐴 ≤ (2 ·
π))) | 
| 31 | 30 | bicomd 223 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ (2 · π) ↔
(𝐴 / 2) ≤
π)) | 
| 32 | 26, 31 | anbi12d 632 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) ↔ (0 ≤
(𝐴 / 2) ∧ (𝐴 / 2) ≤
π))) | 
| 33 |  | rehalfcl 12495 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) | 
| 34 | 33 | rexrd 11312 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ*) | 
| 35 |  | 0xr 11309 | . . . . . . . . 9
⊢ 0 ∈
ℝ* | 
| 36 | 3 | rexri 11320 | . . . . . . . . 9
⊢ π
∈ ℝ* | 
| 37 |  | elicc4 13455 | . . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ (𝐴 / 2) ∈
ℝ*) → ((𝐴 / 2) ∈ (0[,]π) ↔ (0 ≤
(𝐴 / 2) ∧ (𝐴 / 2) ≤
π))) | 
| 38 | 35, 36, 37 | mp3an12 1452 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ*
→ ((𝐴 / 2) ∈
(0[,]π) ↔ (0 ≤ (𝐴 / 2) ∧ (𝐴 / 2) ≤ π))) | 
| 39 | 34, 38 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ∈ (0[,]π) ↔
(0 ≤ (𝐴 / 2) ∧
(𝐴 / 2) ≤
π))) | 
| 40 | 32, 39 | bitr4d 282 | . . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) ↔ (𝐴 / 2) ∈
(0[,]π))) | 
| 41 | 40 | biimpd 229 | . . . . 5
⊢ (𝐴 ∈ ℝ → ((0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) → (𝐴 / 2) ∈
(0[,]π))) | 
| 42 | 41 | 3impib 1116 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ (2 · π)) → (𝐴 / 2) ∈
(0[,]π)) | 
| 43 | 25, 42 | sylbi 217 | . . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ (𝐴 / 2) ∈
(0[,]π)) | 
| 44 |  | sinq12ge0 26551 | . . 3
⊢ ((𝐴 / 2) ∈ (0[,]π) → 0
≤ (sin‘(𝐴 /
2))) | 
| 45 | 43, 44 | syl 17 | . 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ 0 ≤ (sin‘(𝐴
/ 2))) | 
| 46 | 14, 22 | sqrtge0d 15460 | . . 3
⊢ (𝐴 ∈ ℝ → 0 ≤
(√‘((1 − (cos‘𝐴)) / 2))) | 
| 47 | 7, 46 | syl 17 | . 2
⊢ (𝐴 ∈ (0[,](2 · π))
→ 0 ≤ (√‘((1 − (cos‘𝐴)) / 2))) | 
| 48 | 7 | recnd 11290 | . . 3
⊢ (𝐴 ∈ (0[,](2 · π))
→ 𝐴 ∈
ℂ) | 
| 49 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 50 |  | coscl 16164 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) | 
| 51 |  | subcl 11508 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 −
(cos‘𝐴)) ∈
ℂ) | 
| 52 | 49, 50, 51 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (1
− (cos‘𝐴))
∈ ℂ) | 
| 53 | 52 | halfcld 12513 | . . . . 5
⊢ (𝐴 ∈ ℂ → ((1
− (cos‘𝐴)) / 2)
∈ ℂ) | 
| 54 | 53 | sqsqrtd 15479 | . . . 4
⊢ (𝐴 ∈ ℂ →
((√‘((1 − (cos‘𝐴)) / 2))↑2) = ((1 −
(cos‘𝐴)) /
2)) | 
| 55 |  | halfcl 12494 | . . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈
ℂ) | 
| 56 |  | coscl 16164 | . . . . . . . . . . . . 13
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(𝐴 / 2)) ∈
ℂ) | 
| 57 | 56 | sqcld 14185 | . . . . . . . . . . . 12
⊢ ((𝐴 / 2) ∈ ℂ →
((cos‘(𝐴 /
2))↑2) ∈ ℂ) | 
| 58 |  | 2cn 12342 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 59 |  | mulcom 11242 | . . . . . . . . . . . 12
⊢
((((cos‘(𝐴 /
2))↑2) ∈ ℂ ∧ 2 ∈ ℂ) → (((cos‘(𝐴 / 2))↑2) · 2) = (2
· ((cos‘(𝐴 /
2))↑2))) | 
| 60 | 57, 58, 59 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
(((cos‘(𝐴 /
2))↑2) · 2) = (2 · ((cos‘(𝐴 / 2))↑2))) | 
| 61 | 60 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ → ((1
· 2) − (((cos‘(𝐴 / 2))↑2) · 2)) = ((1 ·
2) − (2 · ((cos‘(𝐴 / 2))↑2)))) | 
| 62 | 58 | mullidi 11267 | . . . . . . . . . . . 12
⊢ (1
· 2) = 2 | 
| 63 |  | df-2 12330 | . . . . . . . . . . . 12
⊢ 2 = (1 +
1) | 
| 64 | 62, 63 | eqtri 2764 | . . . . . . . . . . 11
⊢ (1
· 2) = (1 + 1) | 
| 65 | 64 | oveq1i 7442 | . . . . . . . . . 10
⊢ ((1
· 2) − (2 · ((cos‘(𝐴 / 2))↑2))) = ((1 + 1) − (2
· ((cos‘(𝐴 /
2))↑2))) | 
| 66 | 61, 65 | eqtrdi 2792 | . . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ → ((1
· 2) − (((cos‘(𝐴 / 2))↑2) · 2)) = ((1 + 1)
− (2 · ((cos‘(𝐴 / 2))↑2)))) | 
| 67 |  | subdir 11698 | . . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℂ ∧ 2 ∈
ℂ) → ((1 − ((cos‘(𝐴 / 2))↑2)) · 2) = ((1 ·
2) − (((cos‘(𝐴
/ 2))↑2) · 2))) | 
| 68 | 49, 58, 67 | mp3an13 1453 | . . . . . . . . . 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 11240 | . . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℂ) → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ) | 
| 71 | 58, 57, 70 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ) | 
| 72 |  | subsub3 11542 | . . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (2 · ((cos‘(𝐴 / 2))↑2)) ∈ ℂ ∧ 1
∈ ℂ) → (1 − ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) = ((1 + 1)
− (2 · ((cos‘(𝐴 / 2))↑2)))) | 
| 73 | 49, 49, 72 | mp3an13 1453 | . . . . . . . . . 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 2786 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ → ((1
− ((cos‘(𝐴 /
2))↑2)) · 2) = (1 − ((2 · ((cos‘(𝐴 / 2))↑2)) −
1))) | 
| 76 |  | sincl 16163 | . . . . . . . . . . . 12
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(𝐴 / 2)) ∈
ℂ) | 
| 77 | 76 | sqcld 14185 | . . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
((sin‘(𝐴 /
2))↑2) ∈ ℂ) | 
| 78 | 77, 57 | pncand 11622 | . . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) − ((cos‘(𝐴 / 2))↑2)) =
((sin‘(𝐴 /
2))↑2)) | 
| 79 |  | sincossq 16213 | . . . . . . . . . . 11
⊢ ((𝐴 / 2) ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) = 1) | 
| 80 | 79 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝐴 / 2) ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) + ((cos‘(𝐴 / 2))↑2)) − ((cos‘(𝐴 / 2))↑2)) = (1 −
((cos‘(𝐴 /
2))↑2))) | 
| 81 | 78, 80 | eqtr3d 2778 | . . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ →
((sin‘(𝐴 /
2))↑2) = (1 − ((cos‘(𝐴 / 2))↑2))) | 
| 82 | 81 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = ((1 − ((cos‘(𝐴 / 2))↑2)) ·
2)) | 
| 83 |  | cos2t 16215 | . . . . . . . . 9
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) | 
| 84 | 83 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ → (1
− (cos‘(2 · (𝐴 / 2)))) = (1 − ((2 ·
((cos‘(𝐴 /
2))↑2)) − 1))) | 
| 85 | 75, 82, 84 | 3eqtr4d 2786 | . . . . . . 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 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 88 |  | divcan2 11931 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐴 / 2)) = 𝐴) | 
| 89 | 58, 87, 88 | mp3an23 1454 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) | 
| 90 | 89 | fveq2d 6909 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = (cos‘𝐴)) | 
| 91 | 90 | oveq2d 7448 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (1
− (cos‘(2 · (𝐴 / 2)))) = (1 − (cos‘𝐴))) | 
| 92 | 86, 91 | eqtrd 2776 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(((sin‘(𝐴 /
2))↑2) · 2) = (1 − (cos‘𝐴))) | 
| 93 | 92 | oveq1d 7447 | . . . 4
⊢ (𝐴 ∈ ℂ →
((((sin‘(𝐴 /
2))↑2) · 2) / 2) = ((1 − (cos‘𝐴)) / 2)) | 
| 94 | 55 | sincld 16167 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(sin‘(𝐴 / 2)) ∈
ℂ) | 
| 95 | 94 | sqcld 14185 | . . . . 5
⊢ (𝐴 ∈ ℂ →
((sin‘(𝐴 /
2))↑2) ∈ ℂ) | 
| 96 |  | divcan4 11950 | . . . . . 6
⊢
((((sin‘(𝐴 /
2))↑2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) →
((((sin‘(𝐴 /
2))↑2) · 2) / 2) = ((sin‘(𝐴 / 2))↑2)) | 
| 97 | 58, 87, 96 | mp3an23 1454 | . . . . 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 2783 | . . 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 14298 | 1
⊢ (𝐴 ∈ (0[,](2 · π))
→ (sin‘(𝐴 / 2))
= (√‘((1 − (cos‘𝐴)) / 2))) |