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 \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
Assertion	subfaclim	$⊢ N \in ℕ \to \|(\frac{N!}{e}) - S (N)\| < \frac{1}{N}$

Proof

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

Metamath Proof Explorer

Theorem subfaclim

Proof