prmgaplem7

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

	Ref	Expression
Hypotheses	prmgaplem7.n	$⊢ φ \to N \in ℕ$
	prmgaplem7.f	$⊢ φ \to F \in (ℕ^{ℕ})$
	prmgaplem7.i	$⊢ φ \to \forall i \in (2 \dots N) 1 < (F (N) + i) \gcd i$
Assertion	prmgaplem7	$⊢ φ \to \exists p \in ℙ \exists q \in ℙ (p < F (N) + 2 \land F (N) + N < q \land \forall z \in (p + 1 ..^q) z \notin ℙ)$

Proof

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

Metamath Proof Explorer

Theorem prmgaplem7

Proof