Metamath Proof Explorer

Theorem sinhsub

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

Ref Expression
Assertion sinhsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 − 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) − ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
2 sinhadd ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ - 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ - 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) )
4 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
5 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
6 4 5 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
7 6 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 + - 𝐵 ) ) = ( sinh ‘ ( 𝐴 − 𝐵 ) ) )
8 coshneg ⊢ ( 𝐵 ∈ ℂ → ( cosh ‘ - 𝐵 ) = ( cosh ‘ 𝐵 ) )
9 8 oveq2d ⊢ ( 𝐵 ∈ ℂ → ( ( sinh ‘ 𝐴 ) · ( cosh ‘ - 𝐵 ) ) = ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) )
10 5 9 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sinh ‘ 𝐴 ) · ( cosh ‘ - 𝐵 ) ) = ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) )
11 10 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ - 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) )
12 3 7 11 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 − 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) )
13 sinhneg ⊢ ( 𝐵 ∈ ℂ → ( sinh ‘ - 𝐵 ) = - ( sinh ‘ 𝐵 ) )
14 13 oveq2d ⊢ ( 𝐵 ∈ ℂ → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) = ( ( cosh ‘ 𝐴 ) · - ( sinh ‘ 𝐵 ) ) )
15 5 14 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) = ( ( cosh ‘ 𝐴 ) · - ( sinh ‘ 𝐵 ) ) )
16 coshcl ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
17 sinhcl ⊢ ( 𝐵 ∈ ℂ → ( sinh ‘ 𝐵 ) ∈ ℂ )
18 mulneg2 ⊢ ( ( ( cosh ‘ 𝐴 ) ∈ ℂ ∧ ( sinh ‘ 𝐵 ) ∈ ℂ ) → ( ( cosh ‘ 𝐴 ) · - ( sinh ‘ 𝐵 ) ) = - ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) )
19 16 17 18 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cosh ‘ 𝐴 ) · - ( sinh ‘ 𝐵 ) ) = - ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) )
20 15 19 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) = - ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) )
21 20 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ - 𝐵 ) ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + - ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )
22 sinhcl ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) ∈ ℂ )
23 4 22 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ 𝐴 ) ∈ ℂ )
24 coshf ⊢ cosh : ℂ ⟶ ℂ
25 24 a1i ⊢ ( 𝐴 ∈ ℂ → cosh : ℂ ⟶ ℂ )
26 25 ffvelcdmda ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cosh ‘ 𝐵 ) ∈ ℂ )
27 23 26 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ∈ ℂ )
28 4 16 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cosh ‘ 𝐴 ) ∈ ℂ )
29 sinhf ⊢ sinh : ℂ ⟶ ℂ
30 29 a1i ⊢ ( 𝐴 ∈ ℂ → sinh : ℂ ⟶ ℂ )
31 30 ffvelcdmda ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ 𝐵 ) ∈ ℂ )
32 28 31 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ∈ ℂ )
33 27 32 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + - ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) − ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )
34 12 21 33 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 − 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) − ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )