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⁡A2
3 recoscl ⊢A∈ℝ→cos⁡A∈ℝ
4 3 resqcld ⊢A∈ℝ→cos⁡A2∈ℝ
5 1 resqcld ⊢A∈ℝ→sin⁡A2∈ℝ
6 4 5 addge02d ⊢A∈ℝ→0≤sin⁡A2↔cos⁡A2≤sin⁡A2+cos⁡A2
7 2 6 mpbid ⊢A∈ℝ→cos⁡A2≤sin⁡A2+cos⁡A2
8 recn ⊢A∈ℝ→A∈ℂ
9 sincossq ⊢A∈ℂ→sin⁡A2+cos⁡A2=1
10 8 9 syl ⊢A∈ℝ→sin⁡A2+cos⁡A2=1
11 sq1 ⊢12=1
12 10 11 eqtr4di ⊢A∈ℝ→sin⁡A2+cos⁡A2=12
13 7 12 breqtrd ⊢A∈ℝ→cos⁡A2≤12
14 1re ⊢1∈ℝ
15 0le1 ⊢0≤1
16 lenegsq ⊢cos⁡A∈ℝ∧1∈ℝ∧0≤1→cos⁡A≤1∧−cos⁡A≤1↔cos⁡A2≤12
17 14 15 16 mp3an23 ⊢cos⁡A∈ℝ→cos⁡A≤1∧−cos⁡A≤1↔cos⁡A2≤12
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⁡A2≤12↔cos⁡A≤1∧−1≤cos⁡A
22 3 21 syl ⊢A∈ℝ→cos⁡A2≤12↔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