This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efval2

Description: Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014)

		Ref	Expression
	Hypothesis	efcvg.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	efval2	$⊢ A \in ℂ \to e^{A} = \sum_{k \in ℕ_{0}} F (k)$

Step	Hyp	Ref	Expression
1		efcvg.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2		efval	$⊢ A \in ℂ \to e^{A} = \sum_{k \in ℕ_{0}} (\frac{A^{k}}{k!})$
3	1	eftval	$⊢ k \in ℕ_{0} \to F (k) = \frac{A^{k}}{k!}$
4	3	sumeq2i	$⊢ \sum_{k \in ℕ_{0}} F (k) = \sum_{k \in ℕ_{0}} (\frac{A^{k}}{k!})$
5	2 4	eqtr4di	$⊢ A \in ℂ \to e^{A} = \sum_{k \in ℕ_{0}} F (k)$