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

Proof

Step	Hyp	Ref	Expression
1		tanhval	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \tanh \left(A\right)=\frac{\sinh \left(A\right)}{\cosh \left(A\right)}$$
2	1	oveq1d	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to {\tanh \left(A\right)}^2={\left(\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\right)}^2$$
3	2	oveq2d	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to 1-{\tanh \left(A\right)}^2=1-{\left(\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\right)}^2$$
4		coshcl	$$⊢A\in ℂ\to \cosh \left(A\right)\in ℂ$$
5	4	sqcld	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2\in ℂ$$
6	5	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to {\cosh \left(A\right)}^2\in ℂ$$
7		sqne0	$$⊢\cosh \left(A\right)\in ℂ\to \left({\cosh \left(A\right)}^2\ne 0\leftrightarrow \cosh \left(A\right)\ne 0\right)$$
8	4 7	syl	$$⊢A\in ℂ\to \left({\cosh \left(A\right)}^2\ne 0\leftrightarrow \cosh \left(A\right)\ne 0\right)$$
9	8	biimpar	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to {\cosh \left(A\right)}^2\ne 0$$
10	6 9	dividd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \frac{{\cosh \left(A\right)}^2}{{\cosh \left(A\right)}^2}=1$$
11	10	eqcomd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to 1=\frac{{\cosh \left(A\right)}^2}{{\cosh \left(A\right)}^2}$$
12		sinhcl	$$⊢A\in ℂ\to \sinh \left(A\right)\in ℂ$$
13	12	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \sinh \left(A\right)\in ℂ$$
14	4	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\in ℂ$$
15		simpr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \cosh \left(A\right)\ne 0$$
16	13 14 15	sqdivd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to {\left(\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\right)}^2=\frac{{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}$$
17	11 16	oveq12d	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to 1-{\left(\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\right)}^2=\left(\frac{{\cosh \left(A\right)}^2}{{\cosh \left(A\right)}^2}\right)-\left(\frac{{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}\right)$$
18	13	sqcld	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to {\sinh \left(A\right)}^2\in ℂ$$
19	6 18 6 9	divsubdird	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \frac{{\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}=\left(\frac{{\cosh \left(A\right)}^2}{{\cosh \left(A\right)}^2}\right)-\left(\frac{{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}\right)$$
20		coshsinhsq	$$⊢A\in ℂ\to {\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2=1$$
21	20	oveq1d	$$⊢A\in ℂ\to \frac{{\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}=\frac{1}{{\cosh \left(A\right)}^2}$$
22	21	adantr	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to \frac{{\cosh \left(A\right)}^2-{\sinh \left(A\right)}^2}{{\cosh \left(A\right)}^2}=\frac{1}{{\cosh \left(A\right)}^2}$$
23	17 19 22	3eqtr2d	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to 1-{\left(\frac{\sinh \left(A\right)}{\cosh \left(A\right)}\right)}^2=\frac{1}{{\cosh \left(A\right)}^2}$$
24	3 23	eqtrd	$$⊢\left(A\in ℂ\wedge \cosh \left(A\right)\ne 0\right)\to 1-{\tanh \left(A\right)}^2=\frac{1}{{\cosh \left(A\right)}^2}$$