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 ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ! ‘ 𝑅 ) ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 elfznn0 ( 𝑅 ∈ ( 0 ... 𝑁 ) → 𝑅 ∈ ℕ0 )
2 1 faccld ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑅 ) ∈ ℕ )
3 fznn0sub ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( 𝑁𝑅 ) ∈ ℕ0 )
4 3 faccld ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁𝑅 ) ) ∈ ℕ )
5 4 2 nnmulcld ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) ∈ ℕ )
6 elfz3nn0 ( 𝑅 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
7 faccl ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
8 7 nncnd ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℂ )
9 6 8 syl ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
10 4 nncnd ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁𝑅 ) ) ∈ ℂ )
11 2 nncnd ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑅 ) ∈ ℂ )
12 facne0 ( 𝑅 ∈ ℕ0 → ( ! ‘ 𝑅 ) ≠ 0 )
13 1 12 syl ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑅 ) ≠ 0 )
14 10 11 13 divcan4d ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) / ( ! ‘ 𝑅 ) ) = ( ! ‘ ( 𝑁𝑅 ) ) )
15 14 4 eqeltrd ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) / ( ! ‘ 𝑅 ) ) ∈ ℕ )
16 bcval2 ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑅 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) ) )
17 bccl2 ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑅 ) ∈ ℕ )
18 16 17 eqeltrrd ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) ) ∈ ℕ )
19 nndivtr ( ( ( ( ! ‘ 𝑅 ) ∈ ℕ ∧ ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) ∈ ℕ ∧ ( ! ‘ 𝑁 ) ∈ ℂ ) ∧ ( ( ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) / ( ! ‘ 𝑅 ) ) ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁𝑅 ) ) · ( ! ‘ 𝑅 ) ) ) ∈ ℕ ) ) → ( ( ! ‘ 𝑁 ) / ( ! ‘ 𝑅 ) ) ∈ ℕ )
20 2 5 9 15 18 19 syl32anc ( 𝑅 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ! ‘ 𝑅 ) ) ∈ ℕ )