Theorem derangfmla

Description: The derangements formula, which expresses the number of derangements of a finite nonempty set in terms of the factorial. The expression |_( x + 1 / 2 ) is a way of saying "rounded to the nearest integer". This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015)

	Ref	Expression
Hypothesis	derangfmla.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
Assertion	derangfmla	|- ( ( A e. Fin /\ A =/= (/) ) -> ( D ` A ) = ( |_ ` ( ( ( ! ` ( # ` A ) ) / _e ) + ( 1 / 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		derangfmla.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2		oveq2	|- ( n = m -> ( 1 ... n ) = ( 1 ... m ) )
3	2	fveq2d	|- ( n = m -> ( D ` ( 1 ... n ) ) = ( D ` ( 1 ... m ) ) )
4	3	cbvmptv	|- ( n e. NN0 |-> ( D ` ( 1 ... n ) ) ) = ( m e. NN0 |-> ( D ` ( 1 ... m ) ) )
5	1 4	derangen2	|- ( A e. Fin -> ( D ` A ) = ( ( n e. NN0 |-> ( D ` ( 1 ... n ) ) ) ` ( # ` A ) ) )
6	5	adantr	|- ( ( A e. Fin /\ A =/= (/) ) -> ( D ` A ) = ( ( n e. NN0 |-> ( D ` ( 1 ... n ) ) ) ` ( # ` A ) ) )
7		hashnncl	|- ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
8	7	biimpar	|- ( ( A e. Fin /\ A =/= (/) ) -> ( # ` A ) e. NN )
9	1 4	subfacval3	|- ( ( # ` A ) e. NN -> ( ( n e. NN0 |-> ( D ` ( 1 ... n ) ) ) ` ( # ` A ) ) = ( |_ ` ( ( ( ! ` ( # ` A ) ) / _e ) + ( 1 / 2 ) ) ) )
10	8 9	syl	|- ( ( A e. Fin /\ A =/= (/) ) -> ( ( n e. NN0 |-> ( D ` ( 1 ... n ) ) ) ` ( # ` A ) ) = ( |_ ` ( ( ( ! ` ( # ` A ) ) / _e ) + ( 1 / 2 ) ) ) )
11	6 10	eqtrd	|- ( ( A e. Fin /\ A =/= (/) ) -> ( D ` A ) = ( |_ ` ( ( ( ! ` ( # ` A ) ) / _e ) + ( 1 / 2 ) ) ) )