Metamath Proof Explorer


Theorem seccl

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

Ref Expression
Assertion seccl A cos A 0 sec A

Proof

Step Hyp Ref Expression
1 secval A cos A 0 sec A = 1 cos A
2 coscl A cos A
3 2 adantr A cos A 0 cos A
4 simpr A cos A 0 cos A 0
5 3 4 reccld A cos A 0 1 cos A
6 1 5 eqeltrd A cos A 0 sec A