Theorem coshsinhsq

Description: The fundamental identity for hyperbolic functions: cosh^2 - sinh^2 = 1. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Assertion	coshsinhsq	⊢ ( 𝐴 ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		coshcl	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
2	1	sqvald	⊢ ( 𝐴 ∈ ℂ → ( ( cosh ‘ 𝐴 ) ↑ 2 ) = ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐴 ) ) )
3		sinhcl	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) ∈ ℂ )
4	3	sqvald	⊢ ( 𝐴 ∈ ℂ → ( ( sinh ‘ 𝐴 ) ↑ 2 ) = ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐴 ) ) )
5	2 4	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐴 ) ) − ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐴 ) ) ) )
6		coshsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( cosh ‘ ( 𝐴 − 𝐴 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐴 ) ) − ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐴 ) ) ) )
7	6	anidms	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ ( 𝐴 − 𝐴 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐴 ) ) − ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐴 ) ) ) )
8		subid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
9	8	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ ( 𝐴 − 𝐴 ) ) = ( cosh ‘ 0 ) )
10		cosh0	⊢ ( cosh ‘ 0 ) = 1
11	9 10	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ ( 𝐴 − 𝐴 ) ) = 1 )
12	5 7 11	3eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( ( ( cosh ‘ 𝐴 ) ↑ 2 ) − ( ( sinh ‘ 𝐴 ) ↑ 2 ) ) = 1 )