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 e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		secval	|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )
2		coscl	|- ( A e. CC -> ( cos ` A ) e. CC )
3	2	adantr	|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) e. CC )
4		simpr	|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) =/= 0 )
5	3 4	reccld	|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 / ( cos ` A ) ) e. CC )
6	1 5	eqeltrd	|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) e. CC )