This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )