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	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( 1 - ( ( tanh ` A ) ^ 2 ) ) = ( 1 / ( ( cosh ` A ) ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tanhval	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( tanh ` A ) = ( ( sinh ` A ) / ( cosh ` A ) ) )
2	1	oveq1d	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( tanh ` A ) ^ 2 ) = ( ( ( sinh ` A ) / ( cosh ` A ) ) ^ 2 ) )
3	2	oveq2d	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( 1 - ( ( tanh ` A ) ^ 2 ) ) = ( 1 - ( ( ( sinh ` A ) / ( cosh ` A ) ) ^ 2 ) ) )
4		coshcl	|- ( A e. CC -> ( cosh ` A ) e. CC )
5	4	sqcld	|- ( A e. CC -> ( ( cosh ` A ) ^ 2 ) e. CC )
6	5	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( cosh ` A ) ^ 2 ) e. CC )
7		sqne0	|- ( ( cosh ` A ) e. CC -> ( ( ( cosh ` A ) ^ 2 ) =/= 0 <-> ( cosh ` A ) =/= 0 ) )
8	4 7	syl	|- ( A e. CC -> ( ( ( cosh ` A ) ^ 2 ) =/= 0 <-> ( cosh ` A ) =/= 0 ) )
9	8	biimpar	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( cosh ` A ) ^ 2 ) =/= 0 )
10	6 9	dividd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( ( cosh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) = 1 )
11	10	eqcomd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> 1 = ( ( ( cosh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) )
12		sinhcl	|- ( A e. CC -> ( sinh ` A ) e. CC )
13	12	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( sinh ` A ) e. CC )
14	4	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) e. CC )
15		simpr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( cosh ` A ) =/= 0 )
16	13 14 15	sqdivd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( ( sinh ` A ) / ( cosh ` A ) ) ^ 2 ) = ( ( ( sinh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) )
17	11 16	oveq12d	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( 1 - ( ( ( sinh ` A ) / ( cosh ` A ) ) ^ 2 ) ) = ( ( ( ( cosh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) - ( ( ( sinh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) ) )
18	13	sqcld	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( sinh ` A ) ^ 2 ) e. CC )
19	6 18 6 9	divsubdird	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) / ( ( cosh ` A ) ^ 2 ) ) = ( ( ( ( cosh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) - ( ( ( sinh ` A ) ^ 2 ) / ( ( cosh ` A ) ^ 2 ) ) ) )
20		coshsinhsq	|- ( A e. CC -> ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) = 1 )
21	20	oveq1d	|- ( A e. CC -> ( ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) / ( ( cosh ` A ) ^ 2 ) ) = ( 1 / ( ( cosh ` A ) ^ 2 ) ) )
22	21	adantr	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) / ( ( cosh ` A ) ^ 2 ) ) = ( 1 / ( ( cosh ` A ) ^ 2 ) ) )
23	17 19 22	3eqtr2d	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( 1 - ( ( ( sinh ` A ) / ( cosh ` A ) ) ^ 2 ) ) = ( 1 / ( ( cosh ` A ) ^ 2 ) ) )
24	3 23	eqtrd	|- ( ( A e. CC /\ ( cosh ` A ) =/= 0 ) -> ( 1 - ( ( tanh ` A ) ^ 2 ) ) = ( 1 / ( ( cosh ` A ) ^ 2 ) ) )