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	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑀 ) ∥ ( ! ‘ 𝑁 ) )

Proof

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