Metamath Proof Explorer

Theorem prmgaplcmlem1

Description: Lemma for prmgaplcm : The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 14-Aug-2020) (Revised by AV, 27-Aug-2020)

Ref Expression
Assertion prmgaplcmlem1 
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( _lcm ` ( 1 ... N ) ) + I ) )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( I e. ( 2 ... N ) -> I e. ZZ )
2 1 adantl 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. ZZ )
3 fzssz 
 |-  ( 1 ... N ) C_ ZZ
4 fzfi 
 |-  ( 1 ... N ) e. Fin
5 3 4 pm3.2i 
 |-  ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin )
6 lcmfcl 
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. NN0 )
7 6 nn0zd 
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. ZZ )
8 5 7 mp1i 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( _lcm ` ( 1 ... N ) ) e. ZZ )
9 breq1 
 |-  ( x = I -> ( x || ( _lcm ` ( 1 ... N ) ) <-> I || ( _lcm ` ( 1 ... N ) ) ) )
10 dvdslcmf 
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) -> A. x e. ( 1 ... N ) x || ( _lcm ` ( 1 ... N ) ) )
11 5 10 mp1i 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> A. x e. ( 1 ... N ) x || ( _lcm ` ( 1 ... N ) ) )
12 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
13 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... N ) C_ ( 1 ... N ) )
14 12 13 mp1i 
 |-  ( N e. NN -> ( 2 ... N ) C_ ( 1 ... N ) )
15 14 sselda 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. ( 1 ... N ) )
16 9 11 15 rspcdva 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( _lcm ` ( 1 ... N ) ) )
17 iddvds 
 |-  ( I e. ZZ -> I || I )
18 1 17 syl 
 |-  ( I e. ( 2 ... N ) -> I || I )
19 18 adantl 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || I )
20 2 8 2 16 19 dvds2addd 
 |-  ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( _lcm ` ( 1 ... N ) ) + I ) )