# Metamath Proof Explorer

## 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 {x}\phantom{\rule{.4em}{0ex}}{f}\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 {x}\phantom{\rule{.4em}{0ex}}{f}\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 {ℕ}_{0}⟼{D}\left(\left(1\dots {n}\right)\right)\right)=\left({m}\in {ℕ}_{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 {ℕ}_{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 {ℕ}_{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 ℕ↔{A}\ne \varnothing \right)$
8 7 biimpar ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left|{A}\right|\in ℕ$
9 1 4 subfacval3 ${⊢}\left|{A}\right|\in ℕ\to \left({n}\in {ℕ}_{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 {ℕ}_{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)⌋$