Metamath Proof Explorer

Theorem faclim2

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

Ref Expression
Hypothesis faclim2.1 ⊢F=n∈ℕ⟼n!⁢n+1Mn+M!
Assertion faclim2 ⊢M∈ℕ0→F⇝1

Proof

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