This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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