Metamath Proof Explorer

Theorem permnn

Description: The number of permutations of N - R objects from a collection of N objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007)

Ref Expression
Assertion permnn 
|- ( R e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` R ) ) e. NN )

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( R e. ( 0 ... N ) -> R e. NN0 )
2 1 faccld 
 |-  ( R e. ( 0 ... N ) -> ( ! ` R ) e. NN )
3 fznn0sub 
 |-  ( R e. ( 0 ... N ) -> ( N - R ) e. NN0 )
4 3 faccld 
 |-  ( R e. ( 0 ... N ) -> ( ! ` ( N - R ) ) e. NN )
5 4 2 nnmulcld 
 |-  ( R e. ( 0 ... N ) -> ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) e. NN )
6 elfz3nn0 
 |-  ( R e. ( 0 ... N ) -> N e. NN0 )
7 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
8 7 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
9 6 8 syl 
 |-  ( R e. ( 0 ... N ) -> ( ! ` N ) e. CC )
10 4 nncnd 
 |-  ( R e. ( 0 ... N ) -> ( ! ` ( N - R ) ) e. CC )
11 2 nncnd 
 |-  ( R e. ( 0 ... N ) -> ( ! ` R ) e. CC )
12 facne0 
 |-  ( R e. NN0 -> ( ! ` R ) =/= 0 )
13 1 12 syl 
 |-  ( R e. ( 0 ... N ) -> ( ! ` R ) =/= 0 )
14 10 11 13 divcan4d 
 |-  ( R e. ( 0 ... N ) -> ( ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) / ( ! ` R ) ) = ( ! ` ( N - R ) ) )
15 14 4 eqeltrd 
 |-  ( R e. ( 0 ... N ) -> ( ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) / ( ! ` R ) ) e. NN )
16 bcval2 
 |-  ( R e. ( 0 ... N ) -> ( N _C R ) = ( ( ! ` N ) / ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) ) )
17 bccl2 
 |-  ( R e. ( 0 ... N ) -> ( N _C R ) e. NN )
18 16 17 eqeltrrd 
 |-  ( R e. ( 0 ... N ) -> ( ( ! ` N ) / ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) ) e. NN )
19 nndivtr 
 |-  ( ( ( ( ! ` R ) e. NN /\ ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) e. NN /\ ( ! ` N ) e. CC ) /\ ( ( ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) / ( ! ` R ) ) e. NN /\ ( ( ! ` N ) / ( ( ! ` ( N - R ) ) x. ( ! ` R ) ) ) e. NN ) ) -> ( ( ! ` N ) / ( ! ` R ) ) e. NN )
20 2 5 9 15 18 19 syl32anc 
 |-  ( R e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` R ) ) e. NN )