Metamath Proof Explorer

Theorem prmgaplem8

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

Ref Expression
Hypotheses prmgaplem7.n 
|- ( ph -> N e. NN )
prmgaplem7.f 
|- ( ph -> F e. ( NN ^m NN ) )
prmgaplem7.i 
|- ( ph -> A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) )
Assertion prmgaplem8 
|- ( ph -> 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 prmgaplem7.n 
 |-  ( ph -> N e. NN )
2 prmgaplem7.f 
 |-  ( ph -> F e. ( NN ^m NN ) )
3 prmgaplem7.i 
 |-  ( ph -> A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) )
4 prmnn 
 |-  ( q e. Prime -> q e. NN )
5 4 nnred 
 |-  ( q e. Prime -> q e. RR )
6 5 ad2antll 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> q e. RR )
7 prmnn 
 |-  ( p e. Prime -> p e. NN )
8 7 nnred 
 |-  ( p e. Prime -> p e. RR )
9 8 ad2antlr 
 |-  ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> p e. RR )
10 9 adantl 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> p e. RR )
11 1 nnred 
 |-  ( ph -> N e. RR )
12 11 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> N e. RR )
13 12 adantl 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> N e. RR )
14 elmapi 
 |-  ( F e. ( NN ^m NN ) -> F : NN --> NN )
15 ffvelcdm 
 |-  ( ( F : NN --> NN /\ N e. NN ) -> ( F ` N ) e. NN )
16 15 ex 
 |-  ( F : NN --> NN -> ( N e. NN -> ( F ` N ) e. NN ) )
17 2 14 16 3syl 
 |-  ( ph -> ( N e. NN -> ( F ` N ) e. NN ) )
18 1 17 mpd 
 |-  ( ph -> ( F ` N ) e. NN )
19 18 nnred 
 |-  ( ph -> ( F ` N ) e. RR )
20 19 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> ( F ` N ) e. RR )
21 20 adantl 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> ( F ` N ) e. RR )
22 1red 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> 1 e. RR )
23 21 22 readdcld 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> ( ( F ` N ) + 1 ) e. RR )
24 18 nncnd 
 |-  ( ph -> ( F ` N ) e. CC )
25 1cnd 
 |-  ( ph -> 1 e. CC )
26 1 nncnd 
 |-  ( ph -> N e. CC )
27 24 25 26 add32d 
 |-  ( ph -> ( ( ( F ` N ) + 1 ) + N ) = ( ( ( F ` N ) + N ) + 1 ) )
28 27 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( F ` N ) + 1 ) + N ) = ( ( ( F ` N ) + N ) + 1 ) )
29 28 ad2antrr 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( F ` N ) + 1 ) + N ) = ( ( ( F ` N ) + N ) + 1 ) )
30 18 nnzd 
 |-  ( ph -> ( F ` N ) e. ZZ )
31 30 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( F ` N ) e. ZZ )
32 1 nnzd 
 |-  ( ph -> N e. ZZ )
33 32 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. ZZ )
34 31 33 zaddcld 
 |-  ( ( ph /\ p e. Prime ) -> ( ( F ` N ) + N ) e. ZZ )
35 prmz 
 |-  ( q e. Prime -> q e. ZZ )
36 zltp1le 
 |-  ( ( ( ( F ` N ) + N ) e. ZZ /\ q e. ZZ ) -> ( ( ( F ` N ) + N ) < q <-> ( ( ( F ` N ) + N ) + 1 ) <_ q ) )
37 34 35 36 syl2an 
 |-  ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( F ` N ) + N ) < q <-> ( ( ( F ` N ) + N ) + 1 ) <_ q ) )
38 37 biimpa 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( F ` N ) + N ) + 1 ) <_ q )
39 29 38 eqbrtrd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( F ` N ) + 1 ) + N ) <_ q )
40 39 expcom 
 |-  ( ( ( F ` N ) + N ) < q -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( F ` N ) + 1 ) + N ) <_ q ) )
41 40 adantl 
 |-  ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( F ` N ) + 1 ) + N ) <_ q ) )
42 41 imp 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> ( ( ( F ` N ) + 1 ) + N ) <_ q )
43 df-2 
 |-  2 = ( 1 + 1 )
44 43 a1i 
 |-  ( ph -> 2 = ( 1 + 1 ) )
45 44 oveq2d 
 |-  ( ph -> ( ( F ` N ) + 2 ) = ( ( F ` N ) + ( 1 + 1 ) ) )
46 24 25 25 addassd 
 |-  ( ph -> ( ( ( F ` N ) + 1 ) + 1 ) = ( ( F ` N ) + ( 1 + 1 ) ) )
47 45 46 eqtr4d 
 |-  ( ph -> ( ( F ` N ) + 2 ) = ( ( ( F ` N ) + 1 ) + 1 ) )
48 47 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( F ` N ) + 2 ) = ( ( ( F ` N ) + 1 ) + 1 ) )
49 48 breq2d 
 |-  ( ( ph /\ p e. Prime ) -> ( p < ( ( F ` N ) + 2 ) <-> p < ( ( ( F ` N ) + 1 ) + 1 ) ) )
50 prmz 
 |-  ( p e. Prime -> p e. ZZ )
51 30 peano2zd 
 |-  ( ph -> ( ( F ` N ) + 1 ) e. ZZ )
52 zleltp1 
 |-  ( ( p e. ZZ /\ ( ( F ` N ) + 1 ) e. ZZ ) -> ( p <_ ( ( F ` N ) + 1 ) <-> p < ( ( ( F ` N ) + 1 ) + 1 ) ) )
53 50 51 52 syl2anr 
 |-  ( ( ph /\ p e. Prime ) -> ( p <_ ( ( F ` N ) + 1 ) <-> p < ( ( ( F ` N ) + 1 ) + 1 ) ) )
54 53 biimprd 
 |-  ( ( ph /\ p e. Prime ) -> ( p < ( ( ( F ` N ) + 1 ) + 1 ) -> p <_ ( ( F ` N ) + 1 ) ) )
55 49 54 sylbid 
 |-  ( ( ph /\ p e. Prime ) -> ( p < ( ( F ` N ) + 2 ) -> p <_ ( ( F ` N ) + 1 ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> ( p < ( ( F ` N ) + 2 ) -> p <_ ( ( F ` N ) + 1 ) ) )
57 56 com12 
 |-  ( p < ( ( F ` N ) + 2 ) -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> p <_ ( ( F ` N ) + 1 ) ) )
58 57 adantr 
 |-  ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> p <_ ( ( F ` N ) + 1 ) ) )
59 58 imp 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> p <_ ( ( F ` N ) + 1 ) )
60 6 10 13 23 42 59 lesub3d 
 |-  ( ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) /\ ( ( ph /\ p e. Prime ) /\ q e. Prime ) ) -> N <_ ( q - p ) )
61 60 ex 
 |-  ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q ) -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> N <_ ( q - p ) ) )
62 61 3adant3 
 |-  ( ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) -> ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) -> N <_ ( q - p ) ) )
63 62 impcom 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) ) -> N <_ ( q - p ) )
64 simpr3 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) ) -> A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime )
65 63 64 jca 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ q e. Prime ) /\ ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) ) -> ( N <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
66 1 2 3 prmgaplem7 
 |-  ( ph -> E. p e. Prime E. q e. Prime ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
67 65 66 reximddv2 
 |-  ( ph -> E. p e. Prime E. q e. Prime ( N <_ ( q - p ) /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )