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 e. ( 0 ... N ) -> ( ! ` M ) || ( ! ` N ) )

Proof

Step	Hyp	Ref	Expression
1		permnn	|- ( M e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` M ) ) e. NN )
2		nnz	|- ( ( ( ! ` N ) / ( ! ` M ) ) e. NN -> ( ( ! ` N ) / ( ! ` M ) ) e. ZZ )
3	1 2	syl	|- ( M e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` M ) ) e. ZZ )
4		elfznn0	|- ( M e. ( 0 ... N ) -> M e. NN0 )
5		faccl	|- ( M e. NN0 -> ( ! ` M ) e. NN )
6	4 5	syl	|- ( M e. ( 0 ... N ) -> ( ! ` M ) e. NN )
7	6	nnzd	|- ( M e. ( 0 ... N ) -> ( ! ` M ) e. ZZ )
8		facne0	|- ( M e. NN0 -> ( ! ` M ) =/= 0 )
9	4 8	syl	|- ( M e. ( 0 ... N ) -> ( ! ` M ) =/= 0 )
10		elfz3nn0	|- ( M e. ( 0 ... N ) -> N e. NN0 )
11		faccl	|- ( N e. NN0 -> ( ! ` N ) e. NN )
12	10 11	syl	|- ( M e. ( 0 ... N ) -> ( ! ` N ) e. NN )
13	12	nnzd	|- ( M e. ( 0 ... N ) -> ( ! ` N ) e. ZZ )
14	7 9 13	3jca	|- ( M e. ( 0 ... N ) -> ( ( ! ` M ) e. ZZ /\ ( ! ` M ) =/= 0 /\ ( ! ` N ) e. ZZ ) )
15		dvdsval2	|- ( ( ( ! ` M ) e. ZZ /\ ( ! ` M ) =/= 0 /\ ( ! ` N ) e. ZZ ) -> ( ( ! ` M ) || ( ! ` N ) <-> ( ( ! ` N ) / ( ! ` M ) ) e. ZZ ) )
16	14 15	syl	|- ( M e. ( 0 ... N ) -> ( ( ! ` M ) || ( ! ` N ) <-> ( ( ! ` N ) / ( ! ` M ) ) e. ZZ ) )
17	3 16	mpbird	|- ( M e. ( 0 ... N ) -> ( ! ` M ) || ( ! ` N ) )