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

Metamath Proof Explorer

Theorem prmgaplem7

Proof