Proof of Theorem sincosq2sgn
Step | Hyp | Ref
| Expression |
1 | | halfpire 25221 |
. . 3
⊢ (π /
2) ∈ ℝ |
2 | | pire 25215 |
. . 3
⊢ π
∈ ℝ |
3 | | rexr 10777 |
. . . 4
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈
ℝ*) |
4 | | rexr 10777 |
. . . 4
⊢ (π
∈ ℝ → π ∈ ℝ*) |
5 | | elioo2 12874 |
. . . 4
⊢ (((π /
2) ∈ ℝ* ∧ π ∈ ℝ*) →
(𝐴 ∈ ((π /
2)(,)π) ↔ (𝐴 ∈
ℝ ∧ (π / 2) < 𝐴 ∧ 𝐴 < π))) |
6 | 3, 4, 5 | syl2an 599 |
. . 3
⊢ (((π /
2) ∈ ℝ ∧ π ∈ ℝ) → (𝐴 ∈ ((π / 2)(,)π) ↔ (𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π))) |
7 | 1, 2, 6 | mp2an 692 |
. 2
⊢ (𝐴 ∈ ((π / 2)(,)π)
↔ (𝐴 ∈ ℝ
∧ (π / 2) < 𝐴
∧ 𝐴 <
π)) |
8 | | resubcl 11040 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴
− (π / 2)) ∈ ℝ) |
9 | 1, 8 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℝ) |
10 | | 0xr 10778 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
11 | 1 | rexri 10789 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℝ* |
12 | | elioo2 12874 |
. . . . . . . . . 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 25255 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
(0(,)(π / 2)) → (0 < (sin‘(𝐴 − (π / 2))) ∧ 0 <
(cos‘(𝐴 − (π
/ 2))))) |
15 | 13, 14 | sylbir 238 |
. . . . . . . 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 10733 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
19 | | ltsub13 11211 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ ∧ (π / 2) ∈ ℝ) → (0 < (𝐴 − (π / 2)) ↔
(π / 2) < (𝐴 −
0))) |
20 | 18, 1, 19 | mp3an13 1453 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 <
(𝐴 − (π / 2))
↔ (π / 2) < (𝐴
− 0))) |
21 | | recn 10717 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
22 | 21 | subid1d 11076 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − 0) = 𝐴) |
23 | 22 | breq2d 5052 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π /
2) < (𝐴 − 0)
↔ (π / 2) < 𝐴)) |
24 | 20, 23 | bitrd 282 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
(𝐴 − (π / 2))
↔ (π / 2) < 𝐴)) |
25 | | ltsubadd 11200 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ ∧ (π / 2) ∈ ℝ) → ((𝐴 − (π / 2)) < (π / 2) ↔
𝐴 < ((π / 2) + (π
/ 2)))) |
26 | 1, 1, 25 | mp3an23 1454 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < (π
/ 2) ↔ 𝐴 < ((π /
2) + (π / 2)))) |
27 | | pidiv2halves 25224 |
. . . . . . . . 9
⊢ ((π /
2) + (π / 2)) = π |
28 | 27 | breq2i 5048 |
. . . . . . . 8
⊢ (𝐴 < ((π / 2) + (π / 2))
↔ 𝐴 <
π) |
29 | 26, 28 | bitrdi 290 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐴 − (π / 2)) < (π
/ 2) ↔ 𝐴 <
π)) |
30 | 24, 29 | anbi12d 634 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(𝐴 − (π / 2))
∧ (𝐴 − (π /
2)) < (π / 2)) ↔ ((π / 2) < 𝐴 ∧ 𝐴 < π))) |
31 | 9 | resincld 15600 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘(𝐴 − (π
/ 2))) ∈ ℝ) |
32 | 31 | lt0neg2d 11300 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘(𝐴 − (π
/ 2))) ↔ -(sin‘(𝐴 − (π / 2))) <
0)) |
33 | 32 | anbi1d 633 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 − (π
/ 2))) ∧ 0 < (cos‘(𝐴 − (π / 2)))) ↔
(-(sin‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) |
34 | 17, 30, 33 | 3imtr3d 296 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (((π /
2) < 𝐴 ∧ 𝐴 < π) →
(-(sin‘(𝐴 −
(π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) |
35 | 1 | recni 10745 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℂ |
36 | | pncan3 10984 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℂ ∧ 𝐴
∈ ℂ) → ((π / 2) + (𝐴 − (π / 2))) = 𝐴) |
37 | 35, 21, 36 | sylancr 590 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((π /
2) + (𝐴 − (π /
2))) = 𝐴) |
38 | 37 | fveq2d 6690 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘𝐴)) |
39 | 9 | recnd 10759 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 − (π / 2)) ∈
ℂ) |
40 | | coshalfpip 25251 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (cos‘((π / 2) + (𝐴 − (π / 2)))) = -(sin‘(𝐴 − (π /
2)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(cos‘((π / 2) + (𝐴
− (π / 2)))) = -(sin‘(𝐴 − (π / 2)))) |
42 | 38, 41 | eqtr3d 2776 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(cos‘𝐴) =
-(sin‘(𝐴 −
(π / 2)))) |
43 | 42 | breq1d 5050 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
((cos‘𝐴) < 0
↔ -(sin‘(𝐴
− (π / 2))) < 0)) |
44 | 37 | fveq2d 6690 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (sin‘𝐴)) |
45 | | sinhalfpip 25249 |
. . . . . . . . 9
⊢ ((𝐴 − (π / 2)) ∈
ℂ → (sin‘((π / 2) + (𝐴 − (π / 2)))) = (cos‘(𝐴 − (π /
2)))) |
46 | 39, 45 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) + (𝐴
− (π / 2)))) = (cos‘(𝐴 − (π / 2)))) |
47 | 44, 46 | eqtr3d 2776 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) =
(cos‘(𝐴 − (π
/ 2)))) |
48 | 47 | breq2d 5052 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
(sin‘𝐴) ↔ 0 <
(cos‘(𝐴 − (π
/ 2))))) |
49 | 43, 48 | anbi12d 634 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(((cos‘𝐴) < 0
∧ 0 < (sin‘𝐴))
↔ (-(sin‘(𝐴
− (π / 2))) < 0 ∧ 0 < (cos‘(𝐴 − (π / 2)))))) |
50 | 34, 49 | sylibrd 262 |
. . . 4
⊢ (𝐴 ∈ ℝ → (((π /
2) < 𝐴 ∧ 𝐴 < π) →
((cos‘𝐴) < 0 ∧
0 < (sin‘𝐴)))) |
51 | 50 | 3impib 1117 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π) →
((cos‘𝐴) < 0 ∧
0 < (sin‘𝐴))) |
52 | 51 | ancomd 465 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
< 𝐴 ∧ 𝐴 < π) → (0 <
(sin‘𝐴) ∧
(cos‘𝐴) <
0)) |
53 | 7, 52 | sylbi 220 |
1
⊢ (𝐴 ∈ ((π / 2)(,)π)
→ (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0)) |