**Description:** The cosine of a real number is in the closed interval from -1 to 1.
(Contributed by Mario Carneiro, 12-May-2014)

Ref | Expression | ||
---|---|---|---|

Assertion | cosbnd2 | ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | recoscl | ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ ) | |

2 | cosbnd | ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) ) | |

3 | 2 | simpld | ⊢ ( 𝐴 ∈ ℝ → - 1 ≤ ( cos ‘ 𝐴 ) ) |

4 | 2 | simprd | ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ≤ 1 ) |

5 | neg1rr | ⊢ - 1 ∈ ℝ | |

6 | 1re | ⊢ 1 ∈ ℝ | |

7 | 5 6 | elicc2i | ⊢ ( ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) ) |

8 | 1 3 4 7 | syl3anbrc | ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) ) |