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