Metamath Proof Explorer

Theorem ontanhsq

Description: Hyperbolic tangent/secant identity: 1 - tanh^2 = sech^2 (or 1 / cosh^2). (Contributed by Jon Pennant, 27-Sep-2026)

Ref Expression
Assertion ontanhsq ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( ( tanh ‘ 𝐴 ) ↑ 2 ) ) = ( 1 / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 tanhval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
2 1 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( tanh ‘ 𝐴 ) ↑ 2 ) = ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ↑ 2 ) )
3 2 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( ( tanh ‘ 𝐴 ) ↑ 2 ) ) = ( 1 − ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ↑ 2 ) ) )
4 coshcl ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
5 4 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( cosh ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( cosh ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
7 sqne0 ⊢ ( ( cosh ‘ 𝐴 ) ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( cosh ‘ 𝐴 ) ≠ 0 ) )
8 4 7 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( cosh ‘ 𝐴 ) ≠ 0 ) )
9 8 biimpar ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( cosh ‘ 𝐴 ) ↑ 2 ) ≠ 0 )
10 6 9 dividd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) = 1 )
11 10 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → 1 = ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )
12 sinhcl ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) ∈ ℂ )
13 12 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( sinh ‘ 𝐴 ) ∈ ℂ )
14 4 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ∈ ℂ )
15 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( cosh ‘ 𝐴 ) ≠ 0 )
16 13 14 15 sqdivd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ↑ 2 ) = ( ( ( sinh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )
17 11 16 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) − ( ( ( sinh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) ) )
18 13 sqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( sinh ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
19 6 18 6 9 divsubdird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) − ( ( ( sinh ‘ 𝐴 ) ↑ 2 ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) ) )
20 coshsinhsq ⊢ ( 𝐴 ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) = 1 )
21 20 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) = ( 1 / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) = ( 1 / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )
23 17 19 22 3eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) ↑ 2 ) ) = ( 1 / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )
24 3 23 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( ( tanh ‘ 𝐴 ) ↑ 2 ) ) = ( 1 / ( ( cosh ‘ 𝐴 ) ↑ 2 ) ) )