dfef2

Description: The limit of the sequence ( 1 + A / k ) ^ k as k goes to +oo is ( expA ) . This is another common definition of _e . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	dfef2.1	$⊢ φ \to F \in V$
	dfef2.2	$⊢ φ \to A \in ℂ$
	dfef2.3	$⊢ (φ \land k \in ℕ) \to F (k) = {(1 + (\frac{A}{k}))}^{k}$
Assertion	dfef2	$⊢ φ \to F ⇝ e^{A}$

Proof

Step	Hyp	Ref	Expression
1		dfef2.1	$⊢ φ \to F \in V$
2		dfef2.2	$⊢ φ \to A \in ℂ$
3		dfef2.3	$⊢ (φ \land k \in ℕ) \to F (k) = {(1 + (\frac{A}{k}))}^{k}$
4		ax-1cn	$⊢ 1 \in ℂ$
5		simpl	$⊢ (A \in ℂ \land x \in ℕ) \to A \in ℂ$
6		nncn	$⊢ x \in ℕ \to x \in ℂ$
7	6	adantl	$⊢ (A \in ℂ \land x \in ℕ) \to x \in ℂ$
8		nnne0	$⊢ x \in ℕ \to x \neq 0$
9	8	adantl	$⊢ (A \in ℂ \land x \in ℕ) \to x \neq 0$
10	5 7 9	divcld	$⊢ (A \in ℂ \land x \in ℕ) \to \frac{A}{x} \in ℂ$
11		addcl	$⊢ (1 \in ℂ \land \frac{A}{x} \in ℂ) \to 1 + (\frac{A}{x}) \in ℂ$
12	4 10 11	sylancr	$⊢ (A \in ℂ \land x \in ℕ) \to 1 + (\frac{A}{x}) \in ℂ$
13		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
14	13	adantl	$⊢ (A \in ℂ \land x \in ℕ) \to x \in ℕ_{0}$
15		cxpexp	$⊢ (1 + (\frac{A}{x}) \in ℂ \land x \in ℕ_{0}) \to {(1 + (\frac{A}{x}))}^{x} = {(1 + (\frac{A}{x}))}^{x}$
16	12 14 15	syl2anc	$⊢ (A \in ℂ \land x \in ℕ) \to {(1 + (\frac{A}{x}))}^{x} = {(1 + (\frac{A}{x}))}^{x}$
17	16	mpteq2dva	$⊢ A \in ℂ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) = (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x})$
18		nnrp	$⊢ x \in ℕ \to x \in ℝ^{+}$
19	18	ssriv	$⊢ ℕ \subseteq ℝ^{+}$
20	19	a1i	$⊢ A \in ℂ \to ℕ \subseteq ℝ^{+}$
21		eqid	$⊢ 0 ball (abs \circ -) (\frac{1}{\|A\| + 1}) = 0 ball (abs \circ -) (\frac{1}{\|A\| + 1})$
22	21	efrlim	$⊢ A \in ℂ \to (x \in ℝ^{+} ⟼ {(1 + (\frac{A}{x}))}^{x}) \underset{ℝ}{⇝} e^{A}$
23	20 22	rlimres2	$⊢ A \in ℂ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) \underset{ℝ}{⇝} e^{A}$
24	17 23	eqbrtrrd	$⊢ A \in ℂ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) \underset{ℝ}{⇝} e^{A}$
25		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
26		1zzd	$⊢ A \in ℂ \to 1 \in ℤ$
27	12 14	expcld	$⊢ (A \in ℂ \land x \in ℕ) \to {(1 + (\frac{A}{x}))}^{x} \in ℂ$
28	27	fmpttd	$⊢ A \in ℂ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) : ℕ ⟶ ℂ$
29	25 26 28	rlimclim	$⊢ A \in ℂ \to ((x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) \underset{ℝ}{⇝} e^{A} \leftrightarrow (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) ⇝ e^{A})$
30	24 29	mpbid	$⊢ A \in ℂ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) ⇝ e^{A}$
31	2 30	syl	$⊢ φ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) ⇝ e^{A}$
32		nnex	$⊢ ℕ \in V$
33	32	mptex	$⊢ (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) \in V$
34	33	a1i	$⊢ φ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) \in V$
35		1zzd	$⊢ φ \to 1 \in ℤ$
36		oveq2	$⊢ x = k \to \frac{A}{x} = \frac{A}{k}$
37	36	oveq2d	$⊢ x = k \to 1 + (\frac{A}{x}) = 1 + (\frac{A}{k})$
38		id	$⊢ x = k \to x = k$
39	37 38	oveq12d	$⊢ x = k \to {(1 + (\frac{A}{x}))}^{x} = {(1 + (\frac{A}{k}))}^{k}$
40		eqid	$⊢ (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) = (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x})$
41		ovex	$⊢ {(1 + (\frac{A}{k}))}^{k} \in V$
42	39 40 41	fvmpt	$⊢ k \in ℕ \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) (k) = {(1 + (\frac{A}{k}))}^{k}$
43	42	adantl	$⊢ (φ \land k \in ℕ) \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) (k) = {(1 + (\frac{A}{k}))}^{k}$
44	43 3	eqtr4d	$⊢ (φ \land k \in ℕ) \to (x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) (k) = F (k)$
45	25 34 1 35 44	climeq	$⊢ φ \to ((x \in ℕ ⟼ {(1 + (\frac{A}{x}))}^{x}) ⇝ e^{A} \leftrightarrow F ⇝ e^{A})$
46	31 45	mpbid	$⊢ φ \to F ⇝ e^{A}$

Metamath Proof Explorer

Theorem dfef2

Proof