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

Metamath Proof Explorer

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