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 → seq 1 × n ∈ ℕ ⟼ 1 + M n ⁢ 1 + 1 n 1 + M + 1 n ⇝ M + 1

Proof

Step Hyp Ref Expression
1 faclimlem1 ⊢ M ∈ ℕ 0 → seq 1 × n ∈ ℕ ⟼ 1 + M n ⁢ 1 + 1 n 1 + M + 1 n = m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + 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 + 1 m + M + 1 ∈ V
9 8 a1i ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ m + 1 m + 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 + 1 m + M + 1 = k + 1 k + M + 1
13 eqid ⊢ m ∈ ℕ ⟼ m + 1 m + M + 1 = m ∈ ℕ ⟼ m + 1 m + M + 1
14 ovex ⊢ k + 1 k + M + 1 ∈ V
15 12 13 14 fvmpt ⊢ k ∈ ℕ → m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k = k + 1 k + M + 1
16 15 adantl ⊢ M ∈ ℕ 0 ∧ k ∈ ℕ → m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k = k + 1 k + M + 1
17 2 3 4 6 9 16 divcnvlin ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ m + 1 m + M + 1 ⇝ 1
18 5 nncnd ⊢ M ∈ ℕ 0 → M + 1 ∈ ℂ
19 7 mptex ⊢ m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ∈ V
20 19 a1i ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + 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 + 1 m + M + 1 ∈ ℝ
28 27 recnd ⊢ M ∈ ℕ 0 ∧ m ∈ ℕ → m + 1 m + M + 1 ∈ ℂ
29 28 fmpttd ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ m + 1 m + M + 1 : ℕ ⟶ ℂ
30 29 ffvelrnda ⊢ M ∈ ℕ 0 ∧ k ∈ ℕ → m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k ∈ ℂ
31 12 oveq2d ⊢ m = k → M + 1 ⁢ m + 1 m + M + 1 = M + 1 ⁢ k + 1 k + M + 1
32 eqid ⊢ m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 = m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1
33 ovex ⊢ M + 1 ⁢ k + 1 k + M + 1 ∈ V
34 31 32 33 fvmpt ⊢ k ∈ ℕ → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ⁡ k = M + 1 ⁢ k + 1 k + M + 1
35 15 oveq2d ⊢ k ∈ ℕ → M + 1 ⁢ m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k = M + 1 ⁢ k + 1 k + M + 1
36 34 35 eqtr4d ⊢ k ∈ ℕ → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ⁡ k = M + 1 ⁢ m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k
37 36 adantl ⊢ M ∈ ℕ 0 ∧ k ∈ ℕ → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ⁡ k = M + 1 ⁢ m ∈ ℕ ⟼ m + 1 m + M + 1 ⁡ k
38 2 3 17 18 20 30 37 climmulc2 ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ⇝ M + 1 ⋅ 1
39 18 mulid1d ⊢ M ∈ ℕ 0 → M + 1 ⋅ 1 = M + 1
40 38 39 breqtrd ⊢ M ∈ ℕ 0 → m ∈ ℕ ⟼ M + 1 ⁢ m + 1 m + M + 1 ⇝ M + 1
41 1 40 eqbrtrd ⊢ M ∈ ℕ 0 → seq 1 × n ∈ ℕ ⟼ 1 + M n ⁢ 1 + 1 n 1 + M + 1 n ⇝ M + 1