Metamath Proof Explorer

Theorem sinhsub

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

Ref Expression
Assertion sinhsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → sinh ⁡ A − B = sinh ⁡ A ⁢ cosh ⁡ B − cosh ⁡ A ⁢ sinh ⁡ B

Proof

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