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 / 𝑁 ) )