Metamath Proof Explorer

Theorem sinhsub

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

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

Proof

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