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 ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
Assertion subfaclim ( 𝑁 ∈ ℕ → ( abs ‘ ( ( ( ! ‘ 𝑁 ) / e ) − ( 𝑆 ‘ 𝑁 ) ) ) < ( 1 / 𝑁 ) )

Proof

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