Metamath Proof Explorer


Theorem reseccl

Description: The closure of the secant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014)

Ref Expression
Assertion reseccl ( ( 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 secval ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) = ( 1 / ( cos ‘ 𝐴 ) ) )
3 1 2 sylan ( ( 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) = ( 1 / ( cos ‘ 𝐴 ) ) )
4 recoscl ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
5 1red ( 𝐴 ∈ ℝ → 1 ∈ ℝ )
6 redivcl ( ( 1 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cos ‘ 𝐴 ) ) ∈ ℝ )
7 5 6 syl3an1 ( ( 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cos ‘ 𝐴 ) ) ∈ ℝ )
8 4 7 syl3an2 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cos ‘ 𝐴 ) ) ∈ ℝ )
9 8 3anidm12 ( ( 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cos ‘ 𝐴 ) ) ∈ ℝ )
10 3 9 eqeltrd ( ( 𝐴 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) ∈ ℝ )