Metamath Proof Explorer

Theorem cosbnd

Description: The cosine of a real number lies between -1 and 1. Equation 18 of Gleason p. 311. (Contributed by NM, 16-Jan-2006)

Ref Expression
Assertion cosbnd ⊢ A ∈ ℝ → − 1 ≤ cos ⁡ A ∧ cos ⁡ A ≤ 1

Proof

Step Hyp Ref Expression
1 resincl ⊢ A ∈ ℝ → sin ⁡ A ∈ ℝ
2 1 sqge0d ⊢ A ∈ ℝ → 0 ≤ sin ⁡ A 2
3 recoscl ⊢ A ∈ ℝ → cos ⁡ A ∈ ℝ
4 3 resqcld ⊢ A ∈ ℝ → cos ⁡ A 2 ∈ ℝ
5 1 resqcld ⊢ A ∈ ℝ → sin ⁡ A 2 ∈ ℝ
6 4 5 addge02d ⊢ A ∈ ℝ → 0 ≤ sin ⁡ A 2 ↔ cos ⁡ A 2 ≤ sin ⁡ A 2 + cos ⁡ A 2
7 2 6 mpbid ⊢ A ∈ ℝ → cos ⁡ A 2 ≤ sin ⁡ A 2 + cos ⁡ A 2
8 recn ⊢ A ∈ ℝ → A ∈ ℂ
9 sincossq ⊢ A ∈ ℂ → sin ⁡ A 2 + cos ⁡ A 2 = 1
10 8 9 syl ⊢ A ∈ ℝ → sin ⁡ A 2 + cos ⁡ A 2 = 1
11 sq1 ⊢ 1 2 = 1
12 10 11 eqtr4di ⊢ A ∈ ℝ → sin ⁡ A 2 + cos ⁡ A 2 = 1 2
13 7 12 breqtrd ⊢ A ∈ ℝ → cos ⁡ A 2 ≤ 1 2
14 1re ⊢ 1 ∈ ℝ
15 0le1 ⊢ 0 ≤ 1
16 lenegsq ⊢ cos ⁡ A ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1 → cos ⁡ A ≤ 1 ∧ − cos ⁡ A ≤ 1 ↔ cos ⁡ A 2 ≤ 1 2
17 14 15 16 mp3an23 ⊢ cos ⁡ A ∈ ℝ → cos ⁡ A ≤ 1 ∧ − cos ⁡ A ≤ 1 ↔ cos ⁡ A 2 ≤ 1 2
18 lenegcon1 ⊢ cos ⁡ A ∈ ℝ ∧ 1 ∈ ℝ → − cos ⁡ A ≤ 1 ↔ − 1 ≤ cos ⁡ A
19 14 18 mpan2 ⊢ cos ⁡ A ∈ ℝ → − cos ⁡ A ≤ 1 ↔ − 1 ≤ cos ⁡ A
20 19 anbi2d ⊢ cos ⁡ A ∈ ℝ → cos ⁡ A ≤ 1 ∧ − cos ⁡ A ≤ 1 ↔ cos ⁡ A ≤ 1 ∧ − 1 ≤ cos ⁡ A
21 17 20 bitr3d ⊢ cos ⁡ A ∈ ℝ → cos ⁡ A 2 ≤ 1 2 ↔ cos ⁡ A ≤ 1 ∧ − 1 ≤ cos ⁡ A
22 3 21 syl ⊢ A ∈ ℝ → cos ⁡ A 2 ≤ 1 2 ↔ cos ⁡ A ≤ 1 ∧ − 1 ≤ cos ⁡ A
23 13 22 mpbid ⊢ A ∈ ℝ → cos ⁡ A ≤ 1 ∧ − 1 ≤ cos ⁡ A
24 23 ancomd ⊢ A ∈ ℝ → − 1 ≤ cos ⁡ A ∧ cos ⁡ A ≤ 1