subfacp1

Description: A two-term recurrence for the subfactorial. This theorem allows to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 , subfac1 . (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
Assertion	subfacp1	$⊢ N \in ℕ \to S (N + 1) = N (S (N) + S (N - 1))$

Proof

Step	Hyp	Ref	Expression
1		derang.d	$⊢ D = (x \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
2		subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
3		f1oeq1	$⊢ g = f \to (g : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \leftrightarrow f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1))$
4		fveq2	$⊢ z = y \to g (z) = g (y)$
5		id	$⊢ z = y \to z = y$
6	4 5	neeq12d	$⊢ z = y \to (g (z) \neq z \leftrightarrow g (y) \neq y)$
7	6	cbvralvw	$⊢ \forall z \in (1 \dots N + 1) g (z) \neq z \leftrightarrow \forall y \in (1 \dots N + 1) g (y) \neq y$
8		fveq1	$⊢ g = f \to g (y) = f (y)$
9	8	neeq1d	$⊢ g = f \to (g (y) \neq y \leftrightarrow f (y) \neq y)$
10	9	ralbidv	$⊢ g = f \to (\forall y \in (1 \dots N + 1) g (y) \neq y \leftrightarrow \forall y \in (1 \dots N + 1) f (y) \neq y)$
11	7 10	bitrid	$⊢ g = f \to (\forall z \in (1 \dots N + 1) g (z) \neq z \leftrightarrow \forall y \in (1 \dots N + 1) f (y) \neq y)$
12	3 11	anbi12d	$⊢ g = f \to ((g : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall z \in (1 \dots N + 1) g (z) \neq z) \leftrightarrow (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y))$
13	12	cbvabv	$⊢ \{g \| (g : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall z \in (1 \dots N + 1) g (z) \neq z)\} = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
14	1 2 13	subfacp1lem6	$⊢ N \in ℕ \to S (N + 1) = N (S (N) + S (N - 1))$

Metamath Proof Explorer

Theorem subfacp1

Proof