Metamath Proof Explorer

Theorem prmgaplem5

Description: Lemma for prmgap : for each integer greater than 2 there is a smaller prime closest to this integer, i.e. there is a smaller prime and no other prime is between this prime and the integer. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion prmgaplem5 
|- ( N e. ( ZZ>= ` 3 ) -> E. p e. Prime ( p < N /\ A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime ) )

Proof

Step Hyp Ref Expression
1 elrabi 
 |-  ( r e. { q e. Prime | q < N } -> r e. Prime )
2 1 ad2antlr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) -> r e. Prime )
3 breq1 
 |-  ( p = r -> ( p < N <-> r < N ) )
4 oveq1 
 |-  ( p = r -> ( p + 1 ) = ( r + 1 ) )
5 4 oveq1d 
 |-  ( p = r -> ( ( p + 1 ) ..^ N ) = ( ( r + 1 ) ..^ N ) )
6 5 raleqdv 
 |-  ( p = r -> ( A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime <-> A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime ) )
7 3 6 anbi12d 
 |-  ( p = r -> ( ( p < N /\ A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime ) <-> ( r < N /\ A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime ) ) )
8 7 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) /\ p = r ) -> ( ( p < N /\ A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime ) <-> ( r < N /\ A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime ) ) )
9 breq1 
 |-  ( q = r -> ( q < N <-> r < N ) )
10 9 elrab 
 |-  ( r e. { q e. Prime | q < N } <-> ( r e. Prime /\ r < N ) )
11 10 simprbi 
 |-  ( r e. { q e. Prime | q < N } -> r < N )
12 11 ad2antlr 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) -> r < N )
13 elfzo2 
 |-  ( z e. ( ( r + 1 ) ..^ N ) <-> ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) )
14 breq1 
 |-  ( q = z -> ( q < N <-> z < N ) )
15 simpl 
 |-  ( ( z e. Prime /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> z e. Prime )
16 simpr3 
 |-  ( ( z e. Prime /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> z < N )
17 14 15 16 elrabd 
 |-  ( ( z e. Prime /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> z e. { q e. Prime | q < N } )
18 17 adantrl 
 |-  ( ( z e. Prime /\ ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) ) -> z e. { q e. Prime | q < N } )
19 eluz2 
 |-  ( z e. ( ZZ>= ` ( r + 1 ) ) <-> ( ( r + 1 ) e. ZZ /\ z e. ZZ /\ ( r + 1 ) <_ z ) )
20 prmz 
 |-  ( r e. Prime -> r e. ZZ )
21 zltp1le 
 |-  ( ( r e. ZZ /\ z e. ZZ ) -> ( r < z <-> ( r + 1 ) <_ z ) )
22 20 21 sylan 
 |-  ( ( r e. Prime /\ z e. ZZ ) -> ( r < z <-> ( r + 1 ) <_ z ) )
23 prmnn 
 |-  ( r e. Prime -> r e. NN )
24 23 nnred 
 |-  ( r e. Prime -> r e. RR )
25 zre 
 |-  ( z e. ZZ -> z e. RR )
26 ltnle 
 |-  ( ( r e. RR /\ z e. RR ) -> ( r < z <-> -. z <_ r ) )
27 26 biimpd 
 |-  ( ( r e. RR /\ z e. RR ) -> ( r < z -> -. z <_ r ) )
28 24 25 27 syl2an 
 |-  ( ( r e. Prime /\ z e. ZZ ) -> ( r < z -> -. z <_ r ) )
29 pm2.21 
 |-  ( -. z <_ r -> ( z <_ r -> z e/ Prime ) )
30 28 29 syl6 
 |-  ( ( r e. Prime /\ z e. ZZ ) -> ( r < z -> ( z <_ r -> z e/ Prime ) ) )
31 22 30 sylbird 
 |-  ( ( r e. Prime /\ z e. ZZ ) -> ( ( r + 1 ) <_ z -> ( z <_ r -> z e/ Prime ) ) )
32 31 expcom 
 |-  ( z e. ZZ -> ( r e. Prime -> ( ( r + 1 ) <_ z -> ( z <_ r -> z e/ Prime ) ) ) )
33 32 com23 
 |-  ( z e. ZZ -> ( ( r + 1 ) <_ z -> ( r e. Prime -> ( z <_ r -> z e/ Prime ) ) ) )
34 33 a1i 
 |-  ( ( r + 1 ) e. ZZ -> ( z e. ZZ -> ( ( r + 1 ) <_ z -> ( r e. Prime -> ( z <_ r -> z e/ Prime ) ) ) ) )
35 34 3imp 
 |-  ( ( ( r + 1 ) e. ZZ /\ z e. ZZ /\ ( r + 1 ) <_ z ) -> ( r e. Prime -> ( z <_ r -> z e/ Prime ) ) )
36 19 35 sylbi 
 |-  ( z e. ( ZZ>= ` ( r + 1 ) ) -> ( r e. Prime -> ( z <_ r -> z e/ Prime ) ) )
37 36 3ad2ant1 
 |-  ( ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) -> ( r e. Prime -> ( z <_ r -> z e/ Prime ) ) )
38 1 37 syl5com 
 |-  ( r e. { q e. Prime | q < N } -> ( ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) -> ( z <_ r -> z e/ Prime ) ) )
39 38 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) -> ( ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) -> ( z <_ r -> z e/ Prime ) ) )
40 39 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> ( z <_ r -> z e/ Prime ) )
41 40 adantl 
 |-  ( ( z e. Prime /\ ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) ) -> ( z <_ r -> z e/ Prime ) )
42 18 41 embantd 
 |-  ( ( z e. Prime /\ ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> z e/ Prime ) )
43 42 ex 
 |-  ( z e. Prime -> ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> z e/ Prime ) ) )
44 df-nel 
 |-  ( z e/ Prime <-> -. z e. Prime )
45 2a1 
 |-  ( z e/ Prime -> ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> z e/ Prime ) ) )
46 44 45 sylbir 
 |-  ( -. z e. Prime -> ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> z e/ Prime ) ) )
47 43 46 pm2.61i 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> z e/ Prime ) )
48 47 impancom 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. { q e. Prime | q < N } -> z <_ r ) ) -> ( ( z e. ( ZZ>= ` ( r + 1 ) ) /\ N e. ZZ /\ z < N ) -> z e/ Prime ) )
49 13 48 biimtrid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ ( z e. { q e. Prime | q < N } -> z <_ r ) ) -> ( z e. ( ( r + 1 ) ..^ N ) -> z e/ Prime ) )
50 49 ex 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) -> ( ( z e. { q e. Prime | q < N } -> z <_ r ) -> ( z e. ( ( r + 1 ) ..^ N ) -> z e/ Prime ) ) )
51 50 ralimdv2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) -> ( A. z e. { q e. Prime | q < N } z <_ r -> A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime ) )
52 51 imp 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) -> A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime )
53 12 52 jca 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) -> ( r < N /\ A. z e. ( ( r + 1 ) ..^ N ) z e/ Prime ) )
54 2 8 53 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ r e. { q e. Prime | q < N } ) /\ A. z e. { q e. Prime | q < N } z <_ r ) -> E. p e. Prime ( p < N /\ A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime ) )
55 eqid 
 |-  { q e. Prime | q < N } = { q e. Prime | q < N }
56 55 prmgaplem3 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. r e. { q e. Prime | q < N } A. z e. { q e. Prime | q < N } z <_ r )
57 54 56 r19.29a 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. p e. Prime ( p < N /\ A. z e. ( ( p + 1 ) ..^ N ) z e/ Prime ) )