Theorem prmolelcmf

Description: The primorial of a positive integer is less than or equal to the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020) (Revised by AV, 29-Aug-2020)

	Ref	Expression
Assertion	prmolelcmf	|- ( N e. NN0 -> ( #p ` N ) <_ ( _lcm ` ( 1 ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmocl	|- ( N e. NN0 -> ( #p ` N ) e. NN )
2	1	nnzd	|- ( N e. NN0 -> ( #p ` N ) e. ZZ )
3		fzssz	|- ( 1 ... N ) C_ ZZ
4		fzfid	|- ( N e. NN0 -> ( 1 ... N ) e. Fin )
5		0nelfz1	|- 0 e/ ( 1 ... N )
6	5	a1i	|- ( N e. NN0 -> 0 e/ ( 1 ... N ) )
7		lcmfn0cl	|- ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin /\ 0 e/ ( 1 ... N ) ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
8	3 4 6 7	mp3an2i	|- ( N e. NN0 -> ( _lcm ` ( 1 ... N ) ) e. NN )
9	2 8	jca	|- ( N e. NN0 -> ( ( #p ` N ) e. ZZ /\ ( _lcm ` ( 1 ... N ) ) e. NN ) )
10		prmodvdslcmf	|- ( N e. NN0 -> ( #p ` N ) || ( _lcm ` ( 1 ... N ) ) )
11		dvdsle	|- ( ( ( #p ` N ) e. ZZ /\ ( _lcm ` ( 1 ... N ) ) e. NN ) -> ( ( #p ` N ) || ( _lcm ` ( 1 ... N ) ) -> ( #p ` N ) <_ ( _lcm ` ( 1 ... N ) ) ) )
12	9 10 11	sylc	|- ( N e. NN0 -> ( #p ` N ) <_ ( _lcm ` ( 1 ... N ) ) )