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 ⊢ A ∈ − π 2 π 2 → 0 < cos ⁡ A

Proof

Step Hyp Ref Expression
1 halfpire ⊢ π 2 ∈ ℝ
2 elioore ⊢ A ∈ − π 2 π 2 → A ∈ ℝ
3 resubcl ⊢ π 2 ∈ ℝ ∧ A ∈ ℝ → π 2 − A ∈ ℝ
4 1 2 3 sylancr ⊢ A ∈ − π 2 π 2 → π 2 − A ∈ ℝ
5 neghalfpirx ⊢ − π 2 ∈ ℝ *
6 1 rexri ⊢ π 2 ∈ ℝ *
7 elioo2 ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * → A ∈ − π 2 π 2 ↔ A ∈ ℝ ∧ − π 2 < A ∧ A < π 2
8 5 6 7 mp2an ⊢ A ∈ − π 2 π 2 ↔ A ∈ ℝ ∧ − π 2 < A ∧ A < π 2
9 8 simp3bi ⊢ A ∈ − π 2 π 2 → A < π 2
10 posdif ⊢ A ∈ ℝ ∧ π 2 ∈ ℝ → A < π 2 ↔ 0 < π 2 − A
11 2 1 10 sylancl ⊢ A ∈ − π 2 π 2 → A < π 2 ↔ 0 < π 2 − A
12 9 11 mpbid ⊢ A ∈ − π 2 π 2 → 0 < π 2 − A
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 ⊢ A ∈ − π 2 π 2 → − π 2 < A
23 21 22 eqbrtrid ⊢ A ∈ − π 2 π 2 → π 2 − π < A
24 pire ⊢ π ∈ ℝ
25 ltsub23 ⊢ π 2 ∈ ℝ ∧ A ∈ ℝ ∧ π ∈ ℝ → π 2 − A < π ↔ π 2 − π < A
26 1 24 25 mp3an13 ⊢ A ∈ ℝ → π 2 − A < π ↔ π 2 − π < A
27 2 26 syl ⊢ A ∈ − π 2 π 2 → π 2 − A < π ↔ π 2 − π < A
28 23 27 mpbird ⊢ A ∈ − π 2 π 2 → π 2 − A < π
29 0xr ⊢ 0 ∈ ℝ *
30 24 rexri ⊢ π ∈ ℝ *
31 elioo2 ⊢ 0 ∈ ℝ * ∧ π ∈ ℝ * → π 2 − A ∈ 0 π ↔ π 2 − A ∈ ℝ ∧ 0 < π 2 − A ∧ π 2 − A < π
32 29 30 31 mp2an ⊢ π 2 − A ∈ 0 π ↔ π 2 − A ∈ ℝ ∧ 0 < π 2 − A ∧ π 2 − A < π
33 4 12 28 32 syl3anbrc ⊢ A ∈ − π 2 π 2 → π 2 − A ∈ 0 π
34 sinq12gt0 ⊢ π 2 − A ∈ 0 π → 0 < sin ⁡ π 2 − A
35 33 34 syl ⊢ A ∈ − π 2 π 2 → 0 < sin ⁡ π 2 − A
36 2 recnd ⊢ A ∈ − π 2 π 2 → A ∈ ℂ
37 sinhalfpim ⊢ A ∈ ℂ → sin ⁡ π 2 − A = cos ⁡ A
38 36 37 syl ⊢ A ∈ − π 2 π 2 → sin ⁡ π 2 − A = cos ⁡ A
39 35 38 breqtrd ⊢ A ∈ − π 2 π 2 → 0 < cos ⁡ A