Metamath Proof Explorer

Theorem subfaclim

Description: The subfactorial converges rapidly to N ! / _e . This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015)

Ref Expression
Hypotheses derang.d ⊢D=x∈Fin⟼f|f:x⟶1-1 ontox∧∀y∈xf⁡y≠y
subfac.n ⊢S=n∈ℕ0⟼D⁡1…n
Assertion subfaclim ⊢N∈ℕ→N!e−S⁡N<1N

Proof

Step Hyp Ref Expression
1 derang.d ⊢D=x∈Fin⟼f|f:x⟶1-1 ontox∧∀y∈xf⁡y≠y
2 subfac.n ⊢S=n∈ℕ0⟼D⁡1…n
3 nnnn0 ⊢N∈ℕ→N∈ℕ0
4 faccl ⊢N∈ℕ0→N!∈ℕ
5 3 4 syl ⊢N∈ℕ→N!∈ℕ
6 5 nncnd ⊢N∈ℕ→N!∈ℂ
7 ere ⊢e∈ℝ
8 7 recni ⊢e∈ℂ
9 epos ⊢0<e
10 7 9 gt0ne0ii ⊢e≠0
11 divcl ⊢N!∈ℂ∧e∈ℂ∧e≠0→N!e∈ℂ
12 8 10 11 mp3an23 ⊢N!∈ℂ→N!e∈ℂ
13 6 12 syl ⊢N∈ℕ→N!e∈ℂ
14 1 2 subfacf ⊢S:ℕ0⟶ℕ0
15 14 ffvelcdmi ⊢N∈ℕ0→S⁡N∈ℕ0
16 3 15 syl ⊢N∈ℕ→S⁡N∈ℕ0
17 16 nn0cnd ⊢N∈ℕ→S⁡N∈ℂ
18 13 17 subcld ⊢N∈ℕ→N!e−S⁡N∈ℂ
19 18 abscld ⊢N∈ℕ→N!e−S⁡N∈ℝ
20 peano2nn ⊢N∈ℕ→N+1∈ℕ
21 20 peano2nnd ⊢N∈ℕ→N+1+1∈ℕ
22 21 nnred ⊢N∈ℕ→N+1+1∈ℝ
23 20 20 nnmulcld ⊢N∈ℕ→N+1⁢N+1∈ℕ
24 22 23 nndivred ⊢N∈ℕ→N+1+1N+1⁢N+1∈ℝ
25 nnrecre ⊢N∈ℕ→1N∈ℝ
26 eqid ⊢n∈ℕ0⟼−1nn!=n∈ℕ0⟼−1nn!
27 eqid ⊢n∈ℕ0⟼−1nn!=n∈ℕ0⟼−1nn!
28 eqid ⊢n∈ℕ0⟼−1N+1N+1!⁢1N+1+1n=n∈ℕ0⟼−1N+1N+1!⁢1N+1+1n
29 neg1cn ⊢−1∈ℂ
30 29 a1i ⊢N∈ℕ→−1∈ℂ
31 ax-1cn ⊢1∈ℂ
32 31 absnegi ⊢−1=1
33 abs1 ⊢1=1
34 32 33 eqtri ⊢−1=1
35 1le1 ⊢1≤1
36 34 35 eqbrtri ⊢−1≤1
37 36 a1i ⊢N∈ℕ→−1≤1
38 26 27 28 20 30 37 eftlub ⊢N∈ℕ→∑k∈ℤ≥N+1n∈ℕ0⟼−1nn!⁡k≤−1N+1⁢N+1+1N+1!⁢N+1
39 20 nnnn0d ⊢N∈ℕ→N+1∈ℕ0
40 eluznn0 ⊢N+1∈ℕ0∧k∈ℤ≥N+1→k∈ℕ0
41 39 40 sylan ⊢N∈ℕ∧k∈ℤ≥N+1→k∈ℕ0
42 26 eftval ⊢k∈ℕ0→n∈ℕ0⟼−1nn!⁡k=−1kk!
43 41 42 syl ⊢N∈ℕ∧k∈ℤ≥N+1→n∈ℕ0⟼−1nn!⁡k=−1kk!
44 43 sumeq2dv ⊢N∈ℕ→∑k∈ℤ≥N+1n∈ℕ0⟼−1nn!⁡k=∑k∈ℤ≥N+1−1kk!
45 44 fveq2d ⊢N∈ℕ→∑k∈ℤ≥N+1n∈ℕ0⟼−1nn!⁡k=∑k∈ℤ≥N+1−1kk!
46 34 oveq1i ⊢−1N+1=1N+1
47 20 nnzd ⊢N∈ℕ→N+1∈ℤ
48 1exp ⊢N+1∈ℤ→1N+1=1
49 47 48 syl ⊢N∈ℕ→1N+1=1
50 46 49 eqtrid ⊢N∈ℕ→−1N+1=1
51 50 oveq1d ⊢N∈ℕ→−1N+1⁢N+1+1N+1!⁢N+1=1⁢N+1+1N+1!⁢N+1
52 faccl ⊢N+1∈ℕ0→N+1!∈ℕ
53 39 52 syl ⊢N∈ℕ→N+1!∈ℕ
54 53 20 nnmulcld ⊢N∈ℕ→N+1!⁢N+1∈ℕ
55 22 54 nndivred ⊢N∈ℕ→N+1+1N+1!⁢N+1∈ℝ
56 55 recnd ⊢N∈ℕ→N+1+1N+1!⁢N+1∈ℂ
57 56 mullidd ⊢N∈ℕ→1⁢N+1+1N+1!⁢N+1=N+1+1N+1!⁢N+1
58 51 57 eqtrd ⊢N∈ℕ→−1N+1⁢N+1+1N+1!⁢N+1=N+1+1N+1!⁢N+1
59 38 45 58 3brtr3d ⊢N∈ℕ→∑k∈ℤ≥N+1−1kk!≤N+1+1N+1!⁢N+1
60 eqid ⊢ℤ≥N+1=ℤ≥N+1
61 eftcl ⊢−1∈ℂ∧k∈ℕ0→−1kk!∈ℂ
62 29 61 mpan ⊢k∈ℕ0→−1kk!∈ℂ
63 41 62 syl ⊢N∈ℕ∧k∈ℤ≥N+1→−1kk!∈ℂ
64 26 eftlcvg ⊢−1∈ℂ∧N+1∈ℕ0→seqN+1+n∈ℕ0⟼−1nn!∈dom⁡⇝
65 29 39 64 sylancr ⊢N∈ℕ→seqN+1+n∈ℕ0⟼−1nn!∈dom⁡⇝
66 60 47 43 63 65 isumcl ⊢N∈ℕ→∑k∈ℤ≥N+1−1kk!∈ℂ
67 66 abscld ⊢N∈ℕ→∑k∈ℤ≥N+1−1kk!∈ℝ
68 5 nnred ⊢N∈ℕ→N!∈ℝ
69 5 nngt0d ⊢N∈ℕ→0<N!
70 lemul2 ⊢∑k∈ℤ≥N+1−1kk!∈ℝ∧N+1+1N+1!⁢N+1∈ℝ∧N!∈ℝ∧0<N!→∑k∈ℤ≥N+1−1kk!≤N+1+1N+1!⁢N+1↔N!⁢∑k∈ℤ≥N+1−1kk!≤N!⁢N+1+1N+1!⁢N+1
71 67 55 68 69 70 syl112anc ⊢N∈ℕ→∑k∈ℤ≥N+1−1kk!≤N+1+1N+1!⁢N+1↔N!⁢∑k∈ℤ≥N+1−1kk!≤N!⁢N+1+1N+1!⁢N+1
72 59 71 mpbid ⊢N∈ℕ→N!⁢∑k∈ℤ≥N+1−1kk!≤N!⁢N+1+1N+1!⁢N+1
73 1 2 subfacval2 ⊢N∈ℕ0→S⁡N=N!⁢∑k=0N−1kk!
74 3 73 syl ⊢N∈ℕ→S⁡N=N!⁢∑k=0N−1kk!
75 nncn ⊢N∈ℕ→N∈ℂ
76 pncan ⊢N∈ℂ∧1∈ℂ→N+1-1=N
77 75 31 76 sylancl ⊢N∈ℕ→N+1-1=N
78 77 oveq2d ⊢N∈ℕ→0…N+1-1=0…N
79 78 sumeq1d ⊢N∈ℕ→∑k=0N+1-1−1kk!=∑k=0N−1kk!
80 79 oveq2d ⊢N∈ℕ→N!⁢∑k=0N+1-1−1kk!=N!⁢∑k=0N−1kk!
81 74 80 eqtr4d ⊢N∈ℕ→S⁡N=N!⁢∑k=0N+1-1−1kk!
82 81 oveq1d ⊢N∈ℕ→S⁡N+N!⁢∑k∈ℤ≥N+1−1kk!=N!⁢∑k=0N+1-1−1kk!+N!⁢∑k∈ℤ≥N+1−1kk!
83 divrec ⊢N!∈ℂ∧e∈ℂ∧e≠0→N!e=N!⁢1e
84 8 10 83 mp3an23 ⊢N!∈ℂ→N!e=N!⁢1e
85 6 84 syl ⊢N∈ℕ→N!e=N!⁢1e
86 df-e ⊢e=e1
87 86 oveq2i ⊢1e=1e1
88 efneg ⊢1∈ℂ→e−1=1e1
89 31 88 ax-mp ⊢e−1=1e1
90 efval ⊢−1∈ℂ→e−1=∑k∈ℕ0−1kk!
91 29 90 ax-mp ⊢e−1=∑k∈ℕ0−1kk!
92 87 89 91 3eqtr2i ⊢1e=∑k∈ℕ0−1kk!
93 nn0uz ⊢ℕ0=ℤ≥0
94 42 adantl ⊢N∈ℕ∧k∈ℕ0→n∈ℕ0⟼−1nn!⁡k=−1kk!
95 62 adantl ⊢N∈ℕ∧k∈ℕ0→−1kk!∈ℂ
96 0nn0 ⊢0∈ℕ0
97 26 eftlcvg ⊢−1∈ℂ∧0∈ℕ0→seq0+n∈ℕ0⟼−1nn!∈dom⁡⇝
98 29 96 97 mp2an ⊢seq0+n∈ℕ0⟼−1nn!∈dom⁡⇝
99 98 a1i ⊢N∈ℕ→seq0+n∈ℕ0⟼−1nn!∈dom⁡⇝
100 93 60 39 94 95 99 isumsplit ⊢N∈ℕ→∑k∈ℕ0−1kk!=∑k=0N+1-1−1kk!+∑k∈ℤ≥N+1−1kk!
101 92 100 eqtrid ⊢N∈ℕ→1e=∑k=0N+1-1−1kk!+∑k∈ℤ≥N+1−1kk!
102 101 oveq2d ⊢N∈ℕ→N!⁢1e=N!⁢∑k=0N+1-1−1kk!+∑k∈ℤ≥N+1−1kk!
103 fzfid ⊢N∈ℕ→0…N+1-1∈Fin
104 elfznn0 ⊢k∈0…N+1-1→k∈ℕ0
105 104 adantl ⊢N∈ℕ∧k∈0…N+1-1→k∈ℕ0
106 29 105 61 sylancr ⊢N∈ℕ∧k∈0…N+1-1→−1kk!∈ℂ
107 103 106 fsumcl ⊢N∈ℕ→∑k=0N+1-1−1kk!∈ℂ
108 6 107 66 adddid ⊢N∈ℕ→N!⁢∑k=0N+1-1−1kk!+∑k∈ℤ≥N+1−1kk!=N!⁢∑k=0N+1-1−1kk!+N!⁢∑k∈ℤ≥N+1−1kk!
109 85 102 108 3eqtrd ⊢N∈ℕ→N!e=N!⁢∑k=0N+1-1−1kk!+N!⁢∑k∈ℤ≥N+1−1kk!
110 82 109 eqtr4d ⊢N∈ℕ→S⁡N+N!⁢∑k∈ℤ≥N+1−1kk!=N!e
111 6 66 mulcld ⊢N∈ℕ→N!⁢∑k∈ℤ≥N+1−1kk!∈ℂ
112 13 17 111 subaddd ⊢N∈ℕ→N!e−S⁡N=N!⁢∑k∈ℤ≥N+1−1kk!↔S⁡N+N!⁢∑k∈ℤ≥N+1−1kk!=N!e
113 110 112 mpbird ⊢N∈ℕ→N!e−S⁡N=N!⁢∑k∈ℤ≥N+1−1kk!
114 113 fveq2d ⊢N∈ℕ→N!e−S⁡N=N!⁢∑k∈ℤ≥N+1−1kk!
115 6 66 absmuld ⊢N∈ℕ→N!⁢∑k∈ℤ≥N+1−1kk!=N!⁢∑k∈ℤ≥N+1−1kk!
116 5 nnnn0d ⊢N∈ℕ→N!∈ℕ0
117 116 nn0ge0d ⊢N∈ℕ→0≤N!
118 68 117 absidd ⊢N∈ℕ→N!=N!
119 118 oveq1d ⊢N∈ℕ→N!⁢∑k∈ℤ≥N+1−1kk!=N!⁢∑k∈ℤ≥N+1−1kk!
120 114 115 119 3eqtrd ⊢N∈ℕ→N!e−S⁡N=N!⁢∑k∈ℤ≥N+1−1kk!
121 facp1 ⊢N∈ℕ0→N+1!=N!⁢N+1
122 3 121 syl ⊢N∈ℕ→N+1!=N!⁢N+1
123 122 oveq1d ⊢N∈ℕ→N+1!⁢N+1=N!⁢N+1⁢N+1
124 20 nncnd ⊢N∈ℕ→N+1∈ℂ
125 6 124 124 mulassd ⊢N∈ℕ→N!⁢N+1⁢N+1=N!⁢N+1⁢N+1
126 123 125 eqtr2d ⊢N∈ℕ→N!⁢N+1⁢N+1=N+1!⁢N+1
127 126 oveq2d ⊢N∈ℕ→N!⁢N+1+1N!⁢N+1⁢N+1=N!⁢N+1+1N+1!⁢N+1
128 21 nncnd ⊢N∈ℕ→N+1+1∈ℂ
129 23 nncnd ⊢N∈ℕ→N+1⁢N+1∈ℂ
130 23 nnne0d ⊢N∈ℕ→N+1⁢N+1≠0
131 5 nnne0d ⊢N∈ℕ→N!≠0
132 128 129 6 130 131 divcan5d ⊢N∈ℕ→N!⁢N+1+1N!⁢N+1⁢N+1=N+1+1N+1⁢N+1
133 54 nncnd ⊢N∈ℕ→N+1!⁢N+1∈ℂ
134 54 nnne0d ⊢N∈ℕ→N+1!⁢N+1≠0
135 6 128 133 134 divassd ⊢N∈ℕ→N!⁢N+1+1N+1!⁢N+1=N!⁢N+1+1N+1!⁢N+1
136 127 132 135 3eqtr3d ⊢N∈ℕ→N+1+1N+1⁢N+1=N!⁢N+1+1N+1!⁢N+1
137 72 120 136 3brtr4d ⊢N∈ℕ→N!e−S⁡N≤N+1+1N+1⁢N+1
138 nnmulcl ⊢N+1+1∈ℕ∧N∈ℕ→N+1+1⋅ N∈ℕ
139 21 138 mpancom ⊢N∈ℕ→N+1+1⋅ N∈ℕ
140 139 nnred ⊢N∈ℕ→N+1+1⋅ N∈ℝ
141 140 ltp1d ⊢N∈ℕ→N+1+1⋅ N<N+1+1⋅ N+1
142 129 mullidd ⊢N∈ℕ→1⁢N+1⁢N+1=N+1⁢N+1
143 31 a1i ⊢N∈ℕ→1∈ℂ
144 75 143 124 adddird ⊢N∈ℕ→N+1⁢N+1=N⁢N+1+1⁢N+1
145 75 124 mulcomd ⊢N∈ℕ→N⁢N+1=N+1⋅ N
146 124 mullidd ⊢N∈ℕ→1⁢N+1=N+1
147 145 146 oveq12d ⊢N∈ℕ→N⁢N+1+1⁢N+1=N+1⋅ N+N+1
148 124 143 75 adddird ⊢N∈ℕ→N+1+1⋅ N=N+1⋅ N+1⋅ N
149 148 oveq1d ⊢N∈ℕ→N+1+1⋅ N+1=N+1⋅ N+1⋅ N+1
150 75 mullidd ⊢N∈ℕ→1⋅ N=N
151 150 oveq2d ⊢N∈ℕ→N+1⋅ N+1⋅ N=N+1⋅ N+N
152 151 oveq1d ⊢N∈ℕ→N+1⋅ N+1⋅ N+1=N+1⋅ N+N+1
153 124 75 mulcld ⊢N∈ℕ→N+1⋅ N∈ℂ
154 153 75 143 addassd ⊢N∈ℕ→N+1⋅ N+N+1=N+1⋅ N+N+1
155 149 152 154 3eqtrd ⊢N∈ℕ→N+1+1⋅ N+1=N+1⋅ N+N+1
156 147 155 eqtr4d ⊢N∈ℕ→N⁢N+1+1⁢N+1=N+1+1⋅ N+1
157 142 144 156 3eqtrd ⊢N∈ℕ→1⁢N+1⁢N+1=N+1+1⋅ N+1
158 141 157 breqtrrd ⊢N∈ℕ→N+1+1⋅ N<1⁢N+1⁢N+1
159 nnre ⊢N∈ℕ→N∈ℝ
160 nngt0 ⊢N∈ℕ→0<N
161 159 160 jca ⊢N∈ℕ→N∈ℝ∧0<N
162 1red ⊢N∈ℕ→1∈ℝ
163 nnre ⊢N+1⁢N+1∈ℕ→N+1⁢N+1∈ℝ
164 nngt0 ⊢N+1⁢N+1∈ℕ→0<N+1⁢N+1
165 163 164 jca ⊢N+1⁢N+1∈ℕ→N+1⁢N+1∈ℝ∧0<N+1⁢N+1
166 23 165 syl ⊢N∈ℕ→N+1⁢N+1∈ℝ∧0<N+1⁢N+1
167 lt2mul2div ⊢N+1+1∈ℝ∧N∈ℝ∧0<N∧1∈ℝ∧N+1⁢N+1∈ℝ∧0<N+1⁢N+1→N+1+1⋅ N<1⁢N+1⁢N+1↔N+1+1N+1⁢N+1<1N
168 22 161 162 166 167 syl22anc ⊢N∈ℕ→N+1+1⋅ N<1⁢N+1⁢N+1↔N+1+1N+1⁢N+1<1N
169 158 168 mpbid ⊢N∈ℕ→N+1+1N+1⁢N+1<1N
170 19 24 25 137 169 lelttrd ⊢N∈ℕ→N!e−S⁡N<1N