Metamath Proof Explorer

Theorem coshsub

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

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

Proof

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