Metamath Proof Explorer

Theorem tanhvalnegitan

Description: Value of the tanh function in terms of tan and multiplication by -i. (Contributed by Jon Pennant, 22-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 tanhvaltan 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( tan ` ( _i x. A ) ) / _i ) )
2 simpl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> A e. CC )
3 ax-icn 
 |-  _i e. CC
4 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
5 3 4 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
6 2 5 syl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( _i x. A ) e. CC )
7 coshval-named 
 |-  ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
8 2 7 syl 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
9 simpr 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) =/= 0 )
10 8 9 eqnetrrd 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cos ` ( _i x. A ) ) =/= 0 )
11 6 10 tancld 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tan ` ( _i x. A ) ) e. CC )
12 3 a1i 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> _i e. CC )
13 ine0 
 |-  _i =/= 0
14 13 a1i 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> _i =/= 0 )
15 11 12 14 divrec2d 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( 1 / _i ) x. ( tan ` ( _i x. A ) ) ) )
16 irec 
 |-  ( 1 / _i ) = -u _i
17 16 oveq1i 
 |-  ( ( 1 / _i ) x. ( tan ` ( _i x. A ) ) ) = ( -u _i x. ( tan ` ( _i x. A ) ) )
18 15 17 eqtrdi 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( tan ` ( _i x. A ) ) / _i ) = ( -u _i x. ( tan ` ( _i x. A ) ) ) )
19 1 18 eqtrd 
 |-  ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( -u _i x. ( tan ` ( _i x. A ) ) ) )