Description: The subfactorial is defined as the number of derangements (see derangval ) of the set ( 1 ... N ) . (Contributed by Mario Carneiro, 21-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | derang.d | ||
subfac.n | |||
Assertion | subfacval |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | derang.d | ||
2 | subfac.n | ||
3 | oveq2 | ||
4 | 3 | fveq2d | |
5 | fvex | ||
6 | 4 2 5 | fvmpt |