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	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2=1$$

Proof

Step	Hyp	Ref	Expression
1		coshcl	$$⊢A\in ℂ\to \cosh \left(A\right)\in ℂ$$
2	1	sqvald	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2=\cosh \left(A\right)\cosh \left(A\right)$$
3		sinhcl	$$⊢A\in ℂ\to \sinh \left(A\right)\in ℂ$$
4	3	sqvald	$$⊢A\in ℂ\to {\sinh \left(A\right)}^2=\sinh \left(A\right)\sinh \left(A\right)$$
5	2 4	oveq12d	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2=\cosh \left(A\right)\cosh \left(A\right)-\sinh \left(A\right)\sinh \left(A\right)$$
6		coshsub	$$⊢\left(A\in ℂ\wedge A\in ℂ\right)\to \cosh \left(A-A\right)=\cosh \left(A\right)\cosh \left(A\right)-\sinh \left(A\right)\sinh \left(A\right)$$
7	6	anidms	$$⊢A\in ℂ\to \cosh \left(A-A\right)=\cosh \left(A\right)\cosh \left(A\right)-\sinh \left(A\right)\sinh \left(A\right)$$
8		subid	$$⊢A\in ℂ\to A-A=0$$
9	8	fveq2d	$$⊢A\in ℂ\to \cosh \left(A-A\right)=\cosh \left(0\right)$$
10		cosh0	$$⊢\cosh \left(0\right)=1$$
11	9 10	eqtrdi	$$⊢A\in ℂ\to \cosh \left(A-A\right)=1$$
12	5 7 11	3eqtr2d	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2=1$$