efadd

Description: Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006) (Proof shortened by Mario Carneiro, 29-Apr-2014)

		Ref	Expression
	Assertion	efadd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A + B} = e^{A} e^{B}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{B^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{B^{n}}{n!})$
3		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{{(A + B)}^{n}}{n!}) = (n \in ℕ_{0} ⟼ \frac{{(A + B)}^{n}}{n!})$
4		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
5		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
6	1 2 3 4 5	efaddlem	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A + B} = e^{A} e^{B}$

Metamath Proof Explorer