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