Theorem retanhcl

Description: The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	retanhcl	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2		recn	|- ( A e. RR -> A e. CC )
3		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4	1 2 3	sylancr	|- ( A e. RR -> ( _i x. A ) e. CC )
5		rpcoshcl	|- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR+ )
6	5	rpne0d	|- ( A e. RR -> ( cos ` ( _i x. A ) ) =/= 0 )
7		tanval	|- ( ( ( _i x. A ) e. CC /\ ( cos ` ( _i x. A ) ) =/= 0 ) -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
8	4 6 7	syl2anc	|- ( A e. RR -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
9	8	oveq1d	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) )
10	4	sincld	|- ( A e. RR -> ( sin ` ( _i x. A ) ) e. CC )
11		recoshcl	|- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR )
12	11	recnd	|- ( A e. RR -> ( cos ` ( _i x. A ) ) e. CC )
13	1	a1i	|- ( A e. RR -> _i e. CC )
14		ine0	|- _i =/= 0
15	14	a1i	|- ( A e. RR -> _i =/= 0 )
16	10 12 13 6 15	divdiv32d	|- ( A e. RR -> ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) )
17	9 16	eqtrd	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) )
18		resinhcl	|- ( A e. RR -> ( ( sin ` ( _i x. A ) ) / _i ) e. RR )
19	18 5	rerpdivcld	|- ( A e. RR -> ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) e. RR )
20	17 19	eqeltrd	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) e. RR )