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 ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) )

Proof

Step Hyp Ref Expression
1 sinhval-named ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( sinh ‘ 𝐴 ) = ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
3 coshval-named ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
5 2 4 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / i ) / ( cos ‘ ( i · 𝐴 ) ) ) )
6 tanhval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
7 ax-icn ⊢ i ∈ ℂ
8 7 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → i ∈ ℂ )
9 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
10 8 9 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
11 10 sincld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ )
12 10 coscld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ ( i · 𝐴 ) ) ∈ ℂ )
13 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ≠ 0 )
14 4 13 eqnetrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ ( i · 𝐴 ) ) ≠ 0 )
15 ine0 ⊢ i ≠ 0
16 15 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → i ≠ 0 )
17 11 12 8 14 16 divdiv32d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) / i ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / i ) / ( cos ‘ ( i · 𝐴 ) ) ) )
18 5 6 17 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) / i ) )
19 tanval ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( cos ‘ ( i · 𝐴 ) ) ≠ 0 ) → ( tan ‘ ( i · 𝐴 ) ) = ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) )
20 10 14 19 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ ( i · 𝐴 ) ) = ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) )
21 20 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) / i ) )
22 18 21 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) )