Theorem derangfmla

Description: The derangements formula, which expresses the number of derangements of a finite nonempty set in terms of the factorial. The expression |_( x + 1 / 2 ) is a way of saying "rounded to the nearest integer". This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Hypothesis	derangfmla.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)$$
Assertion	derangfmla	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to D\left(A\right)=⌊\left(\frac{\left|A\right|!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$

Proof

Step	Hyp	Ref	Expression
1		derangfmla.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		oveq2	$$⊢n=m\to \left(1\dots n\right)=\left(1\dots m\right)$$
3	2	fveq2d	$$⊢n=m\to D\left(\left(1\dots n\right)\right)=D\left(\left(1\dots m\right)\right)$$
4	3	cbvmptv	$$⊢\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)=\left(m\in {\mathbb{N}}_0⟼D\left(\left(1\dots m\right)\right)\right)$$
5	1 4	derangen2	$$⊢A\in \mathrm{Fin}\to D\left(A\right)=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)\left(\left|A\right|\right)$$
6	5	adantr	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to D\left(A\right)=\left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)\left(\left|A\right|\right)$$
7		hashnncl	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|\in \mathbb{N}\leftrightarrow A\ne \varnothing \right)$$
8	7	biimpar	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to \left|A\right|\in \mathbb{N}$$
9	1 4	subfacval3	$$⊢\left|A\right|\in \mathbb{N}\to \left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)\left(\left|A\right|\right)=⌊\left(\frac{\left|A\right|!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$
10	8 9	syl	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to \left(n\in {\mathbb{N}}_0⟼D\left(\left(1\dots n\right)\right)\right)\left(\left|A\right|\right)=⌊\left(\frac{\left|A\right|!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$
11	6 10	eqtrd	$$⊢\left(A\in \mathrm{Fin}\wedge A\ne \varnothing \right)\to D\left(A\right)=⌊\left(\frac{\left|A\right|!}{\mathrm{e}}\right)+\left(\frac{1}{2}\right)⌋$$