Metamath Proof Explorer

Theorem coshsub

Description: Subtraction formula for cosh. (Contributed by Jon Pennant, 9-Sep-2026)

Ref Expression
Assertion coshsub 
|- ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A - B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sinh ` A ) x. ( sinh ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 coshadd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( cosh ` ( A + -u B ) ) = ( ( ( cosh ` A ) x. ( cosh ` -u B ) ) + ( ( sinh ` A ) x. ( sinh ` -u B ) ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + -u B ) ) = ( ( ( cosh ` A ) x. ( cosh ` -u B ) ) + ( ( sinh ` A ) x. ( sinh ` -u B ) ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + -u B ) ) = ( cosh ` ( A - B ) ) )
6 coshneg 
 |-  ( B e. CC -> ( cosh ` -u B ) = ( cosh ` B ) )
7 6 oveq2d 
 |-  ( B e. CC -> ( ( cosh ` A ) x. ( cosh ` -u B ) ) = ( ( cosh ` A ) x. ( cosh ` B ) ) )
8 7 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cosh ` A ) x. ( cosh ` -u B ) ) = ( ( cosh ` A ) x. ( cosh ` B ) ) )
9 sinhneg 
 |-  ( B e. CC -> ( sinh ` -u B ) = -u ( sinh ` B ) )
10 9 oveq2d 
 |-  ( B e. CC -> ( ( sinh ` A ) x. ( sinh ` -u B ) ) = ( ( sinh ` A ) x. -u ( sinh ` B ) ) )
11 10 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( sinh ` -u B ) ) = ( ( sinh ` A ) x. -u ( sinh ` B ) ) )
12 sinhcl 
 |-  ( A e. CC -> ( sinh ` A ) e. CC )
13 sinhcl 
 |-  ( B e. CC -> ( sinh ` B ) e. CC )
14 mulneg2 
 |-  ( ( ( sinh ` A ) e. CC /\ ( sinh ` B ) e. CC ) -> ( ( sinh ` A ) x. -u ( sinh ` B ) ) = -u ( ( sinh ` A ) x. ( sinh ` B ) ) )
15 12 13 14 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. -u ( sinh ` B ) ) = -u ( ( sinh ` A ) x. ( sinh ` B ) ) )
16 11 15 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( sinh ` -u B ) ) = -u ( ( sinh ` A ) x. ( sinh ` B ) ) )
17 8 16 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cosh ` A ) x. ( cosh ` -u B ) ) + ( ( sinh ` A ) x. ( sinh ` -u B ) ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) + -u ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
18 3 5 17 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A - B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) + -u ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
19 coshcl 
 |-  ( A e. CC -> ( cosh ` A ) e. CC )
20 19 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` A ) e. CC )
21 coshf 
 |-  cosh : CC --> CC
22 21 a1i 
 |-  ( A e. CC -> cosh : CC --> CC )
23 22 ffvelcdmda 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` B ) e. CC )
24 20 23 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cosh ` A ) x. ( cosh ` B ) ) e. CC )
25 12 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` A ) e. CC )
26 sinhf 
 |-  sinh : CC --> CC
27 26 a1i 
 |-  ( A e. CC -> sinh : CC --> CC )
28 27 ffvelcdmda 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` B ) e. CC )
29 25 28 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( sinh ` B ) ) e. CC )
30 24 29 negsubd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cosh ` A ) x. ( cosh ` B ) ) + -u ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
31 18 30 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A - B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sinh ` A ) x. ( sinh ` B ) ) ) )