Theorem 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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	dfef2.2	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	dfef2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
Assertion	dfef2	⊢ ( 𝜑 → 𝐹 ⇝ ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfef2.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		dfef2.2	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3		dfef2.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
4		ax-1cn	⊢ 1 ∈ ℂ
5		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝐴 ∈ ℂ )
6		nncn	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
7	6	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℂ )
8		nnne0	⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ≠ 0 )
10	5 7 9	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( 𝐴 / 𝑥 ) ∈ ℂ )
11		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 / 𝑥 ) ∈ ℂ ) → ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ )
12	4 10 11	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ )
13		nnnn0	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ0 )
15		cxpexp	⊢ ( ( ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) )
16	12 14 15	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) )
17	16	mpteq2dva	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) )
18		nnrp	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ+ )
19	18	ssriv	⊢ ℕ ⊆ ℝ+
20	19	a1i	⊢ ( 𝐴 ∈ ℂ → ℕ ⊆ ℝ+ )
21		eqid	⊢ ( 0 ( ball ‘ ( abs ∘ − ) ) ( 1 / ( ( abs ‘ 𝐴 ) + 1 ) ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) ( 1 / ( ( abs ‘ 𝐴 ) + 1 ) ) )
22	21	efrlim	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) )
23	20 22	rlimres2	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) )
24	17 23	eqbrtrrd	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) )
25		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
26		1zzd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℤ )
27	12 14	expcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ∈ ℂ )
28	27	fmpttd	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) : ℕ ⟶ ℂ )
29	25 26 28	rlimclim	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ) )
30	24 29	mpbid	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) )
31	2 30	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) )
32		nnex	⊢ ℕ ∈ V
33	32	mptex	⊢ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ∈ V
34	33	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ∈ V )
35		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
36		oveq2	⊢ ( 𝑥 = 𝑘 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑘 ) )
37	36	oveq2d	⊢ ( 𝑥 = 𝑘 → ( 1 + ( 𝐴 / 𝑥 ) ) = ( 1 + ( 𝐴 / 𝑘 ) ) )
38		id	⊢ ( 𝑥 = 𝑘 → 𝑥 = 𝑘 )
39	37 38	oveq12d	⊢ ( 𝑥 = 𝑘 → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
40		eqid	⊢ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) )
41		ovex	⊢ ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ∈ V
42	39 40 41	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
44	43 3	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
45	25 34 1 35 44	climeq	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ↔ 𝐹 ⇝ ( exp ‘ 𝐴 ) ) )
46	31 45	mpbid	⊢ ( 𝜑 → 𝐹 ⇝ ( exp ‘ 𝐴 ) )