Metamath Proof Explorer

Theorem prmgaplem4

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

Ref Expression
Hypothesis prmgaplem4.a 
|- A = { p e. Prime | ( N < p /\ p <_ P ) }
Assertion prmgaplem4 
|- ( ( N e. NN /\ P e. Prime /\ N < P ) -> E. x e. A A. y e. A x <_ y )

Proof

Step Hyp Ref Expression
1 prmgaplem4.a 
 |-  A = { p e. Prime | ( N < p /\ p <_ P ) }
2 ssrab2 
 |-  { p e. Prime | ( N < p /\ p <_ P ) } C_ Prime
3 2 a1i 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> { p e. Prime | ( N < p /\ p <_ P ) } 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. NN /\ P e. Prime /\ N < P ) -> { p e. Prime | ( N < p /\ p <_ P ) } C_ RR )
8 fzfid 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( N ... P ) e. Fin )
9 breq2 
 |-  ( p = i -> ( N < p <-> N < i ) )
10 breq1 
 |-  ( p = i -> ( p <_ P <-> i <_ P ) )
11 9 10 anbi12d 
 |-  ( p = i -> ( ( N < p /\ p <_ P ) <-> ( N < i /\ i <_ P ) ) )
12 11 elrab 
 |-  ( i e. { p e. Prime | ( N < p /\ p <_ P ) } <-> ( i e. Prime /\ ( N < i /\ i <_ P ) ) )
13 nnz 
 |-  ( N e. NN -> N e. ZZ )
14 prmz 
 |-  ( P e. Prime -> P e. ZZ )
15 13 14 anim12i 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( N e. ZZ /\ P e. ZZ ) )
16 15 3adant3 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( N e. ZZ /\ P e. ZZ ) )
17 prmz 
 |-  ( i e. Prime -> i e. ZZ )
18 17 adantr 
 |-  ( ( i e. Prime /\ ( N < i /\ i <_ P ) ) -> i e. ZZ )
19 16 18 anim12i 
 |-  ( ( ( N e. NN /\ P e. Prime /\ N < P ) /\ ( i e. Prime /\ ( N < i /\ i <_ P ) ) ) -> ( ( N e. ZZ /\ P e. ZZ ) /\ i e. ZZ ) )
20 df-3an 
 |-  ( ( N e. ZZ /\ P e. ZZ /\ i e. ZZ ) <-> ( ( N e. ZZ /\ P e. ZZ ) /\ i e. ZZ ) )
21 19 20 sylibr 
 |-  ( ( ( N e. NN /\ P e. Prime /\ N < P ) /\ ( i e. Prime /\ ( N < i /\ i <_ P ) ) ) -> ( N e. ZZ /\ P e. ZZ /\ i e. ZZ ) )
22 nnre 
 |-  ( N e. NN -> N e. RR )
23 22 adantr 
 |-  ( ( N e. NN /\ P e. Prime ) -> N e. RR )
24 6 sseli 
 |-  ( i e. Prime -> i e. RR )
25 ltle 
 |-  ( ( N e. RR /\ i e. RR ) -> ( N < i -> N <_ i ) )
26 23 24 25 syl2an 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ i e. Prime ) -> ( N < i -> N <_ i ) )
27 26 anim1d 
 |-  ( ( ( N e. NN /\ P e. Prime ) /\ i e. Prime ) -> ( ( N < i /\ i <_ P ) -> ( N <_ i /\ i <_ P ) ) )
28 27 ex 
 |-  ( ( N e. NN /\ P e. Prime ) -> ( i e. Prime -> ( ( N < i /\ i <_ P ) -> ( N <_ i /\ i <_ P ) ) ) )
29 28 3adant3 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( i e. Prime -> ( ( N < i /\ i <_ P ) -> ( N <_ i /\ i <_ P ) ) ) )
30 29 imp32 
 |-  ( ( ( N e. NN /\ P e. Prime /\ N < P ) /\ ( i e. Prime /\ ( N < i /\ i <_ P ) ) ) -> ( N <_ i /\ i <_ P ) )
31 elfz2 
 |-  ( i e. ( N ... P ) <-> ( ( N e. ZZ /\ P e. ZZ /\ i e. ZZ ) /\ ( N <_ i /\ i <_ P ) ) )
32 21 30 31 sylanbrc 
 |-  ( ( ( N e. NN /\ P e. Prime /\ N < P ) /\ ( i e. Prime /\ ( N < i /\ i <_ P ) ) ) -> i e. ( N ... P ) )
33 32 ex 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( ( i e. Prime /\ ( N < i /\ i <_ P ) ) -> i e. ( N ... P ) ) )
34 12 33 biimtrid 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( i e. { p e. Prime | ( N < p /\ p <_ P ) } -> i e. ( N ... P ) ) )
35 34 ssrdv 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> { p e. Prime | ( N < p /\ p <_ P ) } C_ ( N ... P ) )
36 8 35 ssfid 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> { p e. Prime | ( N < p /\ p <_ P ) } e. Fin )
37 breq2 
 |-  ( p = P -> ( N < p <-> N < P ) )
38 breq1 
 |-  ( p = P -> ( p <_ P <-> P <_ P ) )
39 37 38 anbi12d 
 |-  ( p = P -> ( ( N < p /\ p <_ P ) <-> ( N < P /\ P <_ P ) ) )
40 simp2 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> P e. Prime )
41 prmnn 
 |-  ( P e. Prime -> P e. NN )
42 41 nnred 
 |-  ( P e. Prime -> P e. RR )
43 42 leidd 
 |-  ( P e. Prime -> P <_ P )
44 43 anim1ci 
 |-  ( ( P e. Prime /\ N < P ) -> ( N < P /\ P <_ P ) )
45 44 3adant1 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( N < P /\ P <_ P ) )
46 39 40 45 elrabd 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> P e. { p e. Prime | ( N < p /\ p <_ P ) } )
47 46 ne0d 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> { p e. Prime | ( N < p /\ p <_ P ) } =/= (/) )
48 sseq1 
 |-  ( A = { p e. Prime | ( N < p /\ p <_ P ) } -> ( A C_ RR <-> { p e. Prime | ( N < p /\ p <_ P ) } C_ RR ) )
49 eleq1 
 |-  ( A = { p e. Prime | ( N < p /\ p <_ P ) } -> ( A e. Fin <-> { p e. Prime | ( N < p /\ p <_ P ) } e. Fin ) )
50 neeq1 
 |-  ( A = { p e. Prime | ( N < p /\ p <_ P ) } -> ( A =/= (/) <-> { p e. Prime | ( N < p /\ p <_ P ) } =/= (/) ) )
51 48 49 50 3anbi123d 
 |-  ( A = { p e. Prime | ( N < p /\ p <_ P ) } -> ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) <-> ( { p e. Prime | ( N < p /\ p <_ P ) } C_ RR /\ { p e. Prime | ( N < p /\ p <_ P ) } e. Fin /\ { p e. Prime | ( N < p /\ p <_ P ) } =/= (/) ) ) )
52 1 51 ax-mp 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) <-> ( { p e. Prime | ( N < p /\ p <_ P ) } C_ RR /\ { p e. Prime | ( N < p /\ p <_ P ) } e. Fin /\ { p e. Prime | ( N < p /\ p <_ P ) } =/= (/) ) )
53 7 36 47 52 syl3anbrc 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> ( A C_ RR /\ A e. Fin /\ A =/= (/) ) )
54 fiminre 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )
55 53 54 syl 
 |-  ( ( N e. NN /\ P e. Prime /\ N < P ) -> E. x e. A A. y e. A x <_ y )