Metamath Proof Explorer

Theorem cosq14ge0

Description: The cosine of a number between -upi / 2 and pi / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Assertion cosq14ge0 ⊢ A ∈ − π 2 π 2 → 0 ≤ cos ⁡ A

Proof

Step Hyp Ref Expression
1 halfpire ⊢ π 2 ∈ ℝ
2 neghalfpire ⊢ − π 2 ∈ ℝ
3 2 1 elicc2i ⊢ A ∈ − π 2 π 2 ↔ A ∈ ℝ ∧ − π 2 ≤ A ∧ A ≤ π 2
4 3 simp1bi ⊢ A ∈ − π 2 π 2 → A ∈ ℝ
5 resubcl ⊢ π 2 ∈ ℝ ∧ A ∈ ℝ → π 2 − A ∈ ℝ
6 1 4 5 sylancr ⊢ A ∈ − π 2 π 2 → π 2 − A ∈ ℝ
7 3 simp3bi ⊢ A ∈ − π 2 π 2 → A ≤ π 2
8 subge0 ⊢ π 2 ∈ ℝ ∧ A ∈ ℝ → 0 ≤ π 2 − A ↔ A ≤ π 2
9 1 4 8 sylancr ⊢ A ∈ − π 2 π 2 → 0 ≤ π 2 − A ↔ A ≤ π 2
10 7 9 mpbird ⊢ A ∈ − π 2 π 2 → 0 ≤ π 2 − A
11 picn ⊢ π ∈ ℂ
12 halfcl ⊢ π ∈ ℂ → π 2 ∈ ℂ
13 11 12 ax-mp ⊢ π 2 ∈ ℂ
14 13 negcli ⊢ − π 2 ∈ ℂ
15 11 13 negsubi ⊢ π + − π 2 = π − π 2
16 pidiv2halves ⊢ π 2 + π 2 = π
17 11 13 13 16 subaddrii ⊢ π − π 2 = π 2
18 15 17 eqtri ⊢ π + − π 2 = π 2
19 13 11 14 18 subaddrii ⊢ π 2 − π = − π 2
20 3 simp2bi ⊢ A ∈ − π 2 π 2 → − π 2 ≤ A
21 19 20 eqbrtrid ⊢ A ∈ − π 2 π 2 → π 2 − π ≤ A
22 pire ⊢ π ∈ ℝ
23 suble ⊢ π 2 ∈ ℝ ∧ A ∈ ℝ ∧ π ∈ ℝ → π 2 − A ≤ π ↔ π 2 − π ≤ A
24 1 22 23 mp3an13 ⊢ A ∈ ℝ → π 2 − A ≤ π ↔ π 2 − π ≤ A
25 4 24 syl ⊢ A ∈ − π 2 π 2 → π 2 − A ≤ π ↔ π 2 − π ≤ A
26 21 25 mpbird ⊢ A ∈ − π 2 π 2 → π 2 − A ≤ π
27 0re ⊢ 0 ∈ ℝ
28 27 22 elicc2i ⊢ π 2 − A ∈ 0 π ↔ π 2 − A ∈ ℝ ∧ 0 ≤ π 2 − A ∧ π 2 − A ≤ π
29 6 10 26 28 syl3anbrc ⊢ A ∈ − π 2 π 2 → π 2 − A ∈ 0 π
30 sinq12ge0 ⊢ π 2 − A ∈ 0 π → 0 ≤ sin ⁡ π 2 − A
31 29 30 syl ⊢ A ∈ − π 2 π 2 → 0 ≤ sin ⁡ π 2 − A
32 4 recnd ⊢ A ∈ − π 2 π 2 → A ∈ ℂ
33 sinhalfpim ⊢ A ∈ ℂ → sin ⁡ π 2 − A = cos ⁡ A
34 32 33 syl ⊢ A ∈ − π 2 π 2 → sin ⁡ π 2 − A = cos ⁡ A
35 31 34 breqtrd ⊢ A ∈ − π 2 π 2 → 0 ≤ cos ⁡ A