Metamath Proof Explorer

Theorem prmgaplem7

Description: Lemma for prmgap . (Contributed by AV, 12-Aug-2020) (Proof shortened by AV, 10-Jul-2022)

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 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 ) )

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 elmapi 
 |-  ( F e. ( NN ^m NN ) -> F : NN --> NN )
5 2 4 syl 
 |-  ( ph -> F : NN --> NN )
6 5 1 ffvelcdmd 
 |-  ( ph -> ( F ` N ) e. NN )
7 simpr 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) e. NN )
8 elnnuz 
 |-  ( ( F ` N ) e. NN <-> ( F ` N ) e. ( ZZ>= ` 1 ) )
9 7 8 sylib 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) e. ( ZZ>= ` 1 ) )
10 2z 
 |-  2 e. ZZ
11 10 eluzaddi 
 |-  ( ( F ` N ) e. ( ZZ>= ` 1 ) -> ( ( F ` N ) + 2 ) e. ( ZZ>= ` ( 1 + 2 ) ) )
12 9 11 syl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + 2 ) e. ( ZZ>= ` ( 1 + 2 ) ) )
13 1p2e3 
 |-  ( 1 + 2 ) = 3
14 13 eqcomi 
 |-  3 = ( 1 + 2 )
15 14 fveq2i 
 |-  ( ZZ>= ` 3 ) = ( ZZ>= ` ( 1 + 2 ) )
16 12 15 eleqtrrdi 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + 2 ) e. ( ZZ>= ` 3 ) )
17 prmgaplem5 
 |-  ( ( ( F ` N ) + 2 ) e. ( ZZ>= ` 3 ) -> E. p e. Prime ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) )
18 16 17 syl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> E. p e. Prime ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) )
19 1 anim1ci 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) e. NN /\ N e. NN ) )
20 nnaddcl 
 |-  ( ( ( F ` N ) e. NN /\ N e. NN ) -> ( ( F ` N ) + N ) e. NN )
21 19 20 syl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + N ) e. NN )
22 prmgaplem6 
 |-  ( ( ( F ` N ) + N ) e. NN -> E. q e. Prime ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) )
23 21 22 syl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> E. q e. Prime ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) )
24 reeanv 
 |-  ( E. p e. Prime E. q e. Prime ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) <-> ( E. p e. Prime ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ E. q e. Prime ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) )
25 simprll 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) ) -> p < ( ( F ` N ) + 2 ) )
26 simprrl 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) ) -> ( ( F ` N ) + N ) < q )
27 nnz 
 |-  ( ( F ` N ) e. NN -> ( F ` N ) e. ZZ )
28 27 adantl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) e. ZZ )
29 10 a1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> 2 e. ZZ )
30 28 29 zaddcld 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + 2 ) e. ZZ )
31 30 ad2antrr 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( F ` N ) + 2 ) e. ZZ )
32 31 anim1ci 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ z e. ( ( p + 1 ) ..^ q ) ) -> ( z e. ( ( p + 1 ) ..^ q ) /\ ( ( F ` N ) + 2 ) e. ZZ ) )
33 fzospliti 
 |-  ( ( z e. ( ( p + 1 ) ..^ q ) /\ ( ( F ` N ) + 2 ) e. ZZ ) -> ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) \/ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) )
34 32 33 syl 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ z e. ( ( p + 1 ) ..^ q ) ) -> ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) \/ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) )
35 34 ex 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( z e. ( ( p + 1 ) ..^ q ) -> ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) \/ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) ) )
36 neleq1 
 |-  ( r = z -> ( r e/ Prime <-> z e/ Prime ) )
37 36 rspcv 
 |-  ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) -> ( A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime -> z e/ Prime ) )
38 37 adantld 
 |-  ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) -> ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) -> z e/ Prime ) )
39 38 adantrd 
 |-  ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) )
40 39 a1d 
 |-  ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
41 21 nnzd 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + N ) e. ZZ )
42 41 peano2zd 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( ( F ` N ) + N ) + 1 ) e. ZZ )
43 42 ad2antrr 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( F ` N ) + N ) + 1 ) e. ZZ )
44 43 anim1ci 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ q ) /\ ( ( ( F ` N ) + N ) + 1 ) e. ZZ ) )
45 fzospliti 
 |-  ( ( z e. ( ( ( F ` N ) + 2 ) ..^ q ) /\ ( ( ( F ` N ) + N ) + 1 ) e. ZZ ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) \/ z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) ) )
46 44 45 syl 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) \/ z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) ) )
47 46 ex 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ q ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) \/ z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) ) ) )
48 1 nnzd 
 |-  ( ph -> N e. ZZ )
49 fzshftral 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ ( F ` N ) e. ZZ ) -> ( A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) <-> A. j e. ( ( 2 + ( F ` N ) ) ... ( N + ( F ` N ) ) ) [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) ) )
50 10 48 27 49 mp3an3an 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) <-> A. j e. ( ( 2 + ( F ` N ) ) ... ( N + ( F ` N ) ) ) [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) ) )
51 2cnd 
 |-  ( ph -> 2 e. CC )
52 nncn 
 |-  ( ( F ` N ) e. NN -> ( F ` N ) e. CC )
53 addcom 
 |-  ( ( 2 e. CC /\ ( F ` N ) e. CC ) -> ( 2 + ( F ` N ) ) = ( ( F ` N ) + 2 ) )
54 51 52 53 syl2an 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( 2 + ( F ` N ) ) = ( ( F ` N ) + 2 ) )
55 1 nncnd 
 |-  ( ph -> N e. CC )
56 addcom 
 |-  ( ( N e. CC /\ ( F ` N ) e. CC ) -> ( N + ( F ` N ) ) = ( ( F ` N ) + N ) )
57 55 52 56 syl2an 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( N + ( F ` N ) ) = ( ( F ` N ) + N ) )
58 54 57 oveq12d 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( 2 + ( F ` N ) ) ... ( N + ( F ` N ) ) ) = ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) )
59 ovex 
 |-  ( j - ( F ` N ) ) e. _V
60 sbcbr2g 
 |-  ( ( j - ( F ` N ) ) e. _V -> ( [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) <-> 1 < [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) ) )
61 59 60 mp1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) <-> 1 < [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) ) )
62 csbov12g 
 |-  ( ( j - ( F ` N ) ) e. _V -> [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) = ( [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) gcd [_ ( j - ( F ` N ) ) / i ]_ i ) )
63 59 62 mp1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) = ( [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) gcd [_ ( j - ( F ` N ) ) / i ]_ i ) )
64 csbov2g 
 |-  ( ( j - ( F ` N ) ) e. _V -> [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) = ( ( F ` N ) + [_ ( j - ( F ` N ) ) / i ]_ i ) )
65 59 64 mp1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) = ( ( F ` N ) + [_ ( j - ( F ` N ) ) / i ]_ i ) )
66 csbvarg 
 |-  ( ( j - ( F ` N ) ) e. _V -> [_ ( j - ( F ` N ) ) / i ]_ i = ( j - ( F ` N ) ) )
67 66 oveq2d 
 |-  ( ( j - ( F ` N ) ) e. _V -> ( ( F ` N ) + [_ ( j - ( F ` N ) ) / i ]_ i ) = ( ( F ` N ) + ( j - ( F ` N ) ) ) )
68 59 67 mp1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( F ` N ) + [_ ( j - ( F ` N ) ) / i ]_ i ) = ( ( F ` N ) + ( j - ( F ` N ) ) ) )
69 65 68 eqtrd 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) = ( ( F ` N ) + ( j - ( F ` N ) ) ) )
70 59 66 mp1i 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> [_ ( j - ( F ` N ) ) / i ]_ i = ( j - ( F ` N ) ) )
71 69 70 oveq12d 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( [_ ( j - ( F ` N ) ) / i ]_ ( ( F ` N ) + i ) gcd [_ ( j - ( F ` N ) ) / i ]_ i ) = ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) )
72 63 71 eqtrd 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) = ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) )
73 72 breq2d 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( 1 < [_ ( j - ( F ` N ) ) / i ]_ ( ( ( F ` N ) + i ) gcd i ) <-> 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) ) )
74 61 73 bitrd 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) <-> 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) ) )
75 58 74 raleqbidv 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( A. j e. ( ( 2 + ( F ` N ) ) ... ( N + ( F ` N ) ) ) [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) <-> A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) ) )
76 fzval3 
 |-  ( ( ( F ` N ) + N ) e. ZZ -> ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) = ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) )
77 76 eqcomd 
 |-  ( ( ( F ` N ) + N ) e. ZZ -> ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) = ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) )
78 41 77 syl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) = ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) )
79 78 eleq2d 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) <-> z e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) ) )
80 79 biimpa 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> z e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) )
81 oveq1 
 |-  ( j = z -> ( j - ( F ` N ) ) = ( z - ( F ` N ) ) )
82 81 oveq2d 
 |-  ( j = z -> ( ( F ` N ) + ( j - ( F ` N ) ) ) = ( ( F ` N ) + ( z - ( F ` N ) ) ) )
83 82 81 oveq12d 
 |-  ( j = z -> ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) = ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) )
84 83 breq2d 
 |-  ( j = z -> ( 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) <-> 1 < ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) ) )
85 84 rspcv 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) -> ( A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) -> 1 < ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) ) )
86 80 85 syl 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) -> 1 < ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) ) )
87 52 adantl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) e. CC )
88 elfzoelz 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e. ZZ )
89 88 zcnd 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e. CC )
90 pncan3 
 |-  ( ( ( F ` N ) e. CC /\ z e. CC ) -> ( ( F ` N ) + ( z - ( F ` N ) ) ) = z )
91 87 89 90 syl2an 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( ( F ` N ) + ( z - ( F ` N ) ) ) = z )
92 91 oveq1d 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) = ( z gcd ( z - ( F ` N ) ) ) )
93 88 adantl 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> z e. ZZ )
94 zsubcl 
 |-  ( ( z e. ZZ /\ ( F ` N ) e. ZZ ) -> ( z - ( F ` N ) ) e. ZZ )
95 88 28 94 syl2anr 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( z - ( F ` N ) ) e. ZZ )
96 93 95 gcdcomd 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( z gcd ( z - ( F ` N ) ) ) = ( ( z - ( F ` N ) ) gcd z ) )
97 92 96 eqtrd 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) = ( ( z - ( F ` N ) ) gcd z ) )
98 97 breq2d 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( 1 < ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) <-> 1 < ( ( z - ( F ` N ) ) gcd z ) ) )
99 elfzo2 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) <-> ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) /\ ( ( ( F ` N ) + N ) + 1 ) e. ZZ /\ z < ( ( ( F ` N ) + N ) + 1 ) ) )
100 eluz2 
 |-  ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) <-> ( ( ( F ` N ) + 2 ) e. ZZ /\ z e. ZZ /\ ( ( F ` N ) + 2 ) <_ z ) )
101 nnre 
 |-  ( ( F ` N ) e. NN -> ( F ` N ) e. RR )
102 101 ad2antll 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( F ` N ) e. RR )
103 2rp 
 |-  2 e. RR+
104 103 a1i 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 2 e. RR+ )
105 102 104 ltaddrpd 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( F ` N ) < ( ( F ` N ) + 2 ) )
106 2re 
 |-  2 e. RR
107 106 a1i 
 |-  ( ( F ` N ) e. NN -> 2 e. RR )
108 101 107 readdcld 
 |-  ( ( F ` N ) e. NN -> ( ( F ` N ) + 2 ) e. RR )
109 108 ad2antll 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( ( F ` N ) + 2 ) e. RR )
110 zre 
 |-  ( z e. ZZ -> z e. RR )
111 110 adantr 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> z e. RR )
112 ltletr 
 |-  ( ( ( F ` N ) e. RR /\ ( ( F ` N ) + 2 ) e. RR /\ z e. RR ) -> ( ( ( F ` N ) < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + 2 ) <_ z ) -> ( F ` N ) < z ) )
113 102 109 111 112 syl3anc 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( ( ( F ` N ) < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + 2 ) <_ z ) -> ( F ` N ) < z ) )
114 105 113 mpand 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( ( ( F ` N ) + 2 ) <_ z -> ( F ` N ) < z ) )
115 114 impancom 
 |-  ( ( z e. ZZ /\ ( ( F ` N ) + 2 ) <_ z ) -> ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) < z ) )
116 115 3adant1 
 |-  ( ( ( ( F ` N ) + 2 ) e. ZZ /\ z e. ZZ /\ ( ( F ` N ) + 2 ) <_ z ) -> ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) < z ) )
117 100 116 sylbi 
 |-  ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) < z ) )
118 117 3ad2ant1 
 |-  ( ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) /\ ( ( ( F ` N ) + N ) + 1 ) e. ZZ /\ z < ( ( ( F ` N ) + N ) + 1 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) < z ) )
119 99 118 sylbi 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) < z ) )
120 119 impcom 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( F ` N ) < z )
121 101 adantl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( F ` N ) e. RR )
122 88 zred 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e. RR )
123 posdif 
 |-  ( ( ( F ` N ) e. RR /\ z e. RR ) -> ( ( F ` N ) < z <-> 0 < ( z - ( F ` N ) ) ) )
124 121 122 123 syl2an 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( ( F ` N ) < z <-> 0 < ( z - ( F ` N ) ) ) )
125 120 124 mpbid 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> 0 < ( z - ( F ` N ) ) )
126 elnnz 
 |-  ( ( z - ( F ` N ) ) e. NN <-> ( ( z - ( F ` N ) ) e. ZZ /\ 0 < ( z - ( F ` N ) ) ) )
127 95 125 126 sylanbrc 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( z - ( F ` N ) ) e. NN )
128 106 a1i 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 2 e. RR )
129 nngt0 
 |-  ( ( F ` N ) e. NN -> 0 < ( F ` N ) )
130 129 ad2antll 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 0 < ( F ` N ) )
131 2pos 
 |-  0 < 2
132 131 a1i 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 0 < 2 )
133 102 128 130 132 addgt0d 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 0 < ( ( F ` N ) + 2 ) )
134 0red 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> 0 e. RR )
135 ltletr 
 |-  ( ( 0 e. RR /\ ( ( F ` N ) + 2 ) e. RR /\ z e. RR ) -> ( ( 0 < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + 2 ) <_ z ) -> 0 < z ) )
136 134 109 111 135 syl3anc 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( ( 0 < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + 2 ) <_ z ) -> 0 < z ) )
137 133 136 mpand 
 |-  ( ( z e. ZZ /\ ( ph /\ ( F ` N ) e. NN ) ) -> ( ( ( F ` N ) + 2 ) <_ z -> 0 < z ) )
138 137 impancom 
 |-  ( ( z e. ZZ /\ ( ( F ` N ) + 2 ) <_ z ) -> ( ( ph /\ ( F ` N ) e. NN ) -> 0 < z ) )
139 138 3adant1 
 |-  ( ( ( ( F ` N ) + 2 ) e. ZZ /\ z e. ZZ /\ ( ( F ` N ) + 2 ) <_ z ) -> ( ( ph /\ ( F ` N ) e. NN ) -> 0 < z ) )
140 100 139 sylbi 
 |-  ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> 0 < z ) )
141 140 3ad2ant1 
 |-  ( ( z e. ( ZZ>= ` ( ( F ` N ) + 2 ) ) /\ ( ( ( F ` N ) + N ) + 1 ) e. ZZ /\ z < ( ( ( F ` N ) + N ) + 1 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> 0 < z ) )
142 99 141 sylbi 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> ( ( ph /\ ( F ` N ) e. NN ) -> 0 < z ) )
143 142 impcom 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> 0 < z )
144 elnnz 
 |-  ( z e. NN <-> ( z e. ZZ /\ 0 < z ) )
145 93 143 144 sylanbrc 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> z e. NN )
146 129 adantl 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> 0 < ( F ` N ) )
147 146 adantr 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> 0 < ( F ` N ) )
148 ltsubpos 
 |-  ( ( ( F ` N ) e. RR /\ z e. RR ) -> ( 0 < ( F ` N ) <-> ( z - ( F ` N ) ) < z ) )
149 121 122 148 syl2an 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( 0 < ( F ` N ) <-> ( z - ( F ` N ) ) < z ) )
150 147 149 mpbid 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( z - ( F ` N ) ) < z )
151 ncoprmlnprm 
 |-  ( ( ( z - ( F ` N ) ) e. NN /\ z e. NN /\ ( z - ( F ` N ) ) < z ) -> ( 1 < ( ( z - ( F ` N ) ) gcd z ) -> z e/ Prime ) )
152 127 145 150 151 syl3anc 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( 1 < ( ( z - ( F ` N ) ) gcd z ) -> z e/ Prime ) )
153 98 152 sylbid 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( 1 < ( ( ( F ` N ) + ( z - ( F ` N ) ) ) gcd ( z - ( F ` N ) ) ) -> z e/ Prime ) )
154 86 153 syld 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) ) -> ( A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) -> z e/ Prime ) )
155 154 ex 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> ( A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) -> z e/ Prime ) ) )
156 155 com23 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( A. j e. ( ( ( F ` N ) + 2 ) ... ( ( F ` N ) + N ) ) 1 < ( ( ( F ` N ) + ( j - ( F ` N ) ) ) gcd ( j - ( F ` N ) ) ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) ) )
157 75 156 sylbid 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( A. j e. ( ( 2 + ( F ` N ) ) ... ( N + ( F ` N ) ) ) [. ( j - ( F ` N ) ) / i ]. 1 < ( ( ( F ` N ) + i ) gcd i ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) ) )
158 50 157 sylbid 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) ) )
159 158 ex 
 |-  ( ph -> ( ( F ` N ) e. NN -> ( A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) ) ) )
160 3 159 mpid 
 |-  ( ph -> ( ( F ` N ) e. NN -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) ) )
161 160 imp 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) )
162 161 ad2antrr 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> z e/ Prime ) )
163 162 impcom 
 |-  ( ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) /\ ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) ) -> z e/ Prime )
164 163 a1d 
 |-  ( ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) /\ ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) )
165 164 ex 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
166 neleq1 
 |-  ( s = z -> ( s e/ Prime <-> z e/ Prime ) )
167 166 rspcv 
 |-  ( z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) -> ( A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime -> z e/ Prime ) )
168 167 adantld 
 |-  ( z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) -> ( ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) -> z e/ Prime ) )
169 168 adantld 
 |-  ( z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) )
170 169 a1d 
 |-  ( z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
171 165 170 jaoi 
 |-  ( ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) \/ z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
172 171 com12 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( z e. ( ( ( F ` N ) + 2 ) ..^ ( ( ( F ` N ) + N ) + 1 ) ) \/ z e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
173 47 172 syldc 
 |-  ( z e. ( ( ( F ` N ) + 2 ) ..^ q ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
174 40 173 jaoi 
 |-  ( ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) \/ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) -> ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
175 174 com12 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( z e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) \/ z e. ( ( ( F ` N ) + 2 ) ..^ q ) ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
176 35 175 syld 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( z e. ( ( p + 1 ) ..^ q ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> z e/ Prime ) ) )
177 176 com23 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> ( z e. ( ( p + 1 ) ..^ q ) -> z e/ Prime ) ) )
178 177 imp31 
 |-  ( ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) ) /\ z e. ( ( p + 1 ) ..^ q ) ) -> z e/ Prime )
179 178 ralrimiva 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) ) -> A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime )
180 25 26 179 3jca 
 |-  ( ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) /\ ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) ) -> ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) )
181 180 ex 
 |-  ( ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) ) )
182 181 reximdva 
 |-  ( ( ( ph /\ ( F ` N ) e. NN ) /\ p e. Prime ) -> ( E. q e. Prime ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> E. q e. Prime ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 ) ..^ q ) z e/ Prime ) ) )
183 182 reximdva 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( E. p e. Prime E. q e. Prime ( ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> 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 ) ) )
184 24 183 biimtrrid 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> ( ( E. p e. Prime ( p < ( ( F ` N ) + 2 ) /\ A. r e. ( ( p + 1 ) ..^ ( ( F ` N ) + 2 ) ) r e/ Prime ) /\ E. q e. Prime ( ( ( F ` N ) + N ) < q /\ A. s e. ( ( ( ( F ` N ) + N ) + 1 ) ..^ q ) s e/ Prime ) ) -> 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 ) ) )
185 18 23 184 mp2and 
 |-  ( ( ph /\ ( F ` N ) e. NN ) -> 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 ) )
186 6 185 mpdan 
 |-  ( 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 ) )