Description: The closure of the secant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | seccl | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | secval | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) = ( 1 / ( cos ‘ 𝐴 ) ) ) | |
2 | coscl | ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ ) | |
3 | 2 | adantr | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ∈ ℂ ) |
4 | simpr | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ≠ 0 ) | |
5 | 3 4 | reccld | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cos ‘ 𝐴 ) ) ∈ ℂ ) |
6 | 1 5 | eqeltrd | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sec ‘ 𝐴 ) ∈ ℂ ) |