Metamath Proof Explorer

Theorem derangen2

Description: Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
subfac.n ⊢ S = n ∈ ℕ 0 ⟼ D ⁡ 1 … n
Assertion derangen2 ⊢ A ∈ Fin → D ⁡ A = S ⁡ A

Proof

Step Hyp Ref Expression
1 derang.d ⊢ D = x ∈ Fin ⟼ f | f : x ⟶ 1-1 onto x ∧ ∀ y ∈ x f ⁡ y ≠ y
2 subfac.n ⊢ S = n ∈ ℕ 0 ⟼ D ⁡ 1 … n
3 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
4 1 2 subfacval ⊢ A ∈ ℕ 0 → S ⁡ A = D ⁡ 1 … A
5 3 4 syl ⊢ A ∈ Fin → S ⁡ A = D ⁡ 1 … A
6 hashfz1 ⊢ A ∈ ℕ 0 → 1 … A = A
7 3 6 syl ⊢ A ∈ Fin → 1 … A = A
8 fzfid ⊢ A ∈ Fin → 1 … A ∈ Fin
9 hashen ⊢ 1 … A ∈ Fin ∧ A ∈ Fin → 1 … A = A ↔ 1 … A ≈ A
10 8 9 mpancom ⊢ A ∈ Fin → 1 … A = A ↔ 1 … A ≈ A
11 7 10 mpbid ⊢ A ∈ Fin → 1 … A ≈ A
12 1 derangen ⊢ 1 … A ≈ A ∧ A ∈ Fin → D ⁡ 1 … A = D ⁡ A
13 11 12 mpancom ⊢ A ∈ Fin → D ⁡ 1 … A = D ⁡ A
14 5 13 eqtr2d ⊢ A ∈ Fin → D ⁡ A = S ⁡ A