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

Proof

Step	Hyp	Ref	Expression
1		tanhvaltan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( tan ‘ ( i · 𝐴 ) ) / i ) )
2		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
3		ax-icn	⊢ i ∈ ℂ
4		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5	3 4	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
6	2 5	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
7		coshval-named	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
8	2 7	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
9		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ≠ 0 )
10	8 9	eqnetrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ ( i · 𝐴 ) ) ≠ 0 )
11	6 10	tancld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ ( i · 𝐴 ) ) ∈ ℂ )
12	3	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → i ∈ ℂ )
13		ine0	⊢ i ≠ 0
14	13	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → i ≠ 0 )
15	11 12 14	divrec2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( ( 1 / i ) · ( tan ‘ ( i · 𝐴 ) ) ) )
16		irec	⊢ ( 1 / i ) = - i
17	16	oveq1i	⊢ ( ( 1 / i ) · ( tan ‘ ( i · 𝐴 ) ) ) = ( - i · ( tan ‘ ( i · 𝐴 ) ) )
18	15 17	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( - i · ( tan ‘ ( i · 𝐴 ) ) ) )
19	1 18	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( - i · ( tan ‘ ( i · 𝐴 ) ) ) )