Metamath Proof Explorer

Theorem sincosq2sgn

Description: The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq2sgn ( 𝐴 ∈ ( ( π / 2 ) (,) π ) → ( 0 < ( sin ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 halfpire ⊢ ( π / 2 ) ∈ ℝ
2 pire ⊢ π ∈ ℝ
3 rexr ⊢ ( ( π / 2 ) ∈ ℝ → ( π / 2 ) ∈ ℝ* )
4 rexr ⊢ ( π ∈ ℝ → π ∈ ℝ* )
5 elioo2 ⊢ ( ( ( π / 2 ) ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝐴 ∈ ( ( π / 2 ) (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) ) )
6 3 4 5 syl2an ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ π ∈ ℝ ) → ( 𝐴 ∈ ( ( π / 2 ) (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) ) )
7 1 2 6 mp2an ⊢ ( 𝐴 ∈ ( ( π / 2 ) (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) )
8 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
9 1 8 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℝ )
10 0xr ⊢ 0 ∈ ℝ*
11 1 rexri ⊢ ( π / 2 ) ∈ ℝ*
12 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( 𝐴 − ( π / 2 ) ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) ) )
13 10 11 12 mp2an ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( 0 (,) ( π / 2 ) ) ↔ ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) )
14 sincosq1sgn ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
15 13 14 sylbir ⊢ ( ( ( 𝐴 − ( π / 2 ) ) ∈ ℝ ∧ 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
16 9 15 syl3an1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
17 16 3expib ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
18 0re ⊢ 0 ∈ ℝ
19 ltsub13 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 0 < ( 𝐴 − ( π / 2 ) ) ↔ ( π / 2 ) < ( 𝐴 − 0 ) ) )
20 18 1 19 mp3an13 ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( 𝐴 − ( π / 2 ) ) ↔ ( π / 2 ) < ( 𝐴 − 0 ) ) )
21 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
22 21 subid1d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 0 ) = 𝐴 )
23 22 breq2d ⊢ ( 𝐴 ∈ ℝ → ( ( π / 2 ) < ( 𝐴 − 0 ) ↔ ( π / 2 ) < 𝐴 ) )
24 20 23 bitrd ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( 𝐴 − ( π / 2 ) ) ↔ ( π / 2 ) < 𝐴 ) )
25 ltsubadd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ↔ 𝐴 < ( ( π / 2 ) + ( π / 2 ) ) ) )
26 1 1 25 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ↔ 𝐴 < ( ( π / 2 ) + ( π / 2 ) ) ) )
27 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
28 27 breq2i ⊢ ( 𝐴 < ( ( π / 2 ) + ( π / 2 ) ) ↔ 𝐴 < π )
29 26 28 bitrdi ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ↔ 𝐴 < π ) )
30 24 29 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( 𝐴 − ( π / 2 ) ) ∧ ( 𝐴 − ( π / 2 ) ) < ( π / 2 ) ) ↔ ( ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) ) )
31 9 resincld ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∈ ℝ )
32 31 lt0neg2d ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ↔ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
33 32 anbi1d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) ↔ ( - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
34 17 30 33 3imtr3d ⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) → ( - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
35 1 recni ⊢ ( π / 2 ) ∈ ℂ
36 pncan3 ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
37 35 21 36 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) = 𝐴 )
38 37 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ 𝐴 ) )
39 9 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( π / 2 ) ) ∈ ℂ )
40 coshalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
41 39 40 syl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
42 38 41 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) )
43 42 breq1d ⊢ ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) < 0 ↔ - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ) )
44 37 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( sin ‘ 𝐴 ) )
45 sinhalfpip ⊢ ( ( 𝐴 − ( π / 2 ) ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
46 39 45 syl ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) + ( 𝐴 − ( π / 2 ) ) ) ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
47 44 46 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) )
48 47 breq2d ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( sin ‘ 𝐴 ) ↔ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) )
49 43 48 anbi12d ⊢ ( 𝐴 ∈ ℝ → ( ( ( cos ‘ 𝐴 ) < 0 ∧ 0 < ( sin ‘ 𝐴 ) ) ↔ ( - ( sin ‘ ( 𝐴 − ( π / 2 ) ) ) < 0 ∧ 0 < ( cos ‘ ( 𝐴 − ( π / 2 ) ) ) ) ) )
50 34 49 sylibrd ⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) → ( ( cos ‘ 𝐴 ) < 0 ∧ 0 < ( sin ‘ 𝐴 ) ) ) )
51 50 3impib ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) → ( ( cos ‘ 𝐴 ) < 0 ∧ 0 < ( sin ‘ 𝐴 ) ) )
52 51 ancomd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) < 𝐴 ∧ 𝐴 < π ) → ( 0 < ( sin ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 0 ) )
53 7 52 sylbi ⊢ ( 𝐴 ∈ ( ( π / 2 ) (,) π ) → ( 0 < ( sin ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) < 0 ) )