Metamath Proof Explorer

Theorem prmgaplem3

Description: Lemma for prmgap . (Contributed by AV, 9-Aug-2020)

Ref Expression
Hypothesis prmgaplem3.a 
|- A = { p e. Prime | p < N }
Assertion prmgaplem3 
|- ( N e. ( ZZ>= ` 3 ) -> E. x e. A A. y e. A y <_ x )

Proof

Step Hyp Ref Expression
1 prmgaplem3.a 
 |-  A = { p e. Prime | p < N }
2 ssrab2 
 |-  { p e. Prime | p < N } C_ Prime
3 2 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> { p e. Prime | p < N } C_ Prime )
4 prmssnn 
 |-  Prime C_ NN
5 nnssre 
 |-  NN C_ RR
6 4 5 sstri 
 |-  Prime C_ RR
7 3 6 sstrdi 
 |-  ( N e. ( ZZ>= ` 3 ) -> { p e. Prime | p < N } C_ RR )
8 fzofi 
 |-  ( 0 ..^ N ) e. Fin
9 breq1 
 |-  ( p = i -> ( p < N <-> i < N ) )
10 9 elrab 
 |-  ( i e. { p e. Prime | p < N } <-> ( i e. Prime /\ i < N ) )
11 prmnn 
 |-  ( i e. Prime -> i e. NN )
12 11 nnnn0d 
 |-  ( i e. Prime -> i e. NN0 )
13 12 ad2antrl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( i e. Prime /\ i < N ) ) -> i e. NN0 )
14 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
15 14 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( i e. Prime /\ i < N ) ) -> N e. NN )
16 simprr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( i e. Prime /\ i < N ) ) -> i < N )
17 elfzo0 
 |-  ( i e. ( 0 ..^ N ) <-> ( i e. NN0 /\ N e. NN /\ i < N ) )
18 13 15 16 17 syl3anbrc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( i e. Prime /\ i < N ) ) -> i e. ( 0 ..^ N ) )
19 18 ex 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( i e. Prime /\ i < N ) -> i e. ( 0 ..^ N ) ) )
20 10 19 syl5bi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( i e. { p e. Prime | p < N } -> i e. ( 0 ..^ N ) ) )
21 20 ssrdv 
 |-  ( N e. ( ZZ>= ` 3 ) -> { p e. Prime | p < N } C_ ( 0 ..^ N ) )
22 ssfi 
 |-  ( ( ( 0 ..^ N ) e. Fin /\ { p e. Prime | p < N } C_ ( 0 ..^ N ) ) -> { p e. Prime | p < N } e. Fin )
23 8 21 22 sylancr 
 |-  ( N e. ( ZZ>= ` 3 ) -> { p e. Prime | p < N } e. Fin )
24 breq1 
 |-  ( p = 2 -> ( p < N <-> 2 < N ) )
25 2prm 
 |-  2 e. Prime
26 25 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. Prime )
27 eluz2 
 |-  ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
28 df-3 
 |-  3 = ( 2 + 1 )
29 28 breq1i 
 |-  ( 3 <_ N <-> ( 2 + 1 ) <_ N )
30 2z 
 |-  2 e. ZZ
31 zltp1le 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 < N <-> ( 2 + 1 ) <_ N ) )
32 30 31 mpan 
 |-  ( N e. ZZ -> ( 2 < N <-> ( 2 + 1 ) <_ N ) )
33 32 biimprd 
 |-  ( N e. ZZ -> ( ( 2 + 1 ) <_ N -> 2 < N ) )
34 29 33 syl5bi 
 |-  ( N e. ZZ -> ( 3 <_ N -> 2 < N ) )
35 34 imp 
 |-  ( ( N e. ZZ /\ 3 <_ N ) -> 2 < N )
36 35 3adant1 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> 2 < N )
37 27 36 sylbi 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 < N )
38 24 26 37 elrabd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. { p e. Prime | p < N } )
39 38 ne0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { p e. Prime | p < N } =/= (/) )
40 sseq1 
 |-  ( A = { p e. Prime | p < N } -> ( A C_ RR <-> { p e. Prime | p < N } C_ RR ) )
41 eleq1 
 |-  ( A = { p e. Prime | p < N } -> ( A e. Fin <-> { p e. Prime | p < N } e. Fin ) )
42 neeq1 
 |-  ( A = { p e. Prime | p < N } -> ( A =/= (/) <-> { p e. Prime | p < N } =/= (/) ) )
43 40 41 42 3anbi123d 
 |-  ( A = { p e. Prime | p < N } -> ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) <-> ( { p e. Prime | p < N } C_ RR /\ { p e. Prime | p < N } e. Fin /\ { p e. Prime | p < N } =/= (/) ) ) )
44 1 43 ax-mp 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) <-> ( { p e. Prime | p < N } C_ RR /\ { p e. Prime | p < N } e. Fin /\ { p e. Prime | p < N } =/= (/) ) )
45 7 23 39 44 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( A C_ RR /\ A e. Fin /\ A =/= (/) ) )
46 fimaxre 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )
47 45 46 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. A A. y e. A y <_ x )