tanhadd

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

		Ref	Expression
	Assertion	tanhadd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A + B) = \frac{\tanh (A) + \tanh (B)}{1 + \tanh (A) \tanh (B)}$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to A \in ℂ$
2		simpllr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to B \in ℂ$
3	1 2	addcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to A + B \in ℂ$
4		simprr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A + B) \neq 0$
5		tanhval	$⊢ (A + B \in ℂ \land \cosh (A + B) \neq 0) \to \tanh (A + B) = \frac{\sinh (A + B)}{\cosh (A + B)}$
6	3 4 5	syl2anc	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A + B) = \frac{\sinh (A + B)}{\cosh (A + B)}$
7		sinhadd	$⊢ (A \in ℂ \land B \in ℂ) \to \sinh (A + B) = \sinh (A) \cosh (B) + \cosh (A) \sinh (B)$
8		coshadd	$⊢ (A \in ℂ \land B \in ℂ) \to \cosh (A + B) = \cosh (A) \cosh (B) + \sinh (A) \sinh (B)$
9	7 8	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{\sinh (A + B)}{\cosh (A + B)} = \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}$
10	9	ad2antrr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\sinh (A + B)}{\cosh (A + B)} = \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}$
11		sinhcl	$⊢ A \in ℂ \to \sinh (A) \in ℂ$
12	11	ad3antrrr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (A) \in ℂ$
13		coshcl	$⊢ B \in ℂ \to \cosh (B) \in ℂ$
14	13	ad3antlr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (B) \in ℂ$
15	12 14	mulcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (A) \cosh (B) \in ℂ$
16		coshcl	$⊢ A \in ℂ \to \cosh (A) \in ℂ$
17	16	ad3antrrr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \in ℂ$
18		sinhcl	$⊢ B \in ℂ \to \sinh (B) \in ℂ$
19	18	ad3antlr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (B) \in ℂ$
20	17 19	mulcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \sinh (B) \in ℂ$
21	15 20	addcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (A) \cosh (B) + \cosh (A) \sinh (B) \in ℂ$
22	17 14	mulcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \cosh (B) \in ℂ$
23	12 19	mulcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (A) \sinh (B) \in ℂ$
24	22 23	addcld	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \cosh (B) + \sinh (A) \sinh (B) \in ℂ$
25	8	ad2antrr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A + B) = \cosh (A) \cosh (B) + \sinh (A) \sinh (B)$
26	25 4	eqnetrrd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \cosh (B) + \sinh (A) \sinh (B) \neq 0$
27		simplr	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \neq 0$
28		simprl	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (B) \neq 0$
29	17 14 27 28	mulne0d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \cosh (B) \neq 0$
30	21 24 22 26 29	divcan7d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B)}}{\frac{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}{\cosh (A) \cosh (B)}} = \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}$
31	12 17 19 14 27 28	divadddivd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to (\frac{\sinh (A)}{\cosh (A)}) + (\frac{\sinh (B)}{\cosh (B)}) = \frac{\sinh (A) \cosh (B) + \sinh (B) \cosh (A)}{\cosh (A) \cosh (B)}$
32		tanhval	$⊢ (A \in ℂ \land \cosh (A) \neq 0) \to \tanh (A) = \frac{\sinh (A)}{\cosh (A)}$
33	1 27 32	syl2anc	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A) = \frac{\sinh (A)}{\cosh (A)}$
34		tanhval	$⊢ (B \in ℂ \land \cosh (B) \neq 0) \to \tanh (B) = \frac{\sinh (B)}{\cosh (B)}$
35	2 28 34	syl2anc	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (B) = \frac{\sinh (B)}{\cosh (B)}$
36	33 35	oveq12d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A) + \tanh (B) = (\frac{\sinh (A)}{\cosh (A)}) + (\frac{\sinh (B)}{\cosh (B)})$
37	17 19	mulcomd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \cosh (A) \sinh (B) = \sinh (B) \cosh (A)$
38	37	oveq2d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \sinh (A) \cosh (B) + \cosh (A) \sinh (B) = \sinh (A) \cosh (B) + \sinh (B) \cosh (A)$
39	38	oveq1d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B)} = \frac{\sinh (A) \cosh (B) + \sinh (B) \cosh (A)}{\cosh (A) \cosh (B)}$
40	31 36 39	3eqtr4rd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B)} = \tanh (A) + \tanh (B)$
41	22 23 22 29	divdird	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}{\cosh (A) \cosh (B)} = (\frac{\cosh (A) \cosh (B)}{\cosh (A) \cosh (B)}) + (\frac{\sinh (A) \sinh (B)}{\cosh (A) \cosh (B)})$
42	22 29	dividd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\cosh (A) \cosh (B)}{\cosh (A) \cosh (B)} = 1$
43	33 35	oveq12d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A) \tanh (B) = (\frac{\sinh (A)}{\cosh (A)}) (\frac{\sinh (B)}{\cosh (B)})$
44	12 17 19 14 27 28	divmuldivd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to (\frac{\sinh (A)}{\cosh (A)}) (\frac{\sinh (B)}{\cosh (B)}) = \frac{\sinh (A) \sinh (B)}{\cosh (A) \cosh (B)}$
45	43 44	eqtr2d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\sinh (A) \sinh (B)}{\cosh (A) \cosh (B)} = \tanh (A) \tanh (B)$
46	42 45	oveq12d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to (\frac{\cosh (A) \cosh (B)}{\cosh (A) \cosh (B)}) + (\frac{\sinh (A) \sinh (B)}{\cosh (A) \cosh (B)}) = 1 + \tanh (A) \tanh (B)$
47	41 46	eqtrd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}{\cosh (A) \cosh (B)} = 1 + \tanh (A) \tanh (B)$
48	40 47	oveq12d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B)}}{\frac{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)}{\cosh (A) \cosh (B)}} = \frac{\tanh (A) + \tanh (B)}{1 + \tanh (A) \tanh (B)}$
49	30 48	eqtr3d	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \frac{\sinh (A) \cosh (B) + \cosh (A) \sinh (B)}{\cosh (A) \cosh (B) + \sinh (A) \sinh (B)} = \frac{\tanh (A) + \tanh (B)}{1 + \tanh (A) \tanh (B)}$
50	6 10 49	3eqtrd	$⊢ (((A \in ℂ \land B \in ℂ) \land \cosh (A) \neq 0) \land (\cosh (B) \neq 0 \land \cosh (A + B) \neq 0)) \to \tanh (A + B) = \frac{\tanh (A) + \tanh (B)}{1 + \tanh (A) \tanh (B)}$

Metamath Proof Explorer

Theorem tanhadd

Proof