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