Metamath Proof Explorer

Theorem prmgap

Description: The prime gap theorem: for each positive integer there are (at least) two successive primes with a difference ("gap") at least as big as the given integer. (Contributed by AV, 13-Aug-2020)

Ref Expression
Assertion prmgap 
|- 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 facmapnn 
 |-  ( x e. NN |-> ( ! ` x ) ) e. ( NN ^m NN )
3 2 a1i 
 |-  ( n e. NN -> ( x e. NN |-> ( ! ` x ) ) e. ( NN ^m NN ) )
4 prmgaplem2 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( ! ` n ) + i ) gcd i ) )
5 eqidd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( x e. NN |-> ( ! ` x ) ) = ( x e. NN |-> ( ! ` x ) ) )
6 fveq2 
 |-  ( x = n -> ( ! ` x ) = ( ! ` n ) )
7 6 adantl 
 |-  ( ( ( n e. NN /\ i e. ( 2 ... n ) ) /\ x = n ) -> ( ! ` x ) = ( ! ` n ) )
8 simpl 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> n e. NN )
9 fvexd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ! ` n ) e. _V )
10 5 7 8 9 fvmptd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( x e. NN |-> ( ! ` x ) ) ` n ) = ( ! ` n ) )
11 10 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( x e. NN |-> ( ! ` x ) ) ` n ) + i ) = ( ( ! ` n ) + i ) )
12 11 oveq1d 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> ( ( ( ( x e. NN |-> ( ! ` x ) ) ` n ) + i ) gcd i ) = ( ( ( ! ` n ) + i ) gcd i ) )
13 4 12 breqtrrd 
 |-  ( ( n e. NN /\ i e. ( 2 ... n ) ) -> 1 < ( ( ( ( x e. NN |-> ( ! ` x ) ) ` n ) + i ) gcd i ) )
14 13 ralrimiva 
 |-  ( n e. NN -> A. i e. ( 2 ... n ) 1 < ( ( ( ( x e. NN |-> ( ! ` x ) ) ` n ) + i ) gcd i ) )
15 1 3 14 prmgaplem8 
 |-  ( n e. NN -> E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
16 15 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 )