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