Metamath Proof Explorer

Theorem coshsub

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

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

Proof

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