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

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$⊢ R \in (0 \dots N) \to R \in ℕ_{0}$
2	1	faccld	$⊢ R \in (0 \dots N) \to R! \in ℕ$
3		fznn0sub	$⊢ R \in (0 \dots N) \to N - R \in ℕ_{0}$
4	3	faccld	$⊢ R \in (0 \dots N) \to (N - R)! \in ℕ$
5	4 2	nnmulcld	$⊢ R \in (0 \dots N) \to (N - R)! R! \in ℕ$
6		elfz3nn0	$⊢ R \in (0 \dots N) \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 (0 \dots N) \to N! \in ℂ$
10	4	nncnd	$⊢ R \in (0 \dots N) \to (N - R)! \in ℂ$
11	2	nncnd	$⊢ R \in (0 \dots N) \to R! \in ℂ$
12		facne0	$⊢ R \in ℕ_{0} \to R! \neq 0$
13	1 12	syl	$⊢ R \in (0 \dots N) \to R! \neq 0$
14	10 11 13	divcan4d	$⊢ R \in (0 \dots N) \to \frac{(N - R)! R!}{R!} = (N - R)!$
15	14 4	eqeltrd	$⊢ R \in (0 \dots N) \to \frac{(N - R)! R!}{R!} \in ℕ$
16		bcval2	$⊢ R \in (0 \dots N) \to (\binom{N}{R}) = \frac{N!}{(N - R)! R!}$
17		bccl2	$⊢ R \in (0 \dots N) \to (\binom{N}{R}) \in ℕ$
18	16 17	eqeltrrd	$⊢ R \in (0 \dots N) \to \frac{N!}{(N - R)! R!} \in ℕ$
19		nndivtr	$⊢ ((R! \in ℕ \land (N - R)! R! \in ℕ \land N! \in ℂ) \land (\frac{(N - R)! R!}{R!} \in ℕ \land \frac{N!}{(N - R)! R!} \in ℕ)) \to \frac{N!}{R!} \in ℕ$
20	2 5 9 15 18 19	syl32anc	$⊢ R \in (0 \dots N) \to \frac{N!}{R!} \in ℕ$

Metamath Proof Explorer

Theorem permnn

Proof