Proof of Theorem sincosq3sgn
Step | Hyp | Ref
| Expression |
1 | | pire 25216 |
. . 3
⊢ π
∈ ℝ |
2 | | 3re 11809 |
. . . 4
⊢ 3 ∈
ℝ |
3 | | halfpire 25222 |
. . . 4
⊢ (π /
2) ∈ ℝ |
4 | 2, 3 | remulcli 10748 |
. . 3
⊢ (3
· (π / 2)) ∈ ℝ |
5 | | rexr 10778 |
. . . 4
⊢ (π
∈ ℝ → π ∈ ℝ*) |
6 | | rexr 10778 |
. . . 4
⊢ ((3
· (π / 2)) ∈ ℝ → (3 · (π / 2)) ∈
ℝ*) |
7 | | elioo2 12875 |
. . . 4
⊢ ((π
∈ ℝ* ∧ (3 · (π / 2)) ∈
ℝ*) → (𝐴 ∈ (π(,)(3 · (π / 2)))
↔ (𝐴 ∈ ℝ
∧ π < 𝐴 ∧
𝐴 < (3 · (π /
2))))) |
8 | 5, 6, 7 | syl2an 599 |
. . 3
⊢ ((π
∈ ℝ ∧ (3 · (π / 2)) ∈ ℝ) → (𝐴 ∈ (π(,)(3 ·
(π / 2))) ↔ (𝐴
∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < (3 · (π /
2))))) |
9 | 1, 4, 8 | mp2an 692 |
. 2
⊢ (𝐴 ∈ (π(,)(3 ·
(π / 2))) ↔ (𝐴
∈ ℝ ∧ π < 𝐴 ∧ 𝐴 < (3 · (π /
2)))) |
10 | | pidiv2halves 25225 |
. . . . . . . . 9
⊢ ((π /
2) + (π / 2)) = π |
11 | 10 | breq1i 5047 |
. . . . . . . 8
⊢ (((π /
2) + (π / 2)) < 𝐴
↔ π < 𝐴) |
12 | | ltaddsub 11205 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((π / 2) + (π
/ 2)) < 𝐴 ↔ (π /
2) < (𝐴 − (π /
2)))) |
13 | 3, 3, 12 | mp3an12 1452 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (((π /
2) + (π / 2)) < 𝐴
↔ (π / 2) < (𝐴
− (π / 2)))) |
14 | 11, 13 | bitr3id 288 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (π
< 𝐴 ↔ (π / 2)
< (𝐴 − (π /
2)))) |
15 | | ltsubadd 11201 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ π ∈ ℝ) → ((𝐴 − (π / 2)) < π ↔ 𝐴 < (π + (π /
2)))) |
16 | 3, 1, 15 | mp3an23 1454 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < π
↔ 𝐴 < (π + (π
/ 2)))) |
17 | | df-3 11793 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
18 | 17 | oveq1i 7193 |
. . . . . . . . . 10
⊢ (3
· (π / 2)) = ((2 + 1) · (π / 2)) |
19 | | 2cn 11804 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
20 | | ax-1cn 10686 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
21 | 3 | recni 10746 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℂ |
22 | 19, 20, 21 | adddiri 10745 |
. . . . . . . . . 10
⊢ ((2 + 1)
· (π / 2)) = ((2 · (π / 2)) + (1 · (π /
2))) |
23 | 1 | recni 10746 |
. . . . . . . . . . . 12
⊢ π
∈ ℂ |
24 | | 2ne0 11833 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
25 | 23, 19, 24 | divcan2i 11474 |
. . . . . . . . . . 11
⊢ (2
· (π / 2)) = π |
26 | 21 | mulid2i 10737 |
. . . . . . . . . . 11
⊢ (1
· (π / 2)) = (π / 2) |
27 | 25, 26 | oveq12i 7195 |
. . . . . . . . . 10
⊢ ((2
· (π / 2)) + (1 · (π / 2))) = (π + (π /
2)) |
28 | 18, 22, 27 | 3eqtrri 2767 |
. . . . . . . . 9
⊢ (π +
(π / 2)) = (3 · (π / 2)) |
29 | 28 | breq2i 5048 |
. . . . . . . 8
⊢ (𝐴 < (π + (π / 2)) ↔
𝐴 < (3 · (π /
2))) |
30 | 16, 29 | bitr2di 291 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 < (3 · (π / 2))
↔ (𝐴 − (π /
2)) < π)) |
31 | 14, 30 | anbi12d 634 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
↔ ((π / 2) < (𝐴
− (π / 2)) ∧ (𝐴 − (π / 2)) <
π))) |
32 | | resubcl 11041 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴
− (π / 2)) ∈ ℝ) |
33 | 3, 32 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℝ) |
34 | | sincosq2sgn 25257 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
((π / 2)(,)π) → (0 < (sin‘(𝐴 − (π / 2))) ∧
(cos‘(𝐴 − (π
/ 2))) < 0)) |
35 | | rexr 10778 |
. . . . . . . . . . 11
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
36 | | elioo2 12875 |
. . . . . . . . . . 11
⊢ (((π /
2) ∈ ℝ* ∧ π ∈ ℝ*) →
((𝐴 − (π / 2))
∈ ((π / 2)(,)π) ↔ ((𝐴 − (π / 2)) ∈ ℝ ∧
(π / 2) < (𝐴 −
(π / 2)) ∧ (𝐴
− (π / 2)) < π))) |
37 | 35, 5, 36 | syl2an 599 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ) → ((𝐴 − (π / 2)) ∈ ((π /
2)(,)π) ↔ ((𝐴
− (π / 2)) ∈ ℝ ∧ (π / 2) < (𝐴 − (π / 2)) ∧ (𝐴 − (π / 2)) <
π))) |
38 | 3, 1, 37 | mp2an 692 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
((π / 2)(,)π) ↔ ((𝐴 − (π / 2)) ∈ ℝ ∧
(π / 2) < (𝐴 −
(π / 2)) ∧ (𝐴
− (π / 2)) < π)) |
39 | | ancom 464 |
. . . . . . . . 9
⊢ ((0 <
(sin‘(𝐴 − (π
/ 2))) ∧ (cos‘(𝐴
− (π / 2))) < 0) ↔ ((cos‘(𝐴 − (π / 2))) < 0 ∧ 0 <
(sin‘(𝐴 − (π
/ 2))))) |
40 | 34, 38, 39 | 3imtr3i 294 |
. . . . . . . 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 243 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((cos‘(𝐴
− (π / 2))) < 0 ∧ 0 < (sin‘(𝐴 − (π / 2)))))) |
44 | 33 | resincld 15601 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘(𝐴 − (π
/ 2))) ∈ ℝ) |
45 | 44 | lt0neg2d 11301 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘(𝐴 − (π
/ 2))) ↔ -(sin‘(𝐴 − (π / 2))) <
0)) |
46 | 45 | anbi2d 632 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(((cos‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (sin‘(𝐴 − (π / 2)))) ↔
((cos‘(𝐴 −
(π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
47 | 43, 46 | sylibd 242 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((cos‘(𝐴
− (π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
48 | | recn 10718 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
49 | | pncan3 10985 |
. . . . . . . . 9
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) + (𝐴 − (π / 2))) = 𝐴) |
50 | 21, 48, 49 | sylancr 590 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π /
2) + (𝐴 − (π /
2))) = 𝐴) |
51 | 50 | fveq2d 6691 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (sin‘𝐴)) |
52 | 33 | recnd 10760 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℂ) |
53 | | sinhalfpip 25250 |
. . . . . . . 8
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (sin‘((π / 2) + (𝐴 − (π / 2)))) = (cos‘(𝐴 − (π /
2)))) |
54 | 52, 53 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘(𝐴 − (π / 2)))) |
55 | 51, 54 | eqtr3d 2776 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) =
(cos‘(𝐴 − (π
/ 2)))) |
56 | 55 | breq1d 5050 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((sin‘𝐴) < 0
↔ (cos‘(𝐴
− (π / 2))) < 0)) |
57 | 50 | fveq2d 6691 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘𝐴)) |
58 | | coshalfpip 25252 |
. . . . . . . 8
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (cos‘((π / 2) + (𝐴 − (π / 2)))) = -(sin‘(𝐴 − (π /
2)))) |
59 | 52, 58 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = -(sin‘(𝐴 − (π / 2)))) |
60 | 57, 59 | eqtr3d 2776 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) =
-(sin‘(𝐴 −
(π / 2)))) |
61 | 60 | breq1d 5050 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) < 0
↔ -(sin‘(𝐴
− (π / 2))) < 0)) |
62 | 56, 61 | anbi12d 634 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(((sin‘𝐴) < 0
∧ (cos‘𝐴) < 0)
↔ ((cos‘(𝐴
− (π / 2))) < 0 ∧ -(sin‘(𝐴 − (π / 2))) <
0))) |
63 | 47, 62 | sylibrd 262 |
. . 3
⊢ (𝐴 ∈ ℝ → ((π
< 𝐴 ∧ 𝐴 < (3 · (π / 2)))
→ ((sin‘𝐴) <
0 ∧ (cos‘𝐴) <
0))) |
64 | 63 | 3impib 1117 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ π <
𝐴 ∧ 𝐴 < (3 · (π / 2))) →
((sin‘𝐴) < 0 ∧
(cos‘𝐴) <
0)) |
65 | 9, 64 | sylbi 220 |
1
⊢ (𝐴 ∈ (π(,)(3 ·
(π / 2))) → ((sin‘𝐴) < 0 ∧ (cos‘𝐴) < 0)) |