Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Derangements and the Subfactorial
subfac0
Next ⟩
subfac1
Metamath Proof Explorer
Ascii
Unicode
Theorem
subfac0
Description:
The subfactorial at zero.
(Contributed by
Mario Carneiro
, 19-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
subfac0
⊢
S
⁡
0
=
1
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
0nn0
⊢
0
∈
ℕ
0
4
1
2
subfacval
⊢
0
∈
ℕ
0
→
S
⁡
0
=
D
⁡
1
…
0
5
3
4
ax-mp
⊢
S
⁡
0
=
D
⁡
1
…
0
6
fz10
⊢
1
…
0
=
∅
7
6
fveq2i
⊢
D
⁡
1
…
0
=
D
⁡
∅
8
1
derang0
⊢
D
⁡
∅
=
1
9
5
7
8
3eqtri
⊢
S
⁡
0
=
1