Metamath Proof Explorer

Theorem prmgaplcm

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at the least common multiple of all positive integers less than or equal to n. (Contributed by AV, 13-Aug-2020) (Revised by AV, 27-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prmgaplcm 
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( n e. NN -> n e. NN )
2 fzssz 
 |-  ( 1 ... x ) C_ ZZ
3 2 a1i 
 |-  ( x e. NN -> ( 1 ... x ) C_ ZZ )
4 fzfi 
 |-  ( 1 ... x ) e. Fin
5 4 a1i 
 |-  ( x e. NN -> ( 1 ... x ) e. Fin )
6 0nelfz1 
 |-  0 e/ ( 1 ... x )
7 6 a1i 
 |-  ( x e. NN -> 0 e/ ( 1 ... x ) )
8 lcmfn0cl 
 |-  ( ( ( 1 ... x ) C_ ZZ /\ ( 1 ... x ) e. Fin /\ 0 e/ ( 1 ... x ) ) -> ( _lcm ` ( 1 ... x ) ) e. NN )
9 3 5 7 8 syl3anc 
 |-  ( x e. NN -> ( _lcm ` ( 1 ... x ) ) e. NN )
10 9 adantl 
 |-  ( ( n e. NN /\ x e. NN ) -> ( _lcm ` ( 1 ... x ) ) e. NN )
11 eqid 
 |-  ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) = ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) )
12 10 11 fmptd 
 |-  ( n e. NN -> ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) : NN --> NN )
13 nnex 
 |-  NN e. _V
14 13 13 pm3.2i 
 |-  ( NN e. _V /\ NN e. _V )
15 elmapg 
 |-  ( ( NN e. _V /\ NN e. _V ) -> ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) e. ( NN ^m NN ) <-> ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) : NN --> NN ) )
16 14 15 mp1i 
 |-  ( n e. NN -> ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) e. ( NN ^m NN ) <-> ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) : NN --> NN ) )
17 12 16 mpbird 
 |-  ( n e. NN -> ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) e. ( NN ^m NN ) )
18 prmgaplcmlem2 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( _lcm ` ( 1 ... n ) ) + i ) gcd i ) )
19 eqidd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) = ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) )
20 oveq2 
 |-  ( x = n -> ( 1 ... x ) = ( 1 ... n ) )
21 20 fveq2d 
 |-  ( x = n -> ( _lcm ` ( 1 ... x ) ) = ( _lcm ` ( 1 ... n ) ) )
22 21 adantl 
 |-  ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ x = n ) -> ( _lcm ` ( 1 ... x ) ) = ( _lcm ` ( 1 ... n ) ) )
23 simpl 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> n e. NN )
24 fzssz 
 |-  ( 1 ... n ) C_ ZZ
25 fzfi 
 |-  ( 1 ... n ) e. Fin
26 24 25 pm3.2i 
 |-  ( ( 1 ... n ) C_ ZZ /\ ( 1 ... n ) e. Fin )
27 lcmfcl 
 |-  ( ( ( 1 ... n ) C_ ZZ /\ ( 1 ... n ) e. Fin ) -> ( _lcm ` ( 1 ... n ) ) e. NN0 )
28 26 27 mp1i 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( _lcm ` ( 1 ... n ) ) e. NN0 )
29 19 22 23 28 fvmptd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) ` n ) = ( _lcm ` ( 1 ... n ) ) )
30 29 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) ` n ) + i ) = ( ( _lcm ` ( 1 ... n ) ) + i ) )
31 30 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) ` n ) + i ) gcd i ) = ( ( ( _lcm ` ( 1 ... n ) ) + i ) gcd i ) )
32 18 31 breqtrrd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) ` n ) + i ) gcd i ) )
33 32 ralrimiva 
 |-  ( n e. NN -> A. i e. ( 2 ... n ) 1 < ( ( ( ( x e. NN |-> ( _lcm ` ( 1 ... x ) ) ) ` n ) + i ) gcd i ) )
34 1 17 33 prmgaplem8 
 |-  ( n e. NN -> E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
35 34 rgen 
 |-  A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime )