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		gcdcom	$⊢ (z \in ℤ \land z - F (N) \in ℤ) \to z \gcd (z - F (N)) = (z - F (N)) \gcd z$
98	94 96 97	syl2anc	$⊢ ((φ \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$
99	93 98	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$
100	99	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)$
101		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)$
102		eluz2	$⊢ z \in ℤ_{\geq (F (N) + 2)} \leftrightarrow (F (N) + 2 \in ℤ \land z \in ℤ \land F (N) + 2 \leq z)$
103		nnre	$⊢ F (N) \in ℕ \to F (N) \in ℝ$
104	103	ad2antll	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to F (N) \in ℝ$
105		2rp	$⊢ 2 \in ℝ^{+}$
106	105	a1i	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 2 \in ℝ^{+}$
107	104 106	ltaddrpd	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to F (N) < F (N) + 2$
108		2re	$⊢ 2 \in ℝ$
109	108	a1i	$⊢ F (N) \in ℕ \to 2 \in ℝ$
110	103 109	readdcld	$⊢ F (N) \in ℕ \to F (N) + 2 \in ℝ$
111	110	ad2antll	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to F (N) + 2 \in ℝ$
112		zre	$⊢ z \in ℤ \to z \in ℝ$
113	112	adantr	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to z \in ℝ$
114		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)$
115	104 111 113 114	syl3anc	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to ((F (N) < F (N) + 2 \land F (N) + 2 \leq z) \to F (N) < z)$
116	107 115	mpand	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to (F (N) + 2 \leq z \to F (N) < z)$
117	116	impancom	$⊢ (z \in ℤ \land F (N) + 2 \leq z) \to ((φ \land F (N) \in ℕ) \to F (N) < z)$
118	117	3adant1	$⊢ (F (N) + 2 \in ℤ \land z \in ℤ \land F (N) + 2 \leq z) \to ((φ \land F (N) \in ℕ) \to F (N) < z)$
119	102 118	sylbi	$⊢ z \in ℤ_{\geq (F (N) + 2)} \to ((φ \land F (N) \in ℕ) \to F (N) < z)$
120	119	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)$
121	101 120	sylbi	$⊢ z \in (F (N) + 2 ..^F (N) + N + 1) \to ((φ \land F (N) \in ℕ) \to F (N) < z)$
122	121	impcom	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to F (N) < z$
123	103	adantl	$⊢ (φ \land F (N) \in ℕ) \to F (N) \in ℝ$
124	89	zred	$⊢ z \in (F (N) + 2 ..^F (N) + N + 1) \to z \in ℝ$
125		posdif	$⊢ (F (N) \in ℝ \land z \in ℝ) \to (F (N) < z \leftrightarrow 0 < z - F (N))$
126	123 124 125	syl2an	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to (F (N) < z \leftrightarrow 0 < z - F (N))$
127	122 126	mpbid	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to 0 < z - F (N)$
128		elnnz	$⊢ z - F (N) \in ℕ \leftrightarrow (z - F (N) \in ℤ \land 0 < z - F (N))$
129	96 127 128	sylanbrc	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to z - F (N) \in ℕ$
130	108	a1i	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 2 \in ℝ$
131		nngt0	$⊢ F (N) \in ℕ \to 0 < F (N)$
132	131	ad2antll	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 0 < F (N)$
133		2pos	$⊢ 0 < 2$
134	133	a1i	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 0 < 2$
135	104 130 132 134	addgt0d	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 0 < F (N) + 2$
136		0red	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to 0 \in ℝ$
137		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)$
138	136 111 113 137	syl3anc	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to ((0 < F (N) + 2 \land F (N) + 2 \leq z) \to 0 < z)$
139	135 138	mpand	$⊢ (z \in ℤ \land (φ \land F (N) \in ℕ)) \to (F (N) + 2 \leq z \to 0 < z)$
140	139	impancom	$⊢ (z \in ℤ \land F (N) + 2 \leq z) \to ((φ \land F (N) \in ℕ) \to 0 < z)$
141	140	3adant1	$⊢ (F (N) + 2 \in ℤ \land z \in ℤ \land F (N) + 2 \leq z) \to ((φ \land F (N) \in ℕ) \to 0 < z)$
142	102 141	sylbi	$⊢ z \in ℤ_{\geq (F (N) + 2)} \to ((φ \land F (N) \in ℕ) \to 0 < z)$
143	142	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)$
144	101 143	sylbi	$⊢ z \in (F (N) + 2 ..^F (N) + N + 1) \to ((φ \land F (N) \in ℕ) \to 0 < z)$
145	144	impcom	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to 0 < z$
146		elnnz	$⊢ z \in ℕ \leftrightarrow (z \in ℤ \land 0 < z)$
147	94 145 146	sylanbrc	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to z \in ℕ$
148	131	adantl	$⊢ (φ \land F (N) \in ℕ) \to 0 < F (N)$
149	148	adantr	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to 0 < F (N)$
150		ltsubpos	$⊢ (F (N) \in ℝ \land z \in ℝ) \to (0 < F (N) \leftrightarrow z - F (N) < z)$
151	123 124 150	syl2an	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to (0 < F (N) \leftrightarrow z - F (N) < z)$
152	149 151	mpbid	$⊢ ((φ \land F (N) \in ℕ) \land z \in (F (N) + 2 ..^F (N) + N + 1)) \to z - F (N) < z$
153		ncoprmlnprm	$⊢ (z - F (N) \in ℕ \land z \in ℕ \land z - F (N) < z) \to (1 < (z - F (N)) \gcd z \to z \notin ℙ)$
154	129 147 152 153	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 ℙ)$
155	100 154	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 ℙ)$
156	87 155	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 ℙ)$
157	156	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 ℙ))$
158	157	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 ℙ))$
159	76 158	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 ℙ))$
160	51 159	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 ℙ))$
161	160	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 ℙ)))$
162	3 161	mpid	$⊢ φ \to (F (N) \in ℕ \to (z \in (F (N) + 2 ..^F (N) + N + 1) \to z \notin ℙ))$
163	162	imp	$⊢ (φ \land F (N) \in ℕ) \to (z \in (F (N) + 2 ..^F (N) + N + 1) \to z \notin ℙ)$
164	163	ad2antrr	$⊢ (((φ \land F (N) \in ℕ) \land p \in ℙ) \land q \in ℙ) \to (z \in (F (N) + 2 ..^F (N) + N + 1) \to z \notin ℙ)$
165	164	impcom	$⊢ (z \in (F (N) + 2 ..^F (N) + N + 1) \land (((φ \land F (N) \in ℕ) \land p \in ℙ) \land q \in ℙ)) \to z \notin ℙ$
166	165	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 ℙ)$
167	166	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 ℙ))$
168		neleq1	$⊢ s = z \to (s \notin ℙ \leftrightarrow z \notin ℙ)$
169	168	rspcv	$⊢ z \in (F (N) + N + 1 ..^q) \to (\forall s \in (F (N) + N + 1 ..^q) s \notin ℙ \to z \notin ℙ)$
170	169	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 ℙ)$
171	170	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 ℙ)$
172	171	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 ℙ))$
173	167 172	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 ℙ))$
174	173	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 ℙ))$
175	48 174	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 ℙ))$
176	41 175	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 ℙ))$
177	176	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 ℙ))$
178	36 177	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 ℙ))$
179	178	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 ℙ))$
180	179	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 ℙ$
181	180	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 ℙ$
182	26 27 181	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 ℙ)$
183	182	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 ℙ))$
184	183	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 ℙ))$
185	184	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 ℙ))$
186	25 185	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 ℙ))$
187	19 24 186	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 ℙ)$
188	6 187	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