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