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