Metamath Proof Explorer


Theorem cosq14gt0

Description: The cosine of a number strictly between -upi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion cosq14gt0 ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 halfpire ( π / 2 ) ∈ ℝ
2 elioore ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℝ )
3 resubcl ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
4 1 2 3 sylancr ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
5 neghalfpirx - ( π / 2 ) ∈ ℝ*
6 1 rexri ( π / 2 ) ∈ ℝ*
7 elioo2 ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ - ( π / 2 ) < 𝐴𝐴 < ( π / 2 ) ) ) )
8 5 6 7 mp2an ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ - ( π / 2 ) < 𝐴𝐴 < ( π / 2 ) ) )
9 8 simp3bi ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 < ( π / 2 ) )
10 posdif ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) )
11 2 1 10 sylancl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) )
12 9 11 mpbid ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( ( π / 2 ) − 𝐴 ) )
13 picn π ∈ ℂ
14 halfcl ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
15 13 14 ax-mp ( π / 2 ) ∈ ℂ
16 15 negcli - ( π / 2 ) ∈ ℂ
17 13 15 negsubi ( π + - ( π / 2 ) ) = ( π − ( π / 2 ) )
18 pidiv2halves ( ( π / 2 ) + ( π / 2 ) ) = π
19 13 15 15 18 subaddrii ( π − ( π / 2 ) ) = ( π / 2 )
20 17 19 eqtri ( π + - ( π / 2 ) ) = ( π / 2 )
21 15 13 16 20 subaddrii ( ( π / 2 ) − π ) = - ( π / 2 )
22 8 simp2bi ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → - ( π / 2 ) < 𝐴 )
23 21 22 eqbrtrid ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − π ) < 𝐴 )
24 pire π ∈ ℝ
25 ltsub23 ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) )
26 1 24 25 mp3an13 ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) )
27 2 26 syl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( ( π / 2 ) − 𝐴 ) < π ↔ ( ( π / 2 ) − π ) < 𝐴 ) )
28 23 27 mpbird ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) < π )
29 0xr 0 ∈ ℝ*
30 24 rexri π ∈ ℝ*
31 elioo2 ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) ↔ ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 0 < ( ( π / 2 ) − 𝐴 ) ∧ ( ( π / 2 ) − 𝐴 ) < π ) ) )
32 29 30 31 mp2an ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) ↔ ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 0 < ( ( π / 2 ) − 𝐴 ) ∧ ( ( π / 2 ) − 𝐴 ) < π ) )
33 4 12 28 32 syl3anbrc ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) )
34 sinq12gt0 ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
35 33 34 syl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
36 2 recnd ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℂ )
37 sinhalfpim ( 𝐴 ∈ ℂ → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )
38 36 37 syl ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )
39 35 38 breqtrd ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ 𝐴 ) )