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 ∈ ℂ ∧ cosh ⁡ A ≠ 0 → tanh ⁡ A = − i ⁢ tan ⁡ i ⁢ A

Proof

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