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 ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 halfpire ⊢ ( π / 2 ) ∈ ℝ
2 neghalfpire ⊢ - ( π / 2 ) ∈ ℝ
3 2 1 elicc2i ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( 𝐴 ∈ ℝ ∧ - ( π / 2 ) ≤ 𝐴 ∧ 𝐴 ≤ ( π / 2 ) ) )
4 3 simp1bi ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐴 ∈ ℝ )
5 resubcl ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
6 1 4 5 sylancr ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
7 3 simp3bi ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐴 ≤ ( π / 2 ) )
8 subge0 ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ ( ( π / 2 ) − 𝐴 ) ↔ 𝐴 ≤ ( π / 2 ) ) )
9 1 4 8 sylancr ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( 0 ≤ ( ( π / 2 ) − 𝐴 ) ↔ 𝐴 ≤ ( π / 2 ) ) )
10 7 9 mpbird ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( ( π / 2 ) − 𝐴 ) )
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 ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → - ( π / 2 ) ≤ 𝐴 )
21 19 20 eqbrtrid ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − π ) ≤ 𝐴 )
22 pire ⊢ π ∈ ℝ
23 suble ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( π / 2 ) − 𝐴 ) ≤ π ↔ ( ( π / 2 ) − π ) ≤ 𝐴 ) )
24 1 22 23 mp3an13 ⊢ ( 𝐴 ∈ ℝ → ( ( ( π / 2 ) − 𝐴 ) ≤ π ↔ ( ( π / 2 ) − π ) ≤ 𝐴 ) )
25 4 24 syl ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( ( π / 2 ) − 𝐴 ) ≤ π ↔ ( ( π / 2 ) − π ) ≤ 𝐴 ) )
26 21 25 mpbird ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ≤ π )
27 0re ⊢ 0 ∈ ℝ
28 27 22 elicc2i ⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) ↔ ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 0 ≤ ( ( π / 2 ) − 𝐴 ) ∧ ( ( π / 2 ) − 𝐴 ) ≤ π ) )
29 6 10 26 28 syl3anbrc ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) )
30 sinq12ge0 ⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) → 0 ≤ ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
31 29 30 syl ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
32 4 recnd ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐴 ∈ ℂ )
33 sinhalfpim ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )
34 32 33 syl ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = ( cos ‘ 𝐴 ) )
35 31 34 breqtrd ⊢ ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ 𝐴 ) )