Theorem subfacval3

Description: Another closed form expression for the subfactorial. The expression |_( x + 1 / 2 ) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
	subfac.n	$$⊢S=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)$$
Assertion	subfacval3	$$⊢N\in \mathbb{N}\to S\left(N\right)=⌊\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$$⊢D=\left(x\in \mathrm{Fin}⟼\left|\left\{f|\left(f:x\underset{1-1\; onto}{⟶}x\wedge \forall y\in xf\left(y\right)\ne y\right)\right\}\right|\right)$$
2		subfac.n	$$⊢S=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)$$
3		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
4	1 2	subfacf	$$⊢S:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
5	4	ffvelcdmi	$$⊢N\in {\mathbb{N}}_0\to S\left(N\right)\in {\mathbb{N}}_0$$
6	3 5	syl	$$⊢N\in \mathbb{N}\to S\left(N\right)\in {\mathbb{N}}_0$$
7	6	nn0zd	$$⊢N\in \mathbb{N}\to S\left(N\right)\in \mathbb{Z}$$
8	7	zred	$$⊢N\in \mathbb{N}\to S\left(N\right)\in ℝ$$
9		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
10	3 9	syl	$$⊢N\in \mathbb{N}\to N!\in \mathbb{N}$$
11	10	nnred	$$⊢N\in \mathbb{N}\to N!\in ℝ$$
12		epr	$$⊢\mathrm{e}\in {ℝ}^{+}$$
13		rerpdivcl	$$⊢\left(N!\in ℝ\wedge \mathrm{e}\in {ℝ}^{+}\right)\to \frac{N!}{\mathrm{e}}\in ℝ$$
14	11 12 13	sylancl	$$⊢N\in \mathbb{N}\to \frac{N!}{\mathrm{e}}\in ℝ$$
15		halfre	$$⊢\frac{1}{2}\in ℝ$$
16		readdcl	$$⊢\left(\frac{N!}{\mathrm{e}}\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\in ℝ$$
17	14 15 16	sylancl	$$⊢N\in \mathbb{N}\to \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\in ℝ$$
18		elnn1uz2	$$⊢N\in \mathbb{N}\leftrightarrow \left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)$$
19		fveq2	$$⊢N=1\to N!=1!$$
20		fac1	$$⊢1!=1$$
21	19 20	eqtrdi	$$⊢N=1\to N!=1$$
22	21	oveq1d	$$⊢N=1\to \frac{N!}{\mathrm{e}}=\frac{1}{\mathrm{e}}$$
23		fveq2	$$⊢N=1\to S\left(N\right)=S\left(1\right)$$
24	1 2	subfac1	$$⊢S\left(1\right)=0$$
25	23 24	eqtrdi	$$⊢N=1\to S\left(N\right)=0$$
26	22 25	oveq12d	$$⊢N=1\to \left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)=\left(\frac{1}{\mathrm{e}}\right)-0$$
27		rpreccl	$$⊢\mathrm{e}\in {ℝ}^{+}\to \frac{1}{\mathrm{e}}\in {ℝ}^{+}$$
28	12 27	ax-mp	$$⊢\frac{1}{\mathrm{e}}\in {ℝ}^{+}$$
29		rpre	$$⊢\frac{1}{\mathrm{e}}\in {ℝ}^{+}\to \frac{1}{\mathrm{e}}\in ℝ$$
30	28 29	ax-mp	$$⊢\frac{1}{\mathrm{e}}\in ℝ$$
31	30	recni	$$⊢\frac{1}{\mathrm{e}}\in ℂ$$
32	31	subid1i	$$⊢\left(\frac{1}{\mathrm{e}}\right)-0=\frac{1}{\mathrm{e}}$$
33	26 32	eqtrdi	$$⊢N=1\to \left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)=\frac{1}{\mathrm{e}}$$
34	33	fveq2d	$$⊢N=1\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|=\left|\frac{1}{\mathrm{e}}\right|$$
35		rpge0	$$⊢\frac{1}{\mathrm{e}}\in {ℝ}^{+}\to 0\le \frac{1}{\mathrm{e}}$$
36	28 35	ax-mp	$$⊢0\le \frac{1}{\mathrm{e}}$$
37		absid	$$⊢\left(\frac{1}{\mathrm{e}}\in ℝ\wedge 0\le \frac{1}{\mathrm{e}}\right)\to \left|\frac{1}{\mathrm{e}}\right|=\frac{1}{\mathrm{e}}$$
38	30 36 37	mp2an	$$⊢\left|\frac{1}{\mathrm{e}}\right|=\frac{1}{\mathrm{e}}$$
39	34 38	eqtrdi	$$⊢N=1\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|=\frac{1}{\mathrm{e}}$$
40		egt2lt3	$$⊢\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$$
41	40	simpli	$$⊢2<\mathrm{e}$$
42		2re	$$⊢2\in ℝ$$
43		ere	$$⊢\mathrm{e}\in ℝ$$
44		2pos	$$⊢0<2$$
45		epos	$$⊢0<\mathrm{e}$$
46	42 43 44 45	ltrecii	$$⊢2<\mathrm{e}\leftrightarrow \frac{1}{\mathrm{e}}<\frac{1}{2}$$
47	41 46	mpbi	$$⊢\frac{1}{\mathrm{e}}<\frac{1}{2}$$
48	39 47	eqbrtrdi	$$⊢N=1\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{2}$$
49		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
50	14 8	resubcld	$$⊢N\in \mathbb{N}\to \left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\in ℝ$$
51	50	recnd	$$⊢N\in \mathbb{N}\to \left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\in ℂ$$
52	49 51	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\in ℂ$$
53	52	abscld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|\in ℝ$$
54	49	nnrecred	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}\in ℝ$$
55	15	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{2}\in ℝ$$
56	1 2	subfaclim	$$⊢N\in \mathbb{N}\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{N}$$
57	49 56	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{N}$$
58		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 2\le N$$
59		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
60		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
61		lerec	$$⊢\left(\left(2\in ℝ\wedge 0<2\right)\wedge \left(N\in ℝ\wedge 0<N\right)\right)\to \left(2\le N\leftrightarrow \frac{1}{N}\le \frac{1}{2}\right)$$
62	42 44 61	mpanl12	$$⊢\left(N\in ℝ\wedge 0<N\right)\to \left(2\le N\leftrightarrow \frac{1}{N}\le \frac{1}{2}\right)$$
63	59 60 62	syl2anc	$$⊢N\in \mathbb{N}\to \left(2\le N\leftrightarrow \frac{1}{N}\le \frac{1}{2}\right)$$
64	49 63	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(2\le N\leftrightarrow \frac{1}{N}\le \frac{1}{2}\right)$$
65	58 64	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}\le \frac{1}{2}$$
66	53 54 55 57 65	ltletrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{2}$$
67	48 66	jaoi	$$⊢\left(N=1\vee N\in {\mathbb{Z}}_{\ge 2}\right)\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{2}$$
68	18 67	sylbi	$$⊢N\in \mathbb{N}\to \left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{2}$$
69	15	a1i	$$⊢N\in \mathbb{N}\to \frac{1}{2}\in ℝ$$
70	14 8 69	absdifltd	$$⊢N\in \mathbb{N}\to \left(\left|\left(\frac{N!}{\mathrm{e}}\right)-S\left(N\right)\right|<\frac{1}{2}\leftrightarrow \left(S\left(N\right)-\left(\frac{1}{2}\right)<\frac{N!}{\mathrm{e}}\wedge \frac{N!}{\mathrm{e}}<S\left(N\right)+\left(\frac{1}{2}\right)\right)\right)$$
71	68 70	mpbid	$$⊢N\in \mathbb{N}\to \left(S\left(N\right)-\left(\frac{1}{2}\right)<\frac{N!}{\mathrm{e}}\wedge \frac{N!}{\mathrm{e}}<S\left(N\right)+\left(\frac{1}{2}\right)\right)$$
72	71	simpld	$$⊢N\in \mathbb{N}\to S\left(N\right)-\left(\frac{1}{2}\right)<\frac{N!}{\mathrm{e}}$$
73	8 69 14	ltsubaddd	$$⊢N\in \mathbb{N}\to \left(S\left(N\right)-\left(\frac{1}{2}\right)<\frac{N!}{\mathrm{e}}\leftrightarrow S\left(N\right)<\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\right)$$
74	72 73	mpbid	$$⊢N\in \mathbb{N}\to S\left(N\right)<\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)$$
75	8 17 74	ltled	$$⊢N\in \mathbb{N}\to S\left(N\right)\le \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)$$
76		readdcl	$$⊢\left(S\left(N\right)\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to S\left(N\right)+\left(\frac{1}{2}\right)\in ℝ$$
77	8 15 76	sylancl	$$⊢N\in \mathbb{N}\to S\left(N\right)+\left(\frac{1}{2}\right)\in ℝ$$
78	71	simprd	$$⊢N\in \mathbb{N}\to \frac{N!}{\mathrm{e}}<S\left(N\right)+\left(\frac{1}{2}\right)$$
79	14 77 69 78	ltadd1dd	$$⊢N\in \mathbb{N}\to \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)<S\left(N\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
80	8	recnd	$$⊢N\in \mathbb{N}\to S\left(N\right)\in ℂ$$
81	69	recnd	$$⊢N\in \mathbb{N}\to \frac{1}{2}\in ℂ$$
82	80 81 81	addassd	$$⊢N\in \mathbb{N}\to S\left(N\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=S\left(N\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
83		ax-1cn	$$⊢1\in ℂ$$
84		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
85	83 84	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
86	85	oveq2i	$$⊢S\left(N\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=S\left(N\right)+1$$
87	82 86	eqtrdi	$$⊢N\in \mathbb{N}\to S\left(N\right)+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=S\left(N\right)+1$$
88	79 87	breqtrd	$$⊢N\in \mathbb{N}\to \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)<S\left(N\right)+1$$
89		flbi	$$⊢\left(\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\in ℝ\wedge S\left(N\right)\in \mathbb{Z}\right)\to \left(⌊\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋=S\left(N\right)\leftrightarrow \left(S\left(N\right)\le \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\wedge \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)<S\left(N\right)+1\right)\right)$$
90	17 7 89	syl2anc	$$⊢N\in \mathbb{N}\to \left(⌊\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋=S\left(N\right)\leftrightarrow \left(S\left(N\right)\le \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)\wedge \left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)<S\left(N\right)+1\right)\right)$$
91	75 88 90	mpbir2and	$$⊢N\in \mathbb{N}\to ⌊\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋=S\left(N\right)$$
92	91	eqcomd	$$⊢N\in \mathbb{N}\to S\left(N\right)=⌊\left(\frac{N!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$