Proof of Theorem cos2h
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pire 26501 | . . . . . . 7
⊢ π
∈ ℝ | 
| 2 | 1 | renegcli 11571 | . . . . . 6
⊢ -π
∈ ℝ | 
| 3 |  | iccssre 13470 | . . . . . 6
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) | 
| 4 | 2, 1, 3 | mp2an 692 | . . . . 5
⊢
(-π[,]π) ⊆ ℝ | 
| 5 | 4 | sseli 3978 | . . . 4
⊢ (𝐴 ∈ (-π[,]π) →
𝐴 ∈
ℝ) | 
| 6 | 5 | rehalfcld 12515 | . . 3
⊢ (𝐴 ∈ (-π[,]π) →
(𝐴 / 2) ∈
ℝ) | 
| 7 | 6 | recoscld 16181 | . 2
⊢ (𝐴 ∈ (-π[,]π) →
(cos‘(𝐴 / 2)) ∈
ℝ) | 
| 8 |  | 1re 11262 | . . . . 5
⊢ 1 ∈
ℝ | 
| 9 | 5 | recoscld 16181 | . . . . 5
⊢ (𝐴 ∈ (-π[,]π) →
(cos‘𝐴) ∈
ℝ) | 
| 10 |  | readdcl 11239 | . . . . 5
⊢ ((1
∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → (1 +
(cos‘𝐴)) ∈
ℝ) | 
| 11 | 8, 9, 10 | sylancr 587 | . . . 4
⊢ (𝐴 ∈ (-π[,]π) → (1
+ (cos‘𝐴)) ∈
ℝ) | 
| 12 | 11 | rehalfcld 12515 | . . 3
⊢ (𝐴 ∈ (-π[,]π) →
((1 + (cos‘𝐴)) / 2)
∈ ℝ) | 
| 13 |  | cosbnd 16218 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (-1 ≤
(cos‘𝐴) ∧
(cos‘𝐴) ≤
1)) | 
| 14 | 13 | simpld 494 | . . . . 5
⊢ (𝐴 ∈ ℝ → -1 ≤
(cos‘𝐴)) | 
| 15 |  | recoscl 16178 | . . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) ∈
ℝ) | 
| 16 |  | recn 11246 | . . . . . . . . 9
⊢
((cos‘𝐴)
∈ ℝ → (cos‘𝐴) ∈ ℂ) | 
| 17 |  | recn 11246 | . . . . . . . . 9
⊢ (1 ∈
ℝ → 1 ∈ ℂ) | 
| 18 |  | subneg 11559 | . . . . . . . . . 10
⊢
(((cos‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → ((cos‘𝐴) − -1) = ((cos‘𝐴) + 1)) | 
| 19 |  | addcom 11448 | . . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 +
(cos‘𝐴)) =
((cos‘𝐴) +
1)) | 
| 20 | 19 | ancoms 458 | . . . . . . . . . 10
⊢
(((cos‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → (1 + (cos‘𝐴)) = ((cos‘𝐴) + 1)) | 
| 21 | 18, 20 | eqtr4d 2779 | . . . . . . . . 9
⊢
(((cos‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → ((cos‘𝐴) − -1) = (1 + (cos‘𝐴))) | 
| 22 | 16, 17, 21 | syl2an 596 | . . . . . . . 8
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → ((cos‘𝐴) − -1) = (1 + (cos‘𝐴))) | 
| 23 | 22 | breq2d 5154 | . . . . . . 7
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → (0 ≤ ((cos‘𝐴) − -1) ↔ 0 ≤ (1 +
(cos‘𝐴)))) | 
| 24 |  | renegcl 11573 | . . . . . . . 8
⊢ (1 ∈
ℝ → -1 ∈ ℝ) | 
| 25 |  | subge0 11777 | . . . . . . . 8
⊢
(((cos‘𝐴)
∈ ℝ ∧ -1 ∈ ℝ) → (0 ≤ ((cos‘𝐴) − -1) ↔ -1 ≤
(cos‘𝐴))) | 
| 26 | 24, 25 | sylan2 593 | . . . . . . 7
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → (0 ≤ ((cos‘𝐴) − -1) ↔ -1 ≤
(cos‘𝐴))) | 
| 27 | 10 | ancoms 458 | . . . . . . . 8
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → (1 + (cos‘𝐴)) ∈ ℝ) | 
| 28 |  | halfnneg2 12499 | . . . . . . . 8
⊢ ((1 +
(cos‘𝐴)) ∈
ℝ → (0 ≤ (1 + (cos‘𝐴)) ↔ 0 ≤ ((1 + (cos‘𝐴)) / 2))) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → (0 ≤ (1 + (cos‘𝐴)) ↔ 0 ≤ ((1 +
(cos‘𝐴)) /
2))) | 
| 30 | 23, 26, 29 | 3bitr3d 309 | . . . . . 6
⊢
(((cos‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → (-1 ≤ (cos‘𝐴) ↔ 0 ≤ ((1 +
(cos‘𝐴)) /
2))) | 
| 31 | 15, 8, 30 | sylancl 586 | . . . . 5
⊢ (𝐴 ∈ ℝ → (-1 ≤
(cos‘𝐴) ↔ 0 ≤
((1 + (cos‘𝐴)) /
2))) | 
| 32 | 14, 31 | mpbid 232 | . . . 4
⊢ (𝐴 ∈ ℝ → 0 ≤
((1 + (cos‘𝐴)) /
2)) | 
| 33 | 5, 32 | syl 17 | . . 3
⊢ (𝐴 ∈ (-π[,]π) → 0
≤ ((1 + (cos‘𝐴)) /
2)) | 
| 34 | 12, 33 | resqrtcld 15457 | . 2
⊢ (𝐴 ∈ (-π[,]π) →
(√‘((1 + (cos‘𝐴)) / 2)) ∈ ℝ) | 
| 35 | 2, 1 | elicc2i 13454 | . . . 4
⊢ (𝐴 ∈ (-π[,]π) ↔
(𝐴 ∈ ℝ ∧
-π ≤ 𝐴 ∧ 𝐴 ≤ π)) | 
| 36 |  | 2re 12341 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ | 
| 37 |  | 2pos 12370 | . . . . . . . . . . 11
⊢ 0 <
2 | 
| 38 | 36, 37 | pm3.2i 470 | . . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 39 |  | lediv1 12134 | . . . . . . . . . 10
⊢ ((-π
∈ ℝ ∧ 𝐴
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (-π ≤
𝐴 ↔ (-π / 2) ≤
(𝐴 / 2))) | 
| 40 | 2, 38, 39 | mp3an13 1453 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (-π
≤ 𝐴 ↔ (-π / 2)
≤ (𝐴 /
2))) | 
| 41 |  | picn 26502 | . . . . . . . . . . 11
⊢ π
∈ ℂ | 
| 42 |  | 2cn 12342 | . . . . . . . . . . 11
⊢ 2 ∈
ℂ | 
| 43 |  | 2ne0 12371 | . . . . . . . . . . 11
⊢ 2 ≠
0 | 
| 44 |  | divneg 11960 | . . . . . . . . . . 11
⊢ ((π
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) =
(-π / 2)) | 
| 45 | 41, 42, 43, 44 | mp3an 1462 | . . . . . . . . . 10
⊢ -(π /
2) = (-π / 2) | 
| 46 | 45 | breq1i 5149 | . . . . . . . . 9
⊢ (-(π /
2) ≤ (𝐴 / 2) ↔
(-π / 2) ≤ (𝐴 /
2)) | 
| 47 | 40, 46 | bitr4di 289 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (-π
≤ 𝐴 ↔ -(π / 2)
≤ (𝐴 /
2))) | 
| 48 |  | lediv1 12134 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 ≤ π ↔ (𝐴 / 2) ≤ (π /
2))) | 
| 49 | 1, 38, 48 | mp3an23 1454 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ π ↔ (𝐴 / 2) ≤ (π /
2))) | 
| 50 | 47, 49 | anbi12d 632 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((-π
≤ 𝐴 ∧ 𝐴 ≤ π) ↔ (-(π / 2)
≤ (𝐴 / 2) ∧ (𝐴 / 2) ≤ (π /
2)))) | 
| 51 |  | rehalfcl 12495 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) | 
| 52 | 51 | rexrd 11312 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ*) | 
| 53 |  | halfpire 26507 | . . . . . . . . . . 11
⊢ (π /
2) ∈ ℝ | 
| 54 | 53 | renegcli 11571 | . . . . . . . . . 10
⊢ -(π /
2) ∈ ℝ | 
| 55 | 54 | rexri 11320 | . . . . . . . . 9
⊢ -(π /
2) ∈ ℝ* | 
| 56 | 53 | rexri 11320 | . . . . . . . . 9
⊢ (π /
2) ∈ ℝ* | 
| 57 |  | elicc4 13455 | . . . . . . . . 9
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*
∧ (𝐴 / 2) ∈
ℝ*) → ((𝐴 / 2) ∈ (-(π / 2)[,](π / 2))
↔ (-(π / 2) ≤ (𝐴
/ 2) ∧ (𝐴 / 2) ≤
(π / 2)))) | 
| 58 | 55, 56, 57 | mp3an12 1452 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ*
→ ((𝐴 / 2) ∈
(-(π / 2)[,](π / 2)) ↔ (-(π / 2) ≤ (𝐴 / 2) ∧ (𝐴 / 2) ≤ (π / 2)))) | 
| 59 | 52, 58 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴 / 2) ∈ (-(π /
2)[,](π / 2)) ↔ (-(π / 2) ≤ (𝐴 / 2) ∧ (𝐴 / 2) ≤ (π / 2)))) | 
| 60 | 50, 59 | bitr4d 282 | . . . . . 6
⊢ (𝐴 ∈ ℝ → ((-π
≤ 𝐴 ∧ 𝐴 ≤ π) ↔ (𝐴 / 2) ∈ (-(π /
2)[,](π / 2)))) | 
| 61 | 60 | biimpd 229 | . . . . 5
⊢ (𝐴 ∈ ℝ → ((-π
≤ 𝐴 ∧ 𝐴 ≤ π) → (𝐴 / 2) ∈ (-(π /
2)[,](π / 2)))) | 
| 62 | 61 | 3impib 1116 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ -π ≤
𝐴 ∧ 𝐴 ≤ π) → (𝐴 / 2) ∈ (-(π / 2)[,](π /
2))) | 
| 63 | 35, 62 | sylbi 217 | . . 3
⊢ (𝐴 ∈ (-π[,]π) →
(𝐴 / 2) ∈ (-(π /
2)[,](π / 2))) | 
| 64 |  | cosq14ge0 26554 | . . 3
⊢ ((𝐴 / 2) ∈ (-(π /
2)[,](π / 2)) → 0 ≤ (cos‘(𝐴 / 2))) | 
| 65 | 63, 64 | syl 17 | . 2
⊢ (𝐴 ∈ (-π[,]π) → 0
≤ (cos‘(𝐴 /
2))) | 
| 66 | 12, 33 | sqrtge0d 15460 | . 2
⊢ (𝐴 ∈ (-π[,]π) → 0
≤ (√‘((1 + (cos‘𝐴)) / 2))) | 
| 67 | 5 | recnd 11290 | . . 3
⊢ (𝐴 ∈ (-π[,]π) →
𝐴 ∈
ℂ) | 
| 68 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 69 |  | coscl 16164 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) | 
| 70 |  | addcl 11238 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → (1 +
(cos‘𝐴)) ∈
ℂ) | 
| 71 | 68, 69, 70 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (1 +
(cos‘𝐴)) ∈
ℂ) | 
| 72 | 71 | halfcld 12513 | . . . . 5
⊢ (𝐴 ∈ ℂ → ((1 +
(cos‘𝐴)) / 2) ∈
ℂ) | 
| 73 | 72 | sqsqrtd 15479 | . . . 4
⊢ (𝐴 ∈ ℂ →
((√‘((1 + (cos‘𝐴)) / 2))↑2) = ((1 + (cos‘𝐴)) / 2)) | 
| 74 |  | divcan2 11931 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐴 / 2)) = 𝐴) | 
| 75 | 42, 43, 74 | mp3an23 1454 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) | 
| 76 | 75 | fveq2d 6909 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = (cos‘𝐴)) | 
| 77 |  | halfcl 12494 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈
ℂ) | 
| 78 |  | cos2t 16215 | . . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) | 
| 79 | 77, 78 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(cos‘(2 · (𝐴 /
2))) = ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) | 
| 80 | 76, 79 | eqtr3d 2778 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) = ((2
· ((cos‘(𝐴 /
2))↑2)) − 1)) | 
| 81 | 80 | oveq2d 7448 | . . . . 5
⊢ (𝐴 ∈ ℂ → (1 +
(cos‘𝐴)) = (1 + ((2
· ((cos‘(𝐴 /
2))↑2)) − 1))) | 
| 82 | 81 | oveq1d 7447 | . . . 4
⊢ (𝐴 ∈ ℂ → ((1 +
(cos‘𝐴)) / 2) = ((1 +
((2 · ((cos‘(𝐴
/ 2))↑2)) − 1)) / 2)) | 
| 83 | 77 | coscld 16168 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(cos‘(𝐴 / 2)) ∈
ℂ) | 
| 84 | 83 | sqcld 14185 | . . . . 5
⊢ (𝐴 ∈ ℂ →
((cos‘(𝐴 /
2))↑2) ∈ ℂ) | 
| 85 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ ((cos‘(𝐴 / 2))↑2) ∈ ℂ) → (2
· ((cos‘(𝐴 /
2))↑2)) ∈ ℂ) | 
| 86 | 42, 85 | mpan 690 | . . . . . . . 8
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → (2 · ((cos‘(𝐴 / 2))↑2)) ∈
ℂ) | 
| 87 |  | pncan3 11517 | . . . . . . . 8
⊢ ((1
∈ ℂ ∧ (2 · ((cos‘(𝐴 / 2))↑2)) ∈ ℂ) → (1 +
((2 · ((cos‘(𝐴
/ 2))↑2)) − 1)) = (2 · ((cos‘(𝐴 / 2))↑2))) | 
| 88 | 68, 86, 87 | sylancr 587 | . . . . . . 7
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → (1 + ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) = (2
· ((cos‘(𝐴 /
2))↑2))) | 
| 89 | 88 | oveq1d 7447 | . . . . . 6
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → ((1 + ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) / 2)
= ((2 · ((cos‘(𝐴 / 2))↑2)) / 2)) | 
| 90 |  | divcan3 11949 | . . . . . . 7
⊢
((((cos‘(𝐴 /
2))↑2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2
· ((cos‘(𝐴 /
2))↑2)) / 2) = ((cos‘(𝐴 / 2))↑2)) | 
| 91 | 42, 43, 90 | mp3an23 1454 | . . . . . 6
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → ((2 · ((cos‘(𝐴 / 2))↑2)) / 2) = ((cos‘(𝐴 / 2))↑2)) | 
| 92 | 89, 91 | eqtrd 2776 | . . . . 5
⊢
(((cos‘(𝐴 /
2))↑2) ∈ ℂ → ((1 + ((2 · ((cos‘(𝐴 / 2))↑2)) − 1)) / 2)
= ((cos‘(𝐴 /
2))↑2)) | 
| 93 | 84, 92 | syl 17 | . . . 4
⊢ (𝐴 ∈ ℂ → ((1 + ((2
· ((cos‘(𝐴 /
2))↑2)) − 1)) / 2) = ((cos‘(𝐴 / 2))↑2)) | 
| 94 | 73, 82, 93 | 3eqtrrd 2781 | . . 3
⊢ (𝐴 ∈ ℂ →
((cos‘(𝐴 /
2))↑2) = ((√‘((1 + (cos‘𝐴)) / 2))↑2)) | 
| 95 | 67, 94 | syl 17 | . 2
⊢ (𝐴 ∈ (-π[,]π) →
((cos‘(𝐴 /
2))↑2) = ((√‘((1 + (cos‘𝐴)) / 2))↑2)) | 
| 96 | 7, 34, 65, 66, 95 | sq11d 14298 | 1
⊢ (𝐴 ∈ (-π[,]π) →
(cos‘(𝐴 / 2)) =
(√‘((1 + (cos‘𝐴)) / 2))) |