Theorem faclimlem2

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

	Ref	Expression
Assertion	faclimlem2	⊢ ( 𝑀 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( 𝑀 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		faclimlem1	⊢ ( 𝑀 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3		1zzd	⊢ ( 𝑀 ∈ ℕ0 → 1 ∈ ℤ )
4		1cnd	⊢ ( 𝑀 ∈ ℕ0 → 1 ∈ ℂ )
5		nn0p1nn	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ )
6	5	nnzd	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℤ )
7		nnex	⊢ ℕ ∈ V
8	7	mptex	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ∈ V
9	8	a1i	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ∈ V )
10		oveq1	⊢ ( 𝑚 = 𝑘 → ( 𝑚 + 1 ) = ( 𝑘 + 1 ) )
11		oveq1	⊢ ( 𝑚 = 𝑘 → ( 𝑚 + ( 𝑀 + 1 ) ) = ( 𝑘 + ( 𝑀 + 1 ) ) )
12	10 11	oveq12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) )
13		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) )
14		ovex	⊢ ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ∈ V
15	12 13 14	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) )
16	15	adantl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) = ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) )
17	2 3 4 6 9 16	divcnvlin	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ⇝ 1 )
18	5	nncnd	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℂ )
19	7	mptex	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ∈ V
20	19	a1i	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ∈ V )
21		peano2nn	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
22	21	adantl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
23	22	nnred	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℝ )
24		simpr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
25	5	adantr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( 𝑀 + 1 ) ∈ ℕ )
26	24 25	nnaddcld	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + ( 𝑀 + 1 ) ) ∈ ℕ )
27	23 26	nndivred	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ∈ ℝ )
28	27	recnd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ∈ ℂ )
29	28	fmpttd	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) : ℕ ⟶ ℂ )
30	29	ffvelrnda	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) ∈ ℂ )
31	12	oveq2d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) )
32		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) )
33		ovex	⊢ ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) ∈ V
34	31 32 33	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) )
35	15	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑀 + 1 ) · ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) ) = ( ( 𝑀 + 1 ) · ( ( 𝑘 + 1 ) / ( 𝑘 + ( 𝑀 + 1 ) ) ) ) )
36	34 35	eqtr4d	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) ) )
37	36	adantl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ‘ 𝑘 ) = ( ( 𝑀 + 1 ) · ( ( 𝑚 ∈ ℕ ↦ ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ‘ 𝑘 ) ) )
38	2 3 17 18 20 30 37	climmulc2	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ⇝ ( ( 𝑀 + 1 ) · 1 ) )
39	18	mulid1d	⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑀 + 1 ) · 1 ) = ( 𝑀 + 1 ) )
40	38 39	breqtrd	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑚 ∈ ℕ ↦ ( ( 𝑀 + 1 ) · ( ( 𝑚 + 1 ) / ( 𝑚 + ( 𝑀 + 1 ) ) ) ) ) ⇝ ( 𝑀 + 1 ) )
41	1 40	eqbrtrd	⊢ ( 𝑀 ∈ ℕ0 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( ( ( 1 + ( 𝑀 / 𝑛 ) ) · ( 1 + ( 1 / 𝑛 ) ) ) / ( 1 + ( ( 𝑀 + 1 ) / 𝑛 ) ) ) ) ) ⇝ ( 𝑀 + 1 ) )