Theorem lcmflefac

Description: The least common multiple of all positive integers less than or equal to an integer is less than or equal to the factorial of the integer. (Contributed by AV, 16-Aug-2020) (Revised by AV, 27-Aug-2020)

	Ref	Expression
Assertion	lcmflefac	|- ( N e. NN -> ( _lcm ` ( 1 ... N ) ) <_ ( ! ` N ) )

Proof

Step	Hyp	Ref	Expression
1		fzssz	|- ( 1 ... N ) C_ ZZ
2	1	a1i	|- ( N e. NN -> ( 1 ... N ) C_ ZZ )
3		fzfid	|- ( N e. NN -> ( 1 ... N ) e. Fin )
4		0nelfz1	|- 0 e/ ( 1 ... N )
5	4	a1i	|- ( N e. NN -> 0 e/ ( 1 ... N ) )
6	2 3 5	3jca	|- ( N e. NN -> ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin /\ 0 e/ ( 1 ... N ) ) )
7		nnnn0	|- ( N e. NN -> N e. NN0 )
8	7	faccld	|- ( N e. NN -> ( ! ` N ) e. NN )
9		elfznn	|- ( m e. ( 1 ... N ) -> m e. NN )
10		elfzuz3	|- ( m e. ( 1 ... N ) -> N e. ( ZZ>= ` m ) )
11	10	adantl	|- ( ( N e. NN /\ m e. ( 1 ... N ) ) -> N e. ( ZZ>= ` m ) )
12		dvdsfac	|- ( ( m e. NN /\ N e. ( ZZ>= ` m ) ) -> m || ( ! ` N ) )
13	9 11 12	syl2an2	|- ( ( N e. NN /\ m e. ( 1 ... N ) ) -> m || ( ! ` N ) )
14	13	ralrimiva	|- ( N e. NN -> A. m e. ( 1 ... N ) m || ( ! ` N ) )
15	8 14	jca	|- ( N e. NN -> ( ( ! ` N ) e. NN /\ A. m e. ( 1 ... N ) m || ( ! ` N ) ) )
16		lcmfledvds	|- ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin /\ 0 e/ ( 1 ... N ) ) -> ( ( ( ! ` N ) e. NN /\ A. m e. ( 1 ... N ) m || ( ! ` N ) ) -> ( _lcm ` ( 1 ... N ) ) <_ ( ! ` N ) ) )
17	6 15 16	sylc	|- ( N e. NN -> ( _lcm ` ( 1 ... N ) ) <_ ( ! ` N ) )