Metamath Proof Explorer

Theorem prmgapprmo

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prmgapprmo 
|- 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 eqid 
 |-  ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) = ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) )
3 fzfid 
 |-  ( j e. NN -> ( 1 ... j ) e. Fin )
4 eqidd 
 |-  ( ( j e. NN /\ k e. ( 1 ... j ) ) -> ( m e. NN |-> if ( m e. Prime , m , 1 ) ) = ( m e. NN |-> if ( m e. Prime , m , 1 ) ) )
5 eleq1 
 |-  ( m = k -> ( m e. Prime <-> k e. Prime ) )
6 id 
 |-  ( m = k -> m = k )
7 5 6 ifbieq1d 
 |-  ( m = k -> if ( m e. Prime , m , 1 ) = if ( k e. Prime , k , 1 ) )
8 7 adantl 
 |-  ( ( ( j e. NN /\ k e. ( 1 ... j ) ) /\ m = k ) -> if ( m e. Prime , m , 1 ) = if ( k e. Prime , k , 1 ) )
9 elfznn 
 |-  ( k e. ( 1 ... j ) -> k e. NN )
10 9 adantl 
 |-  ( ( j e. NN /\ k e. ( 1 ... j ) ) -> k e. NN )
11 1nn 
 |-  1 e. NN
12 11 a1i 
 |-  ( k e. ( 1 ... j ) -> 1 e. NN )
13 9 12 ifcld 
 |-  ( k e. ( 1 ... j ) -> if ( k e. Prime , k , 1 ) e. NN )
14 13 adantl 
 |-  ( ( j e. NN /\ k e. ( 1 ... j ) ) -> if ( k e. Prime , k , 1 ) e. NN )
15 4 8 10 14 fvmptd 
 |-  ( ( j e. NN /\ k e. ( 1 ... j ) ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) = if ( k e. Prime , k , 1 ) )
16 15 14 eqeltrd 
 |-  ( ( j e. NN /\ k e. ( 1 ... j ) ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) e. NN )
17 3 16 fprodnncl 
 |-  ( j e. NN -> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) e. NN )
18 2 17 fmpti 
 |-  ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) : NN --> NN
19 nnex 
 |-  NN e. _V
20 19 19 elmap 
 |-  ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) e. ( NN ^m NN ) <-> ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) : NN --> NN )
21 18 20 mpbir 
 |-  ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) e. ( NN ^m NN )
22 21 a1i 
 |-  ( n e. NN -> ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) e. ( NN ^m NN ) )
23 prmgapprmolem 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( #p ` n ) + i ) gcd i ) )
24 eqidd 
 |-  ( ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> ( m e. NN |-> if ( m e. Prime , m , 1 ) ) = ( m e. NN |-> if ( m e. Prime , m , 1 ) ) )
25 7 adantl 
 |-  ( ( ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) /\ k e. ( 1 ... j ) ) /\ m = k ) -> if ( m e. Prime , m , 1 ) = if ( k e. Prime , k , 1 ) )
26 9 adantl 
 |-  ( ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> k e. NN )
27 elfzelz 
 |-  ( k e. ( 1 ... j ) -> k e. ZZ )
28 1zzd 
 |-  ( k e. ( 1 ... j ) -> 1 e. ZZ )
29 27 28 ifcld 
 |-  ( k e. ( 1 ... j ) -> if ( k e. Prime , k , 1 ) e. ZZ )
30 29 adantl 
 |-  ( ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> if ( k e. Prime , k , 1 ) e. ZZ )
31 24 25 26 30 fvmptd 
 |-  ( ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) = if ( k e. Prime , k , 1 ) )
32 31 prodeq2dv 
 |-  ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j e. NN ) -> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) = prod_ k e. ( 1 ... j ) if ( k e. Prime , k , 1 ) )
33 32 mpteq2dva 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) = ( j e. NN |-> prod_ k e. ( 1 ... j ) if ( k e. Prime , k , 1 ) ) )
34 oveq2 
 |-  ( j = n -> ( 1 ... j ) = ( 1 ... n ) )
35 34 prodeq1d 
 |-  ( j = n -> prod_ k e. ( 1 ... j ) if ( k e. Prime , k , 1 ) = prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
36 35 adantl 
 |-  ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ j = n ) -> prod_ k e. ( 1 ... j ) if ( k e. Prime , k , 1 ) = prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
37 simpl 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> n e. NN )
38 fzfid 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( 1 ... n ) e. Fin )
39 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
40 11 a1i 
 |-  ( k e. ( 1 ... n ) -> 1 e. NN )
41 39 40 ifcld 
 |-  ( k e. ( 1 ... n ) -> if ( k e. Prime , k , 1 ) e. NN )
42 41 adantl 
 |-  ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ k e. ( 1 ... n ) ) -> if ( k e. Prime , k , 1 ) e. NN )
43 38 42 fprodnncl 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) e. NN )
44 33 36 37 43 fvmptd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) = prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
45 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
46 prmoval 
 |-  ( n e. NN0 -> ( #p ` n ) = prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
47 45 46 syl 
 |-  ( n e. NN -> ( #p ` n ) = prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
48 47 eqcomd 
 |-  ( n e. NN -> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) = ( #p ` n ) )
49 48 adantr 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) = ( #p ` n ) )
50 44 49 eqtrd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) = ( #p ` n ) )
51 50 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) + i ) = ( ( #p ` n ) + i ) )
52 51 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) + i ) gcd i ) = ( ( ( #p ` n ) + i ) gcd i ) )
53 23 52 breqtrrd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) + i ) gcd i ) )
54 53 ralrimiva 
 |-  ( n e. NN -> A. i e. ( 2 ... n ) 1 < ( ( ( ( j e. NN |-> prod_ k e. ( 1 ... j ) ( ( m e. NN |-> if ( m e. Prime , m , 1 ) ) ` k ) ) ` n ) + i ) gcd i ) )
55 1 22 54 prmgaplem8 
 |-  ( n e. NN -> E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
56 55 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 )