Proof of Theorem sincosq3sgn
| Step | Hyp | Ref
| Expression |
| 1 | | pire 26500 |
. . 3
⊢ π
∈ ℝ |
| 2 | | 3re 12346 |
. . . 4
⊢ 3 ∈
ℝ |
| 3 | | halfpire 26506 |
. . . 4
⊢ (π /
2) ∈ ℝ |
| 4 | 2, 3 | remulcli 11277 |
. . 3
⊢ (3
· (π / 2)) ∈ ℝ |
| 5 | | rexr 11307 |
. . . 4
⊢ (π
∈ ℝ → π ∈ ℝ*) |
| 6 | | rexr 11307 |
. . . 4
⊢ ((3
· (π / 2)) ∈ ℝ → (3 · (π / 2)) ∈
ℝ*) |
| 7 | | elioo2 13428 |
. . . 4
⊢ ((π
∈ ℝ* ∧ (3 · (π / 2)) ∈
ℝ*) → (𝐴 ∈ (π(,)(3 · (π / 2)))
↔ (𝐴 ∈ ℝ
∧ π < 𝐴 ∧
𝐴 < (3 · (π /
2))))) |
| 8 | 5, 6, 7 | syl2an 596 |
. . 3
⊢ ((π
∈ ℝ ∧ (3 · (π / 2)) ∈ ℝ) → (𝐴 ∈ (π(,)(3 ·
(π / 2))) ↔ (𝐴
∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < (3 · (π /
2))))) |
| 9 | 1, 4, 8 | mp2an 692 |
. 2
⊢ (𝐴 ∈ (π(,)(3 ·
(π / 2))) ↔ (𝐴
∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < (3 · (π /
2)))) |
| 10 | | pidiv2halves 26509 |
. . . . . . . . 9
⊢ ((π /
2) + (π / 2)) = π |
| 11 | 10 | breq1i 5150 |
. . . . . . . 8
⊢ (((π /
2) + (π / 2)) < 𝐴
↔ π < 𝐴) |
| 12 | | ltaddsub 11737 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((π / 2) + (π
/ 2)) < 𝐴 ↔ (π /
2) < (𝐴 − (π /
2)))) |
| 13 | 3, 3, 12 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (((π /
2) + (π / 2)) < 𝐴
↔ (π / 2) < (𝐴
− (π / 2)))) |
| 14 | 11, 13 | bitr3id 285 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (π
< 𝐴 ↔ (π / 2)
< (𝐴 − (π /
2)))) |
| 15 | | ltsubadd 11733 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ π ∈ ℝ) → ((𝐴 − (π / 2)) < π ↔ 𝐴 < (π + (π /
2)))) |
| 16 | 3, 1, 15 | mp3an23 1455 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < π
↔ 𝐴 < (π + (π
/ 2)))) |
| 17 | | df-3 12330 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
| 18 | 17 | oveq1i 7441 |
. . . . . . . . . 10
⊢ (3
· (π / 2)) = ((2 + 1) · (π / 2)) |
| 19 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 20 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 21 | 3 | recni 11275 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℂ |
| 22 | 19, 20, 21 | adddiri 11274 |
. . . . . . . . . 10
⊢ ((2 + 1)
· (π / 2)) = ((2 · (π / 2)) + (1 · (π /
2))) |
| 23 | 1 | recni 11275 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
| 24 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 25 | 23, 19, 24 | divcan2i 12010 |
. . . . . . . . . . 11
⊢ (2
· (π / 2)) = π |
| 26 | 21 | mullidi 11266 |
. . . . . . . . . . 11
⊢ (1
· (π / 2)) = (π / 2) |
| 27 | 25, 26 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((2
· (π / 2)) + (1 · (π / 2))) = (π + (π /
2)) |
| 28 | 18, 22, 27 | 3eqtrri 2770 |
. . . . . . . . 9
⊢ (π +
(π / 2)) = (3 · (π / 2)) |
| 29 | 28 | breq2i 5151 |
. . . . . . . 8
⊢ (𝐴 < (π + (π / 2)) ↔
𝐴 < (3 · (π /
2))) |
| 30 | 16, 29 | bitr2di 288 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 < (3 · (π / 2))
↔ (𝐴 − (π /
2)) < π)) |
| 31 | 14, 30 | anbi12d 632 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
↔ ((π / 2) < (𝐴
− (π / 2)) ∧ (𝐴 − (π / 2)) <
π))) |
| 32 | | resubcl 11573 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴
− (π / 2)) ∈ ℝ) |
| 33 | 3, 32 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℝ) |
| 34 | | sincosq2sgn 26541 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
((π / 2)(,)π) → (0 < (sin‘(𝐴 − (π / 2))) ∧
(cos‘(𝐴 − (π
/ 2))) < 0)) |
| 35 | | rexr 11307 |
. . . . . . . . . . 11
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
| 36 | | elioo2 13428 |
. . . . . . . . . . 11
⊢ (((π /
2) ∈ ℝ* ∧ π ∈ ℝ*) →
((𝐴 − (π / 2))
∈ ((π / 2)(,)π) ↔ ((𝐴 − (π / 2)) ∈ ℝ ∧
(π / 2) < (𝐴 −
(π / 2)) ∧ (𝐴
− (π / 2)) < π))) |
| 37 | 35, 5, 36 | syl2an 596 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ) → ((𝐴 − (π / 2)) ∈ ((π /
2)(,)π) ↔ ((𝐴
− (π / 2)) ∈ ℝ ∧ (π / 2) < (𝐴 − (π / 2)) ∧ (𝐴 − (π / 2)) <
π))) |
| 38 | 3, 1, 37 | mp2an 692 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
((π / 2)(,)π) ↔ ((𝐴 − (π / 2)) ∈ ℝ ∧
(π / 2) < (𝐴 −
(π / 2)) ∧ (𝐴
− (π / 2)) < π)) |
| 39 | | ancom 460 |
. . . . . . . . 9
⊢ ((0 <
(sin‘(𝐴 − (π
/ 2))) ∧ (cos‘(𝐴
− (π / 2))) < 0) ↔ ((cos‘(𝐴 − (π / 2))) < 0 ∧ 0 <
(sin‘(𝐴 − (π
/ 2))))) |
| 40 | 34, 38, 39 | 3imtr3i 291 |
. . . . . . . 8
⊢ (((𝐴 − (π / 2)) ∈
ℝ ∧ (π / 2) < (𝐴 − (π / 2)) ∧ (𝐴 − (π / 2)) < π)
→ ((cos‘(𝐴
− (π / 2))) < 0 ∧ 0 < (sin‘(𝐴 − (π / 2))))) |
| 41 | 33, 40 | syl3an1 1164 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
< (𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < π) → ((cos‘(𝐴 − (π / 2))) < 0 ∧ 0 <
(sin‘(𝐴 − (π
/ 2))))) |
| 42 | 41 | 3expib 1123 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (((π /
2) < (𝐴 − (π /
2)) ∧ (𝐴 − (π
/ 2)) < π) → ((cos‘(𝐴 − (π / 2))) < 0 ∧ 0 <
(sin‘(𝐴 − (π
/ 2)))))) |
| 43 | 31, 42 | sylbid 240 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((cos‘(𝐴
− (π / 2))) < 0 ∧ 0 < (sin‘(𝐴 − (π / 2)))))) |
| 44 | 33 | resincld 16179 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘(𝐴 − (π
/ 2))) ∈ ℝ) |
| 45 | 44 | lt0neg2d 11833 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘(𝐴 − (π
/ 2))) ↔ -(sin‘(𝐴 − (π / 2))) <
0)) |
| 46 | 45 | anbi2d 630 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(((cos‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (sin‘(𝐴 − (π / 2)))) ↔
((cos‘(𝐴 −
(π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
| 47 | 43, 46 | sylibd 239 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((cos‘(𝐴
− (π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
| 48 | | recn 11245 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 49 | | pncan3 11516 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) + (𝐴 − (π / 2))) = 𝐴) |
| 50 | 21, 48, 49 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π /
2) + (𝐴 − (π /
2))) = 𝐴) |
| 51 | 50 | fveq2d 6910 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (sin‘𝐴)) |
| 52 | 33 | recnd 11289 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℂ) |
| 53 | | sinhalfpip 26534 |
. . . . . . . 8
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (sin‘((π / 2) + (𝐴 − (π / 2)))) = (cos‘(𝐴 − (π /
2)))) |
| 54 | 52, 53 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘(𝐴 − (π / 2)))) |
| 55 | 51, 54 | eqtr3d 2779 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) =
(cos‘(𝐴 − (π
/ 2)))) |
| 56 | 55 | breq1d 5153 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((sin‘𝐴) < 0
↔ (cos‘(𝐴
− (π / 2))) < 0)) |
| 57 | 50 | fveq2d 6910 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘𝐴)) |
| 58 | | coshalfpip 26536 |
. . . . . . . 8
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (cos‘((π / 2) + (𝐴 − (π / 2)))) = -(sin‘(𝐴 − (π /
2)))) |
| 59 | 52, 58 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = -(sin‘(𝐴 − (π / 2)))) |
| 60 | 57, 59 | eqtr3d 2779 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) =
-(sin‘(𝐴 −
(π / 2)))) |
| 61 | 60 | breq1d 5153 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) < 0
↔ -(sin‘(𝐴
− (π / 2))) < 0)) |
| 62 | 56, 61 | anbi12d 632 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(((sin‘𝐴) < 0
∧ (cos‘𝐴) < 0)
↔ ((cos‘(𝐴
− (π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
| 63 | 47, 62 | sylibrd 259 |
. . 3
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((sin‘𝐴) <
0 ∧ (cos‘𝐴) <
0))) |
| 64 | 63 | 3impib 1117 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ π <
𝐴 ∧ 𝐴 < (3 · (π / 2))) →
((sin‘𝐴) < 0 ∧
(cos‘𝐴) <
0)) |
| 65 | 9, 64 | sylbi 217 |
1
⊢ (𝐴 ∈ (π(,)(3 ·
(π / 2))) → ((sin‘𝐴) < 0 ∧ (cos‘𝐴) < 0)) |