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 ) )