Metamath Proof Explorer

Theorem facnn0dvdsfac

Description: The factorial of a nonnegative integer divides the factorial of an integer which is greater than or equal to the first integer. (Contributed by AV, 6-Apr-2026)

Ref Expression
Assertion facnn0dvdsfac ⊢ M ∈ 0 … N → M ! ∥ N !

Proof

Step Hyp Ref Expression
1 permnn ⊢ M ∈ 0 … N → N ! M ! ∈ ℕ
2 nnz ⊢ N ! M ! ∈ ℕ → N ! M ! ∈ ℤ
3 1 2 syl ⊢ M ∈ 0 … N → N ! M ! ∈ ℤ
4 elfznn0 ⊢ M ∈ 0 … N → M ∈ ℕ 0
5 faccl ⊢ M ∈ ℕ 0 → M ! ∈ ℕ
6 4 5 syl ⊢ M ∈ 0 … N → M ! ∈ ℕ
7 6 nnzd ⊢ M ∈ 0 … N → M ! ∈ ℤ
8 facne0 ⊢ M ∈ ℕ 0 → M ! ≠ 0
9 4 8 syl ⊢ M ∈ 0 … N → M ! ≠ 0
10 elfz3nn0 ⊢ M ∈ 0 … N → N ∈ ℕ 0
11 faccl ⊢ N ∈ ℕ 0 → N ! ∈ ℕ
12 10 11 syl ⊢ M ∈ 0 … N → N ! ∈ ℕ
13 12 nnzd ⊢ M ∈ 0 … N → N ! ∈ ℤ
14 7 9 13 3jca ⊢ M ∈ 0 … N → M ! ∈ ℤ ∧ M ! ≠ 0 ∧ N ! ∈ ℤ
15 dvdsval2 ⊢ M ! ∈ ℤ ∧ M ! ≠ 0 ∧ N ! ∈ ℤ → M ! ∥ N ! ↔ N ! M ! ∈ ℤ
16 14 15 syl ⊢ M ∈ 0 … N → M ! ∥ N ! ↔ N ! M ! ∈ ℤ
17 3 16 mpbird ⊢ M ∈ 0 … N → M ! ∥ N !