faclim2

Description: Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017)

		Ref	Expression
	Hypothesis	faclim2.1	$⊢ F = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{M}}{(n + M)!})$
	Assertion	faclim2	$⊢ M \in ℕ_{0} \to F ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		faclim2.1	$⊢ F = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{M}}{(n + M)!})$
2		oveq2	$⊢ a = 0 \to {(n + 1)}^{a} = {(n + 1)}^{0}$
3	2	oveq2d	$⊢ a = 0 \to n! {(n + 1)}^{a} = n! {(n + 1)}^{0}$
4		oveq2	$⊢ a = 0 \to n + a = n + 0$
5	4	fveq2d	$⊢ a = 0 \to (n + a)! = (n + 0)!$
6	3 5	oveq12d	$⊢ a = 0 \to \frac{n! {(n + 1)}^{a}}{(n + a)!} = \frac{n! {(n + 1)}^{0}}{(n + 0)!}$
7	6	mpteq2dv	$⊢ a = 0 \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!})$
8	7	breq1d	$⊢ a = 0 \to ((n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) ⇝ 1 \leftrightarrow (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) ⇝ 1)$
9		oveq2	$⊢ a = m \to {(n + 1)}^{a} = {(n + 1)}^{m}$
10	9	oveq2d	$⊢ a = m \to n! {(n + 1)}^{a} = n! {(n + 1)}^{m}$
11		oveq2	$⊢ a = m \to n + a = n + m$
12	11	fveq2d	$⊢ a = m \to (n + a)! = (n + m)!$
13	10 12	oveq12d	$⊢ a = m \to \frac{n! {(n + 1)}^{a}}{(n + a)!} = \frac{n! {(n + 1)}^{m}}{(n + m)!}$
14	13	mpteq2dv	$⊢ a = m \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!})$
15	14	breq1d	$⊢ a = m \to ((n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) ⇝ 1 \leftrightarrow (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1)$
16		oveq2	$⊢ a = m + 1 \to {(n + 1)}^{a} = {(n + 1)}^{m + 1}$
17	16	oveq2d	$⊢ a = m + 1 \to n! {(n + 1)}^{a} = n! {(n + 1)}^{m + 1}$
18		oveq2	$⊢ a = m + 1 \to n + a = n + m + 1$
19	18	fveq2d	$⊢ a = m + 1 \to (n + a)! = (n + m + 1)!$
20	17 19	oveq12d	$⊢ a = m + 1 \to \frac{n! {(n + 1)}^{a}}{(n + a)!} = \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}$
21	20	mpteq2dv	$⊢ a = m + 1 \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!})$
22	21	breq1d	$⊢ a = m + 1 \to ((n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) ⇝ 1 \leftrightarrow (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) ⇝ 1)$
23		oveq2	$⊢ a = M \to {(n + 1)}^{a} = {(n + 1)}^{M}$
24	23	oveq2d	$⊢ a = M \to n! {(n + 1)}^{a} = n! {(n + 1)}^{M}$
25		oveq2	$⊢ a = M \to n + a = n + M$
26	25	fveq2d	$⊢ a = M \to (n + a)! = (n + M)!$
27	24 26	oveq12d	$⊢ a = M \to \frac{n! {(n + 1)}^{a}}{(n + a)!} = \frac{n! {(n + 1)}^{M}}{(n + M)!}$
28	27	mpteq2dv	$⊢ a = M \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{M}}{(n + M)!})$
29	28	breq1d	$⊢ a = M \to ((n \in ℕ ⟼ \frac{n! {(n + 1)}^{a}}{(n + a)!}) ⇝ 1 \leftrightarrow (n \in ℕ ⟼ \frac{n! {(n + 1)}^{M}}{(n + M)!}) ⇝ 1)$
30		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
31		1zzd	$⊢ ⊤ \to 1 \in ℤ$
32		nnex	$⊢ ℕ \in V$
33	32	mptex	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) \in V$
34	33	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) \in V$
35		1cnd	$⊢ ⊤ \to 1 \in ℂ$
36		fveq2	$⊢ n = m \to n! = m!$
37		oveq1	$⊢ n = m \to n + 1 = m + 1$
38	37	oveq1d	$⊢ n = m \to {(n + 1)}^{0} = {(m + 1)}^{0}$
39	36 38	oveq12d	$⊢ n = m \to n! {(n + 1)}^{0} = m! {(m + 1)}^{0}$
40		fvoveq1	$⊢ n = m \to (n + 0)! = (m + 0)!$
41	39 40	oveq12d	$⊢ n = m \to \frac{n! {(n + 1)}^{0}}{(n + 0)!} = \frac{m! {(m + 1)}^{0}}{(m + 0)!}$
42		eqid	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!})$
43		ovex	$⊢ \frac{m! {(m + 1)}^{0}}{(m + 0)!} \in V$
44	41 42 43	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) (m) = \frac{m! {(m + 1)}^{0}}{(m + 0)!}$
45		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
46	45	nncnd	$⊢ m \in ℕ \to m + 1 \in ℂ$
47	46	exp0d	$⊢ m \in ℕ \to {(m + 1)}^{0} = 1$
48	47	oveq2d	$⊢ m \in ℕ \to m! {(m + 1)}^{0} = m! \cdot 1$
49		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
50		faccl	$⊢ m \in ℕ_{0} \to m! \in ℕ$
51	49 50	syl	$⊢ m \in ℕ \to m! \in ℕ$
52	51	nncnd	$⊢ m \in ℕ \to m! \in ℂ$
53	52	mulid1d	$⊢ m \in ℕ \to m! \cdot 1 = m!$
54	48 53	eqtrd	$⊢ m \in ℕ \to m! {(m + 1)}^{0} = m!$
55		nncn	$⊢ m \in ℕ \to m \in ℂ$
56	55	addid1d	$⊢ m \in ℕ \to m + 0 = m$
57	56	fveq2d	$⊢ m \in ℕ \to (m + 0)! = m!$
58	54 57	oveq12d	$⊢ m \in ℕ \to \frac{m! {(m + 1)}^{0}}{(m + 0)!} = \frac{m!}{m!}$
59	51	nnne0d	$⊢ m \in ℕ \to m! \neq 0$
60	52 59	dividd	$⊢ m \in ℕ \to \frac{m!}{m!} = 1$
61	44 58 60	3eqtrd	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) (m) = 1$
62	61	adantl	$⊢ (⊤ \land m \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) (m) = 1$
63	30 31 34 35 62	climconst	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) ⇝ 1$
64	63	mptru	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{0}}{(n + 0)!}) ⇝ 1$
65		1zzd	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to 1 \in ℤ$
66		simpr	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1$
67	32	mptex	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) \in V$
68	67	a1i	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) \in V$
69		1zzd	$⊢ m \in ℕ_{0} \to 1 \in ℤ$
70		1cnd	$⊢ m \in ℕ_{0} \to 1 \in ℂ$
71		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
72	71	nnzd	$⊢ m \in ℕ_{0} \to m + 1 \in ℤ$
73	32	mptex	$⊢ (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) \in V$
74	73	a1i	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) \in V$
75		oveq1	$⊢ n = k \to n + 1 = k + 1$
76		oveq1	$⊢ n = k \to n + m + 1 = k + m + 1$
77	75 76	oveq12d	$⊢ n = k \to \frac{n + 1}{n + m + 1} = \frac{k + 1}{k + m + 1}$
78		eqid	$⊢ (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) = (n \in ℕ ⟼ \frac{n + 1}{n + m + 1})$
79		ovex	$⊢ \frac{k + 1}{k + m + 1} \in V$
80	77 78 79	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) = \frac{k + 1}{k + m + 1}$
81	80	adantl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) = \frac{k + 1}{k + m + 1}$
82	30 69 70 72 74 81	divcnvlin	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) ⇝ 1$
83	82	adantr	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) ⇝ 1$
84		simpr	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n \in ℕ$
85	84	nnnn0d	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n \in ℕ_{0}$
86		faccl	$⊢ n \in ℕ_{0} \to n! \in ℕ$
87	85 86	syl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n! \in ℕ$
88		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
89		nnexpcl	$⊢ (n + 1 \in ℕ \land m \in ℕ_{0}) \to {(n + 1)}^{m} \in ℕ$
90	88 89	sylan	$⊢ (n \in ℕ \land m \in ℕ_{0}) \to {(n + 1)}^{m} \in ℕ$
91	90	ancoms	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to {(n + 1)}^{m} \in ℕ$
92	87 91	nnmulcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n! {(n + 1)}^{m} \in ℕ$
93	92	nnred	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n! {(n + 1)}^{m} \in ℝ$
94		nnnn0addcl	$⊢ (n \in ℕ \land m \in ℕ_{0}) \to n + m \in ℕ$
95	94	ancoms	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n + m \in ℕ$
96	95	nnnn0d	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n + m \in ℕ_{0}$
97		faccl	$⊢ n + m \in ℕ_{0} \to (n + m)! \in ℕ$
98	96 97	syl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to (n + m)! \in ℕ$
99	93 98	nndivred	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{n! {(n + 1)}^{m}}{(n + m)!} \in ℝ$
100	99	recnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{n! {(n + 1)}^{m}}{(n + m)!} \in ℂ$
101	100	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) : ℕ ⟶ ℂ$
102	101	ffvelrnda	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) \in ℂ$
103	102	adantlr	$⊢ ((m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) \in ℂ$
104	88	adantl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n + 1 \in ℕ$
105	104	nnred	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n + 1 \in ℝ$
106	71	adantr	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to m + 1 \in ℕ$
107	84 106	nnaddcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to n + m + 1 \in ℕ$
108	105 107	nndivred	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{n + 1}{n + m + 1} \in ℝ$
109	108	recnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{n + 1}{n + m + 1} \in ℂ$
110	109	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) : ℕ ⟶ ℂ$
111	110	ffvelrnda	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) \in ℂ$
112	111	adantlr	$⊢ ((m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) \in ℂ$
113		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
114	113	adantl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + 1 \in ℕ$
115	114	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + 1 \in ℂ$
116		simpl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to m \in ℕ_{0}$
117	115 116	expp1d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to {(k + 1)}^{m + 1} = {(k + 1)}^{m} (k + 1)$
118	117	oveq2d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! {(k + 1)}^{m + 1} = k! {(k + 1)}^{m} (k + 1)$
119		simpr	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k \in ℕ$
120	119	nnnn0d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k \in ℕ_{0}$
121		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
122	120 121	syl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! \in ℕ$
123	122	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! \in ℂ$
124		nnexpcl	$⊢ (k + 1 \in ℕ \land m \in ℕ_{0}) \to {(k + 1)}^{m} \in ℕ$
125	113 124	sylan	$⊢ (k \in ℕ \land m \in ℕ_{0}) \to {(k + 1)}^{m} \in ℕ$
126	125	ancoms	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to {(k + 1)}^{m} \in ℕ$
127	126	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to {(k + 1)}^{m} \in ℂ$
128	123 127 115	mulassd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! {(k + 1)}^{m} (k + 1) = k! {(k + 1)}^{m} (k + 1)$
129	118 128	eqtr4d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! {(k + 1)}^{m + 1} = k! {(k + 1)}^{m} (k + 1)$
130	120 116	nn0addcld	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + m \in ℕ_{0}$
131		facp1	$⊢ k + m \in ℕ_{0} \to (k + m + 1)! = (k + m)! (k + m + 1)$
132	130 131	syl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m + 1)! = (k + m)! (k + m + 1)$
133	119	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k \in ℂ$
134	116	nn0cnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to m \in ℂ$
135		1cnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to 1 \in ℂ$
136	133 134 135	addassd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + m + 1 = k + m + 1$
137	136	fveq2d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m + 1)! = (k + m + 1)!$
138	136	oveq2d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m)! (k + m + 1) = (k + m)! (k + m + 1)$
139	132 137 138	3eqtr3d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m + 1)! = (k + m)! (k + m + 1)$
140	129 139	oveq12d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!} = \frac{k! {(k + 1)}^{m} (k + 1)}{(k + m)! (k + m + 1)}$
141	122 126	nnmulcld	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! {(k + 1)}^{m} \in ℕ$
142	141	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k! {(k + 1)}^{m} \in ℂ$
143		faccl	$⊢ k + m \in ℕ_{0} \to (k + m)! \in ℕ$
144	130 143	syl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m)! \in ℕ$
145	144	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m)! \in ℂ$
146	71	adantr	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to m + 1 \in ℕ$
147	119 146	nnaddcld	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + m + 1 \in ℕ$
148	147	nncnd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + m + 1 \in ℂ$
149	144	nnne0d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (k + m)! \neq 0$
150	147	nnne0d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to k + m + 1 \neq 0$
151	142 145 115 148 149 150	divmuldivd	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (\frac{k! {(k + 1)}^{m}}{(k + m)!}) (\frac{k + 1}{k + m + 1}) = \frac{k! {(k + 1)}^{m} (k + 1)}{(k + m)! (k + m + 1)}$
152	140 151	eqtr4d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!} = (\frac{k! {(k + 1)}^{m}}{(k + m)!}) (\frac{k + 1}{k + m + 1})$
153		fveq2	$⊢ n = k \to n! = k!$
154	75	oveq1d	$⊢ n = k \to {(n + 1)}^{m + 1} = {(k + 1)}^{m + 1}$
155	153 154	oveq12d	$⊢ n = k \to n! {(n + 1)}^{m + 1} = k! {(k + 1)}^{m + 1}$
156		fvoveq1	$⊢ n = k \to (n + m + 1)! = (k + m + 1)!$
157	155 156	oveq12d	$⊢ n = k \to \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!} = \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!}$
158		eqid	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!})$
159		ovex	$⊢ \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!} \in V$
160	157 158 159	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) (k) = \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!}$
161	160	adantl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) (k) = \frac{k! {(k + 1)}^{m + 1}}{(k + m + 1)!}$
162	75	oveq1d	$⊢ n = k \to {(n + 1)}^{m} = {(k + 1)}^{m}$
163	153 162	oveq12d	$⊢ n = k \to n! {(n + 1)}^{m} = k! {(k + 1)}^{m}$
164		fvoveq1	$⊢ n = k \to (n + m)! = (k + m)!$
165	163 164	oveq12d	$⊢ n = k \to \frac{n! {(n + 1)}^{m}}{(n + m)!} = \frac{k! {(k + 1)}^{m}}{(k + m)!}$
166		eqid	$⊢ (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!})$
167		ovex	$⊢ \frac{k! {(k + 1)}^{m}}{(k + m)!} \in V$
168	165 166 167	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) = \frac{k! {(k + 1)}^{m}}{(k + m)!}$
169	168 80	oveq12d	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) = (\frac{k! {(k + 1)}^{m}}{(k + m)!}) (\frac{k + 1}{k + m + 1})$
170	169	adantl	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k) = (\frac{k! {(k + 1)}^{m}}{(k + m)!}) (\frac{k + 1}{k + m + 1})$
171	152 161 170	3eqtr4d	$⊢ (m \in ℕ_{0} \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) (k) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k)$
172	171	adantlr	$⊢ ((m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) (k) = (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) (k) (n \in ℕ ⟼ \frac{n + 1}{n + m + 1}) (k)$
173	30 65 66 68 83 103 112 172	climmul	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) ⇝ 1 \cdot 1$
174		1t1e1	$⊢ 1 \cdot 1 = 1$
175	173 174	breqtrdi	$⊢ (m \in ℕ_{0} \land (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1) \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) ⇝ 1$
176	175	ex	$⊢ m \in ℕ_{0} \to ((n \in ℕ ⟼ \frac{n! {(n + 1)}^{m}}{(n + m)!}) ⇝ 1 \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{m + 1}}{(n + m + 1)!}) ⇝ 1)$
177	8 15 22 29 64 176	nn0ind	$⊢ M \in ℕ_{0} \to (n \in ℕ ⟼ \frac{n! {(n + 1)}^{M}}{(n + M)!}) ⇝ 1$
178	1 177	eqbrtrid	$⊢ M \in ℕ_{0} \to F ⇝ 1$

Metamath Proof Explorer

Theorem faclim2

Proof