Theorem 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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐵 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐵 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
3		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
4		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
5		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
6	1 2 3 4 5	efaddlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )