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