Metamath Proof Explorer

Theorem faclimlem2

Description: Lemma for faclim . Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017)

Ref Expression
Assertion faclimlem2 ⊢M∈ℕ0→seq1×n∈ℕ⟼1+Mn⁢1+1n1+M+1n⇝M+1

Proof

Step Hyp Ref Expression
1 faclimlem1 ⊢M∈ℕ0→seq1×n∈ℕ⟼1+Mn⁢1+1n1+M+1n=m∈ℕ⟼M+1⁢m+1m+M+1
2 nnuz ⊢ℕ=ℤ≥1
3 1zzd ⊢M∈ℕ0→1∈ℤ
4 1cnd ⊢M∈ℕ0→1∈ℂ
5 nn0p1nn ⊢M∈ℕ0→M+1∈ℕ
6 5 nnzd ⊢M∈ℕ0→M+1∈ℤ
7 nnex ⊢ℕ∈V
8 7 mptex ⊢m∈ℕ⟼m+1m+M+1∈V
9 8 a1i ⊢M∈ℕ0→m∈ℕ⟼m+1m+M+1∈V
10 oveq1 ⊢m=k→m+1=k+1
11 oveq1 ⊢m=k→m+M+1=k+M+1
12 10 11 oveq12d ⊢m=k→m+1m+M+1=k+1k+M+1
13 eqid ⊢m∈ℕ⟼m+1m+M+1=m∈ℕ⟼m+1m+M+1
14 ovex ⊢k+1k+M+1∈V
15 12 13 14 fvmpt ⊢k∈ℕ→m∈ℕ⟼m+1m+M+1⁡k=k+1k+M+1
16 15 adantl ⊢M∈ℕ0∧k∈ℕ→m∈ℕ⟼m+1m+M+1⁡k=k+1k+M+1
17 2 3 4 6 9 16 divcnvlin ⊢M∈ℕ0→m∈ℕ⟼m+1m+M+1⇝1
18 5 nncnd ⊢M∈ℕ0→M+1∈ℂ
19 7 mptex ⊢m∈ℕ⟼M+1⁢m+1m+M+1∈V
20 19 a1i ⊢M∈ℕ0→m∈ℕ⟼M+1⁢m+1m+M+1∈V
21 peano2nn ⊢m∈ℕ→m+1∈ℕ
22 21 adantl ⊢M∈ℕ0∧m∈ℕ→m+1∈ℕ
23 22 nnred ⊢M∈ℕ0∧m∈ℕ→m+1∈ℝ
24 simpr ⊢M∈ℕ0∧m∈ℕ→m∈ℕ
25 5 adantr ⊢M∈ℕ0∧m∈ℕ→M+1∈ℕ
26 24 25 nnaddcld ⊢M∈ℕ0∧m∈ℕ→m+M+1∈ℕ
27 23 26 nndivred ⊢M∈ℕ0∧m∈ℕ→m+1m+M+1∈ℝ
28 27 recnd ⊢M∈ℕ0∧m∈ℕ→m+1m+M+1∈ℂ
29 28 fmpttd ⊢M∈ℕ0→m∈ℕ⟼m+1m+M+1:ℕ⟶ℂ
30 29 ffvelcdmda ⊢M∈ℕ0∧k∈ℕ→m∈ℕ⟼m+1m+M+1⁡k∈ℂ
31 12 oveq2d ⊢m=k→M+1⁢m+1m+M+1=M+1⁢k+1k+M+1
32 eqid ⊢m∈ℕ⟼M+1⁢m+1m+M+1=m∈ℕ⟼M+1⁢m+1m+M+1
33 ovex ⊢M+1⁢k+1k+M+1∈V
34 31 32 33 fvmpt ⊢k∈ℕ→m∈ℕ⟼M+1⁢m+1m+M+1⁡k=M+1⁢k+1k+M+1
35 15 oveq2d ⊢k∈ℕ→M+1⁢m∈ℕ⟼m+1m+M+1⁡k=M+1⁢k+1k+M+1
36 34 35 eqtr4d ⊢k∈ℕ→m∈ℕ⟼M+1⁢m+1m+M+1⁡k=M+1⁢m∈ℕ⟼m+1m+M+1⁡k
37 36 adantl ⊢M∈ℕ0∧k∈ℕ→m∈ℕ⟼M+1⁢m+1m+M+1⁡k=M+1⁢m∈ℕ⟼m+1m+M+1⁡k
38 2 3 17 18 20 30 37 climmulc2 ⊢M∈ℕ0→m∈ℕ⟼M+1⁢m+1m+M+1⇝M+1⋅1
39 18 mulridd ⊢M∈ℕ0→M+1⋅1=M+1
40 38 39 breqtrd ⊢M∈ℕ0→m∈ℕ⟼M+1⁢m+1m+M+1⇝M+1
41 1 40 eqbrtrd ⊢M∈ℕ0→seq1×n∈ℕ⟼1+Mn⁢1+1n1+M+1n⇝M+1