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	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
Assertion	derangfmla	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝐷 ‘ 𝐴 ) = ( ⌊ ‘ ( ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) / e ) + ( 1 / 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		derangfmla.d	⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
2		oveq2	⊢ ( 𝑛 = 𝑚 → ( 1 ... 𝑛 ) = ( 1 ... 𝑚 ) )
3	2	fveq2d	⊢ ( 𝑛 = 𝑚 → ( 𝐷 ‘ ( 1 ... 𝑛 ) ) = ( 𝐷 ‘ ( 1 ... 𝑚 ) ) )
4	3	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑚 ) ) )
5	1 4	derangen2	⊢ ( 𝐴 ∈ Fin → ( 𝐷 ‘ 𝐴 ) = ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝐷 ‘ 𝐴 ) = ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
7		hashnncl	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
8	7	biimpar	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
9	1 4	subfacval3	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ⌊ ‘ ( ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) / e ) + ( 1 / 2 ) ) ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ⌊ ‘ ( ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) / e ) + ( 1 / 2 ) ) ) )
11	6 10	eqtrd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝐷 ‘ 𝐴 ) = ( ⌊ ‘ ( ( ( ! ‘ ( ♯ ‘ 𝐴 ) ) / e ) + ( 1 / 2 ) ) ) )