This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )