Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Derangements and the Subfactorial
subfac1
Next ⟩
subfacp1lem1
Metamath Proof Explorer
Ascii
Unicode
Theorem
subfac1
Description:
The subfactorial at one.
(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
subfac1
⊢
S
⁡
1
=
0
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
1nn0
⊢
1
∈
ℕ
0
4
1
2
subfacval
⊢
1
∈
ℕ
0
→
S
⁡
1
=
D
⁡
1
…
1
5
3
4
ax-mp
⊢
S
⁡
1
=
D
⁡
1
…
1
6
1z
⊢
1
∈
ℤ
7
fzsn
⊢
1
∈
ℤ
→
1
…
1
=
1
8
6
7
ax-mp
⊢
1
…
1
=
1
9
8
fveq2i
⊢
D
⁡
1
…
1
=
D
⁡
1
10
1
derangsn
⊢
1
∈
ℕ
0
→
D
⁡
1
=
0
11
3
10
ax-mp
⊢
D
⁡
1
=
0
12
5
9
11
3eqtri
⊢
S
⁡
1
=
0