Metamath Proof Explorer

Theorem tanhvaltan

Description: Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh . (Contributed by David A. Wheeler, 10-May-2015) (Revised by Jon Pennant, 22-Oct-2026)

Ref Expression
Assertion tanhvaltan 
|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) )

Proof

Step Hyp Ref Expression
1 sinhval-named 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
2 1 adantr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
3 coshval-named 
 |-  ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
4 3 adantr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
5 2 4 oveq12d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( sinh ` A ) / ( cosh ` A ) ) = ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) )
6 tanhval 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )
7 ax-icn 
 |-  _i e. CC
8 7 a1i 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> _i e. CC )
9 simpl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> A e. CC )
10 8 9 mulcld 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( _i x. A ) e. CC )
11 10 sincld 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( sin ` ( _i x. A ) ) e. CC )
12 10 coscld 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cos ` ( _i x. A ) ) e. CC )
13 simpr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) =/= 0 )
14 4 13 eqnetrrd 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cos ` ( _i x. A ) ) =/= 0 )
15 ine0 
 |-  _i =/= 0
16 15 a1i 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> _i =/= 0 )
17 11 12 8 14 16 divdiv32d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) )
18 5 6 17 3eqtr4d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) )
19 tanval 
 |-  ( ( ( _i x. A ) e. CC /\ ( cos ` ( _i x. A ) ) =/= 0 ) -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
20 10 14 19 syl2anc 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
21 20 oveq1d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) )
22 18 21 eqtr4d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) )