Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 coshcl 
 |-  ( A e. CC -> ( cosh ` A ) e. CC )
2 1 sqvald 
 |-  ( A e. CC -> ( ( cosh ` A ) ^ 2 ) = ( ( cosh ` A ) x. ( cosh ` A ) ) )
3 sinhcl 
 |-  ( A e. CC -> ( sinh ` A ) e. CC )
4 3 sqvald 
 |-  ( A e. CC -> ( ( sinh ` A ) ^ 2 ) = ( ( sinh ` A ) x. ( sinh ` A ) ) )
5 2 4 oveq12d 
 |-  ( A e. CC -> ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) = ( ( ( cosh ` A ) x. ( cosh ` A ) ) - ( ( sinh ` A ) x. ( sinh ` A ) ) ) )
6 coshsub 
 |-  ( ( A e. CC /\ A e. CC ) -> ( cosh ` ( A - A ) ) = ( ( ( cosh ` A ) x. ( cosh ` A ) ) - ( ( sinh ` A ) x. ( sinh ` A ) ) ) )
7 6 anidms 
 |-  ( A e. CC -> ( cosh ` ( A - A ) ) = ( ( ( cosh ` A ) x. ( cosh ` A ) ) - ( ( sinh ` A ) x. ( sinh ` A ) ) ) )
8 subid 
 |-  ( A e. CC -> ( A - A ) = 0 )
9 8 fveq2d 
 |-  ( A e. CC -> ( cosh ` ( A - A ) ) = ( cosh ` 0 ) )
10 cosh0 
 |-  ( cosh ` 0 ) = 1
11 9 10 eqtrdi 
 |-  ( A e. CC -> ( cosh ` ( A - A ) ) = 1 )
12 5 7 11 3eqtr2d 
 |-  ( A e. CC -> ( ( ( cosh ` A ) ^ 2 ) - ( ( sinh ` A ) ^ 2 ) ) = 1 )