Metamath Proof Explorer

Theorem prmgaplem6

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

Ref Expression
Assertion prmgaplem6 
|- ( N e. NN -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) )

Proof

Step Hyp Ref Expression
1 prmunb 
 |-  ( N e. NN -> E. n e. Prime N < n )
2 eqid 
 |-  { q e. Prime | ( N < q /\ q <_ n ) } = { q e. Prime | ( N < q /\ q <_ n ) }
3 2 prmgaplem4 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> E. p e. { q e. Prime | ( N < q /\ q <_ n ) } A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z )
4 breq2 
 |-  ( q = p -> ( N < q <-> N < p ) )
5 breq1 
 |-  ( q = p -> ( q <_ n <-> p <_ n ) )
6 4 5 anbi12d 
 |-  ( q = p -> ( ( N < q /\ q <_ n ) <-> ( N < p /\ p <_ n ) ) )
7 6 elrab 
 |-  ( p e. { q e. Prime | ( N < q /\ q <_ n ) } <-> ( p e. Prime /\ ( N < p /\ p <_ n ) ) )
8 simplrl 
 |-  ( ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) /\ A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z ) -> p e. Prime )
9 simprrl 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> N < p )
10 9 adantr 
 |-  ( ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) /\ A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z ) -> N < p )
11 breq2 
 |-  ( q = z -> ( N < q <-> N < z ) )
12 breq1 
 |-  ( q = z -> ( q <_ n <-> z <_ n ) )
13 11 12 anbi12d 
 |-  ( q = z -> ( ( N < q /\ q <_ n ) <-> ( N < z /\ z <_ n ) ) )
14 simpll 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z e. ( ( N + 1 ) ..^ p ) ) -> z e. Prime )
15 elfzo2 
 |-  ( z e. ( ( N + 1 ) ..^ p ) <-> ( z e. ( ZZ>= ` ( N + 1 ) ) /\ p e. ZZ /\ z < p ) )
16 eluz2 
 |-  ( z e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ z e. ZZ /\ ( N + 1 ) <_ z ) )
17 nnz 
 |-  ( N e. NN -> N e. ZZ )
18 prmz 
 |-  ( z e. Prime -> z e. ZZ )
19 zltp1le 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( N < z <-> ( N + 1 ) <_ z ) )
20 17 18 19 syl2an 
 |-  ( ( N e. NN /\ z e. Prime ) -> ( N < z <-> ( N + 1 ) <_ z ) )
21 20 exbiri 
 |-  ( N e. NN -> ( z e. Prime -> ( ( N + 1 ) <_ z -> N < z ) ) )
22 21 3ad2ant1 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( z e. Prime -> ( ( N + 1 ) <_ z -> N < z ) ) )
23 22 adantr 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( z e. Prime -> ( ( N + 1 ) <_ z -> N < z ) ) )
24 23 impcom 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( ( N + 1 ) <_ z -> N < z ) )
25 24 com12 
 |-  ( ( N + 1 ) <_ z -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> N < z ) )
26 25 adantr 
 |-  ( ( ( N + 1 ) <_ z /\ p e. ZZ ) -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> N < z ) )
27 26 adantr 
 |-  ( ( ( ( N + 1 ) <_ z /\ p e. ZZ ) /\ z < p ) -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> N < z ) )
28 27 imp 
 |-  ( ( ( ( ( N + 1 ) <_ z /\ p e. ZZ ) /\ z < p ) /\ ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) ) -> N < z )
29 prmnn 
 |-  ( z e. Prime -> z e. NN )
30 29 nnred 
 |-  ( z e. Prime -> z e. RR )
31 30 ad2antrl 
 |-  ( ( n e. Prime /\ ( z e. Prime /\ p e. Prime ) ) -> z e. RR )
32 prmnn 
 |-  ( p e. Prime -> p e. NN )
33 32 nnred 
 |-  ( p e. Prime -> p e. RR )
34 33 adantl 
 |-  ( ( z e. Prime /\ p e. Prime ) -> p e. RR )
35 34 adantl 
 |-  ( ( n e. Prime /\ ( z e. Prime /\ p e. Prime ) ) -> p e. RR )
36 prmnn 
 |-  ( n e. Prime -> n e. NN )
37 36 nnred 
 |-  ( n e. Prime -> n e. RR )
38 37 adantr 
 |-  ( ( n e. Prime /\ ( z e. Prime /\ p e. Prime ) ) -> n e. RR )
39 ltleletr 
 |-  ( ( z e. RR /\ p e. RR /\ n e. RR ) -> ( ( z < p /\ p <_ n ) -> z <_ n ) )
40 31 35 38 39 syl3anc 
 |-  ( ( n e. Prime /\ ( z e. Prime /\ p e. Prime ) ) -> ( ( z < p /\ p <_ n ) -> z <_ n ) )
41 40 exp4b 
 |-  ( n e. Prime -> ( ( z e. Prime /\ p e. Prime ) -> ( z < p -> ( p <_ n -> z <_ n ) ) ) )
42 41 3ad2ant2 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( ( z e. Prime /\ p e. Prime ) -> ( z < p -> ( p <_ n -> z <_ n ) ) ) )
43 42 expdcom 
 |-  ( z e. Prime -> ( p e. Prime -> ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( z < p -> ( p <_ n -> z <_ n ) ) ) ) )
44 43 com45 
 |-  ( z e. Prime -> ( p e. Prime -> ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( p <_ n -> ( z < p -> z <_ n ) ) ) ) )
45 44 com14 
 |-  ( p <_ n -> ( p e. Prime -> ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( z e. Prime -> ( z < p -> z <_ n ) ) ) ) )
46 45 adantl 
 |-  ( ( N < p /\ p <_ n ) -> ( p e. Prime -> ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( z e. Prime -> ( z < p -> z <_ n ) ) ) ) )
47 46 impcom 
 |-  ( ( p e. Prime /\ ( N < p /\ p <_ n ) ) -> ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( z e. Prime -> ( z < p -> z <_ n ) ) ) )
48 47 impcom 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( z e. Prime -> ( z < p -> z <_ n ) ) )
49 48 impcom 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( z < p -> z <_ n ) )
50 49 adantld 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( ( ( ( N + 1 ) <_ z /\ p e. ZZ ) /\ z < p ) -> z <_ n ) )
51 50 impcom 
 |-  ( ( ( ( ( N + 1 ) <_ z /\ p e. ZZ ) /\ z < p ) /\ ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) ) -> z <_ n )
52 28 51 jca 
 |-  ( ( ( ( ( N + 1 ) <_ z /\ p e. ZZ ) /\ z < p ) /\ ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) ) -> ( N < z /\ z <_ n ) )
53 52 exp41 
 |-  ( ( N + 1 ) <_ z -> ( p e. ZZ -> ( z < p -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( N < z /\ z <_ n ) ) ) ) )
54 53 3ad2ant3 
 |-  ( ( ( N + 1 ) e. ZZ /\ z e. ZZ /\ ( N + 1 ) <_ z ) -> ( p e. ZZ -> ( z < p -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( N < z /\ z <_ n ) ) ) ) )
55 16 54 sylbi 
 |-  ( z e. ( ZZ>= ` ( N + 1 ) ) -> ( p e. ZZ -> ( z < p -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( N < z /\ z <_ n ) ) ) ) )
56 55 3imp 
 |-  ( ( z e. ( ZZ>= ` ( N + 1 ) ) /\ p e. ZZ /\ z < p ) -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( N < z /\ z <_ n ) ) )
57 15 56 sylbi 
 |-  ( z e. ( ( N + 1 ) ..^ p ) -> ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( N < z /\ z <_ n ) ) )
58 57 impcom 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z e. ( ( N + 1 ) ..^ p ) ) -> ( N < z /\ z <_ n ) )
59 13 14 58 elrabd 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z e. ( ( N + 1 ) ..^ p ) ) -> z e. { q e. Prime | ( N < q /\ q <_ n ) } )
60 elfzolt2 
 |-  ( z e. ( ( N + 1 ) ..^ p ) -> z < p )
61 33 ad2antrl 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> p e. RR )
62 ltnle 
 |-  ( ( z e. RR /\ p e. RR ) -> ( z < p <-> -. p <_ z ) )
63 62 biimpd 
 |-  ( ( z e. RR /\ p e. RR ) -> ( z < p -> -. p <_ z ) )
64 30 61 63 syl2an 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( z < p -> -. p <_ z ) )
65 64 imp 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z < p ) -> -. p <_ z )
66 65 pm2.21d 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z < p ) -> ( p <_ z -> z e/ Prime ) )
67 60 66 sylan2 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z e. ( ( N + 1 ) ..^ p ) ) -> ( p <_ z -> z e/ Prime ) )
68 59 67 embantd 
 |-  ( ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) /\ z e. ( ( N + 1 ) ..^ p ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> z e/ Prime ) )
69 68 ex 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( z e. ( ( N + 1 ) ..^ p ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> z e/ Prime ) ) )
70 69 com23 
 |-  ( ( z e. Prime /\ ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) )
71 70 ex 
 |-  ( z e. Prime -> ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) ) )
72 df-nel 
 |-  ( z e/ Prime <-> -. z e. Prime )
73 2a1 
 |-  ( z e/ Prime -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) )
74 73 a1d 
 |-  ( z e/ Prime -> ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) ) )
75 72 74 sylbir 
 |-  ( -. z e. Prime -> ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) ) )
76 71 75 pm2.61i 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( ( z e. { q e. Prime | ( N < q /\ q <_ n ) } -> p <_ z ) -> ( z e. ( ( N + 1 ) ..^ p ) -> z e/ Prime ) ) )
77 76 ralimdv2 
 |-  ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) -> ( A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z -> A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) )
78 77 imp 
 |-  ( ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) /\ A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z ) -> A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime )
79 8 10 78 jca32 
 |-  ( ( ( ( N e. NN /\ n e. Prime /\ N < n ) /\ ( p e. Prime /\ ( N < p /\ p <_ n ) ) ) /\ A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z ) -> ( p e. Prime /\ ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) )
80 79 exp31 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( ( p e. Prime /\ ( N < p /\ p <_ n ) ) -> ( A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z -> ( p e. Prime /\ ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) ) ) )
81 7 80 syl5bi 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( p e. { q e. Prime | ( N < q /\ q <_ n ) } -> ( A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z -> ( p e. Prime /\ ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) ) ) )
82 81 impd 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( ( p e. { q e. Prime | ( N < q /\ q <_ n ) } /\ A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z ) -> ( p e. Prime /\ ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) ) )
83 82 reximdv2 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> ( E. p e. { q e. Prime | ( N < q /\ q <_ n ) } A. z e. { q e. Prime | ( N < q /\ q <_ n ) } p <_ z -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) )
84 3 83 mpd 
 |-  ( ( N e. NN /\ n e. Prime /\ N < n ) -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) )
85 84 rexlimdv3a 
 |-  ( N e. NN -> ( E. n e. Prime N < n -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) ) )
86 1 85 mpd 
 |-  ( N e. NN -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 ) ..^ p ) z e/ Prime ) )