Proof of Theorem sincosq2sgn
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | halfpire 26506 | . . 3
⊢ (π /
2) ∈ ℝ | 
| 2 |  | pire 26500 | . . 3
⊢ π
∈ ℝ | 
| 3 |  | rexr 11307 | . . . 4
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) | 
| 4 |  | rexr 11307 | . . . 4
⊢ (π
∈ ℝ → π ∈ ℝ*) | 
| 5 |  | elioo2 13428 | . . . 4
⊢ (((π /
2) ∈ ℝ* ∧ π ∈ ℝ*) →
(𝐴 ∈ ((π /
2)(,)π) ↔ (𝐴 ∈
ℝ ∧ (π / 2) < 𝐴 ∧ 𝐴 < π))) | 
| 6 | 3, 4, 5 | syl2an 596 | . . 3
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ) → (𝐴 ∈ ((π / 2)(,)π) ↔ (𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π))) | 
| 7 | 1, 2, 6 | mp2an 692 | . 2
⊢ (𝐴 ∈ ((π / 2)(,)π)
↔ (𝐴 ∈ ℝ
∧ (π / 2) < 𝐴
∧ 𝐴 <
π)) | 
| 8 |  | resubcl 11573 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴
− (π / 2)) ∈ ℝ) | 
| 9 | 1, 8 | mpan2 691 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℝ) | 
| 10 |  | 0xr 11308 | . . . . . . . . . 10
⊢ 0 ∈
ℝ* | 
| 11 | 1 | rexri 11319 | . . . . . . . . . 10
⊢ (π /
2) ∈ ℝ* | 
| 12 |  | elioo2 13428 | . . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
((𝐴 − (π / 2))
∈ (0(,)(π / 2)) ↔ ((𝐴 − (π / 2)) ∈ ℝ ∧ 0
< (𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < (π / 2)))) | 
| 13 | 10, 11, 12 | mp2an 692 | . . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
(0(,)(π / 2)) ↔ ((𝐴
− (π / 2)) ∈ ℝ ∧ 0 < (𝐴 − (π / 2)) ∧ (𝐴 − (π / 2)) < (π
/ 2))) | 
| 14 |  | sincosq1sgn 26540 | . . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
(0(,)(π / 2)) → (0 < (sin‘(𝐴 − (π / 2))) ∧ 0 <
(cos‘(𝐴 − (π
/ 2))))) | 
| 15 | 13, 14 | sylbir 235 | . . . . . . . 8
⊢ (((𝐴 − (π / 2)) ∈
ℝ ∧ 0 < (𝐴
− (π / 2)) ∧ (𝐴 − (π / 2)) < (π / 2)) →
(0 < (sin‘(𝐴
− (π / 2))) ∧ 0 < (cos‘(𝐴 − (π / 2))))) | 
| 16 | 9, 15 | syl3an1 1164 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
(𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < (π / 2)) → (0 < (sin‘(𝐴 − (π / 2))) ∧ 0 <
(cos‘(𝐴 − (π
/ 2))))) | 
| 17 | 16 | 3expib 1123 | . . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < (π / 2)) → (0 < (sin‘(𝐴 − (π / 2))) ∧ 0 <
(cos‘(𝐴 − (π
/ 2)))))) | 
| 18 |  | 0re 11263 | . . . . . . . . 9
⊢ 0 ∈
ℝ | 
| 19 |  | ltsub13 11744 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ ∧ (π / 2) ∈ ℝ) → (0 < (𝐴 − (π / 2)) ↔
(π / 2) < (𝐴 −
0))) | 
| 20 | 18, 1, 19 | mp3an13 1454 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 <
(𝐴 − (π / 2))
↔ (π / 2) < (𝐴
− 0))) | 
| 21 |  | recn 11245 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 22 | 21 | subid1d 11609 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − 0) = 𝐴) | 
| 23 | 22 | breq2d 5155 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π /
2) < (𝐴 − 0)
↔ (π / 2) < 𝐴)) | 
| 24 | 20, 23 | bitrd 279 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
(𝐴 − (π / 2))
↔ (π / 2) < 𝐴)) | 
| 25 |  | ltsubadd 11733 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ (π / 2) ∈ ℝ) → ((𝐴 − (π / 2)) < (π / 2) ↔
𝐴 < ((π / 2) + (π
/ 2)))) | 
| 26 | 1, 1, 25 | mp3an23 1455 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < (π
/ 2) ↔ 𝐴 < ((π /
2) + (π / 2)))) | 
| 27 |  | pidiv2halves 26509 | . . . . . . . . 9
⊢ ((π /
2) + (π / 2)) = π | 
| 28 | 27 | breq2i 5151 | . . . . . . . 8
⊢ (𝐴 < ((π / 2) + (π / 2))
↔ 𝐴 <
π) | 
| 29 | 26, 28 | bitrdi 287 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < (π
/ 2) ↔ 𝐴 <
π)) | 
| 30 | 24, 29 | anbi12d 632 | . . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < (π / 2)) ↔ ((π / 2) < 𝐴 ∧ 𝐴 < π))) | 
| 31 | 9 | resincld 16179 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘(𝐴 − (π
/ 2))) ∈ ℝ) | 
| 32 | 31 | lt0neg2d 11833 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘(𝐴 − (π
/ 2))) ↔ -(sin‘(𝐴 − (π / 2))) <
0)) | 
| 33 | 32 | anbi1d 631 | . . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 − (π
/ 2))) ∧ 0 < (cos‘(𝐴 − (π / 2)))) ↔
(-(sin‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) | 
| 34 | 17, 30, 33 | 3imtr3d 293 | . . . . 5
⊢ (𝐴 ∈ ℝ → (((π /
2) < 𝐴 ∧ 𝐴 < π) →
(-(sin‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) | 
| 35 | 1 | recni 11275 | . . . . . . . . . 10
⊢ (π /
2) ∈ ℂ | 
| 36 |  | pncan3 11516 | . . . . . . . . . 10
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) + (𝐴 − (π / 2))) = 𝐴) | 
| 37 | 35, 21, 36 | sylancr 587 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((π /
2) + (𝐴 − (π /
2))) = 𝐴) | 
| 38 | 37 | fveq2d 6910 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘𝐴)) | 
| 39 | 9 | recnd 11289 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℂ) | 
| 40 |  | coshalfpip 26536 | . . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (cos‘((π / 2) + (𝐴 − (π / 2)))) = -(sin‘(𝐴 − (π /
2)))) | 
| 41 | 39, 40 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = -(sin‘(𝐴 − (π / 2)))) | 
| 42 | 38, 41 | eqtr3d 2779 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) =
-(sin‘(𝐴 −
(π / 2)))) | 
| 43 | 42 | breq1d 5153 | . . . . . 6
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) < 0
↔ -(sin‘(𝐴
− (π / 2))) < 0)) | 
| 44 | 37 | fveq2d 6910 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (sin‘𝐴)) | 
| 45 |  | sinhalfpip 26534 | . . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (sin‘((π / 2) + (𝐴 − (π / 2)))) = (cos‘(𝐴 − (π /
2)))) | 
| 46 | 39, 45 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘(𝐴 − (π / 2)))) | 
| 47 | 44, 46 | eqtr3d 2779 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) =
(cos‘(𝐴 − (π
/ 2)))) | 
| 48 | 47 | breq2d 5155 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘𝐴) ↔ 0 <
(cos‘(𝐴 − (π
/ 2))))) | 
| 49 | 43, 48 | anbi12d 632 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(((cos‘𝐴) < 0
∧ 0 < (sin‘𝐴))
↔ (-(sin‘(𝐴
− (π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) | 
| 50 | 34, 49 | sylibrd 259 | . . . 4
⊢ (𝐴 ∈ ℝ → (((π /
2) < 𝐴 ∧ 𝐴 < π) →
((cos‘𝐴) < 0 ∧
0 < (sin‘𝐴)))) | 
| 51 | 50 | 3impib 1117 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π) →
((cos‘𝐴) < 0 ∧
0 < (sin‘𝐴))) | 
| 52 | 51 | ancomd 461 | . 2
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π) → (0 <
(sin‘𝐴) ∧
(cos‘𝐴) <
0)) | 
| 53 | 7, 52 | sylbi 217 | 1
⊢ (𝐴 ∈ ((π / 2)(,)π)
→ (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0)) |