# 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}\in \left(0\dots {N}\right)\to \frac{{N}!}{{R}!}\in ℕ$

### Proof

Step Hyp Ref Expression
1 elfznn0 ${⊢}{R}\in \left(0\dots {N}\right)\to {R}\in {ℕ}_{0}$
2 1 faccld ${⊢}{R}\in \left(0\dots {N}\right)\to {R}!\in ℕ$
3 fznn0sub ${⊢}{R}\in \left(0\dots {N}\right)\to {N}-{R}\in {ℕ}_{0}$
4 3 faccld ${⊢}{R}\in \left(0\dots {N}\right)\to \left({N}-{R}\right)!\in ℕ$
5 4 2 nnmulcld ${⊢}{R}\in \left(0\dots {N}\right)\to \left({N}-{R}\right)!{R}!\in ℕ$
6 elfz3nn0 ${⊢}{R}\in \left(0\dots {N}\right)\to {N}\in {ℕ}_{0}$
7 faccl ${⊢}{N}\in {ℕ}_{0}\to {N}!\in ℕ$
8 7 nncnd ${⊢}{N}\in {ℕ}_{0}\to {N}!\in ℂ$
9 6 8 syl ${⊢}{R}\in \left(0\dots {N}\right)\to {N}!\in ℂ$
10 4 nncnd ${⊢}{R}\in \left(0\dots {N}\right)\to \left({N}-{R}\right)!\in ℂ$
11 2 nncnd ${⊢}{R}\in \left(0\dots {N}\right)\to {R}!\in ℂ$
12 facne0 ${⊢}{R}\in {ℕ}_{0}\to {R}!\ne 0$
13 1 12 syl ${⊢}{R}\in \left(0\dots {N}\right)\to {R}!\ne 0$
14 10 11 13 divcan4d ${⊢}{R}\in \left(0\dots {N}\right)\to \frac{\left({N}-{R}\right)!{R}!}{{R}!}=\left({N}-{R}\right)!$
15 14 4 eqeltrd ${⊢}{R}\in \left(0\dots {N}\right)\to \frac{\left({N}-{R}\right)!{R}!}{{R}!}\in ℕ$
16 bcval2 ${⊢}{R}\in \left(0\dots {N}\right)\to \left(\genfrac{}{}{0}{}{{N}}{{R}}\right)=\frac{{N}!}{\left({N}-{R}\right)!{R}!}$
17 bccl2 ${⊢}{R}\in \left(0\dots {N}\right)\to \left(\genfrac{}{}{0}{}{{N}}{{R}}\right)\in ℕ$
18 16 17 eqeltrrd ${⊢}{R}\in \left(0\dots {N}\right)\to \frac{{N}!}{\left({N}-{R}\right)!{R}!}\in ℕ$
19 nndivtr ${⊢}\left(\left({R}!\in ℕ\wedge \left({N}-{R}\right)!{R}!\in ℕ\wedge {N}!\in ℂ\right)\wedge \left(\frac{\left({N}-{R}\right)!{R}!}{{R}!}\in ℕ\wedge \frac{{N}!}{\left({N}-{R}\right)!{R}!}\in ℕ\right)\right)\to \frac{{N}!}{{R}!}\in ℕ$
20 2 5 9 15 18 19 syl32anc ${⊢}{R}\in \left(0\dots {N}\right)\to \frac{{N}!}{{R}!}\in ℕ$