sinhadd

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

		Ref	Expression
	Assertion	sinhadd	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = \sinh (A) \cosh (B) + \cosh (A) \sinh (B)$

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
2		sinhval-named	$⊢ A + B \in ℂ \to \sinh (A + B) = \frac{\sin i (A + B)}{i}$
3	1 2	syl	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = \frac{\sin i (A + B)}{i}$
4		ax-icn	$⊢ i \in ℂ$
5		adddi	$⊢ (i \in ℂ \land A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
6	4 5	mp3an1	$⊢ (A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
7	6	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \sin i (A + B) = \sin (i A + i B)$
8	7	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\sin i (A + B)}{i} = \frac{\sin (i A + i B)}{i}$
9	4	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to i \in ℂ$
10		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
11	9 10	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to i A \in ℂ$
12		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
13	9 12	sylancom	$⊢ (A \in ℂ \land B \in ℂ) \to i B \in ℂ$
14		sinadd	$⊢ (i A \in ℂ \land i B \in ℂ) \to \sin (i A + i B) = \sin i A \cos i B + \cos i A \sin i B$
15	11 13 14	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to \sin (i A + i B) = \sin i A \cos i B + \cos i A \sin i B$
16	15	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\sin (i A + i B)}{i} = \frac{\sin i A \cos i B + \cos i A \sin i B}{i}$
17	3 8 16	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = \frac{\sin i A \cos i B + \cos i A \sin i B}{i}$
18	11	sincld	$⊢ (A \in ℂ \land B \in ℂ) \to \sin i A \in ℂ$
19	13	coscld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos i B \in ℂ$
20	18 19	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \sin i A \cos i B \in ℂ$
21	11	coscld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos i A \in ℂ$
22	13	sincld	$⊢ (A \in ℂ \land B \in ℂ) \to \sin i B \in ℂ$
23	21 22	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos i A \sin i B \in ℂ$
24		ine0	$⊢ i \neq 0$
25	4 24	pm3.2i	$⊢ (i \in ℂ \land i \neq 0)$
26		divdir	$⊢ (\sin i A \cos i B \in ℂ \land \cos i A \sin i B \in ℂ \land (i \in ℂ \land i \neq 0)) \to \frac{\sin i A \cos i B + \cos i A \sin i B}{i} = (\frac{\sin i A \cos i B}{i}) + (\frac{\cos i A \sin i B}{i})$
27	25 26	mp3an3	$⊢ (\sin i A \cos i B \in ℂ \land \cos i A \sin i B \in ℂ) \to \frac{\sin i A \cos i B + \cos i A \sin i B}{i} = (\frac{\sin i A \cos i B}{i}) + (\frac{\cos i A \sin i B}{i})$
28	20 23 27	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\sin i A \cos i B + \cos i A \sin i B}{i} = (\frac{\sin i A \cos i B}{i}) + (\frac{\cos i A \sin i B}{i})$
29	24	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to i \neq 0$
30	18 19 9 29	div23d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\sin i A \cos i B}{i} = (\frac{\sin i A}{i}) \cos i B$
31	21 22 9 29	divassd	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\cos i A \sin i B}{i} = \cos i A (\frac{\sin i B}{i})$
32	30 31	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to (\frac{\sin i A \cos i B}{i}) + (\frac{\cos i A \sin i B}{i}) = (\frac{\sin i A}{i}) \cos i B + \cos i A (\frac{\sin i B}{i})$
33	17 28 32	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = (\frac{\sin i A}{i}) \cos i B + \cos i A (\frac{\sin i B}{i})$
34		sinhval-named	$⊢ A \in ℂ \to \sinh (A) = \frac{\sin i A}{i}$
35		coshval-named	$⊢ B \in ℂ \to \cosh (B) = \cos i B$
36	34 35	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A) \cosh (B) = (\frac{\sin i A}{i}) \cos i B$
37		coshval-named	$⊢ A \in ℂ \to \cosh (A) = \cos i A$
38		sinhval-named	$⊢ B \in ℂ \to \sinh (B) = \frac{\sin i B}{i}$
39	37 38	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to \cosh (A) \sinh (B) = \cos i A (\frac{\sin i B}{i})$
40	36 39	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A) \cosh (B) + \cosh (A) \sinh (B) = (\frac{\sin i A}{i}) \cos i B + \cos i A (\frac{\sin i B}{i})$
41	33 40	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = \sinh (A) \cosh (B) + \cosh (A) \sinh (B)$

Metamath Proof Explorer

Theorem sinhadd

Proof