prmgaplem8

	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	prmgaplem8	$⊢ φ \to \exists p \in ℙ \exists q \in ℙ (N \leq q - p \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		prmnn	$⊢ q \in ℙ \to q \in ℕ$
5	4	nnred	$⊢ q \in ℙ \to q \in ℝ$
6	5	ad2antll	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to q \in ℝ$
7		prmnn	$⊢ p \in ℙ \to p \in ℕ$
8	7	nnred	$⊢ p \in ℙ \to p \in ℝ$
9	8	ad2antlr	$⊢ ((φ \land p \in ℙ) \land q \in ℙ) \to p \in ℝ$
10	9	adantl	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to p \in ℝ$
11	1	nnred	$⊢ φ \to N \in ℝ$
12	11	ad2antrr	$⊢ ((φ \land p \in ℙ) \land q \in ℙ) \to N \in ℝ$
13	12	adantl	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to N \in ℝ$
14		elmapi	$⊢ F \in (ℕ^{ℕ}) \to F : ℕ ⟶ ℕ$
15		ffvelcdm	$⊢ (F : ℕ ⟶ ℕ \land N \in ℕ) \to F (N) \in ℕ$
16	15	ex	$⊢ F : ℕ ⟶ ℕ \to (N \in ℕ \to F (N) \in ℕ)$
17	2 14 16	3syl	$⊢ φ \to (N \in ℕ \to F (N) \in ℕ)$
18	1 17	mpd	$⊢ φ \to F (N) \in ℕ$
19	18	nnred	$⊢ φ \to F (N) \in ℝ$
20	19	ad2antrr	$⊢ ((φ \land p \in ℙ) \land q \in ℙ) \to F (N) \in ℝ$
21	20	adantl	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to F (N) \in ℝ$
22		1red	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to 1 \in ℝ$
23	21 22	readdcld	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to F (N) + 1 \in ℝ$
24	18	nncnd	$⊢ φ \to F (N) \in ℂ$
25		1cnd	$⊢ φ \to 1 \in ℂ$
26	1	nncnd	$⊢ φ \to N \in ℂ$
27	24 25 26	add32d	$⊢ φ \to F (N) + 1 + N = F (N) + N + 1$
28	27	adantr	$⊢ (φ \land p \in ℙ) \to F (N) + 1 + N = F (N) + N + 1$
29	28	ad2antrr	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land F (N) + N < q) \to F (N) + 1 + N = F (N) + N + 1$
30	18	nnzd	$⊢ φ \to F (N) \in ℤ$
31	30	adantr	$⊢ (φ \land p \in ℙ) \to F (N) \in ℤ$
32	1	nnzd	$⊢ φ \to N \in ℤ$
33	32	adantr	$⊢ (φ \land p \in ℙ) \to N \in ℤ$
34	31 33	zaddcld	$⊢ (φ \land p \in ℙ) \to F (N) + N \in ℤ$
35		prmz	$⊢ q \in ℙ \to q \in ℤ$
36		zltp1le	$⊢ (F (N) + N \in ℤ \land q \in ℤ) \to (F (N) + N < q \leftrightarrow F (N) + N + 1 \leq q)$
37	34 35 36	syl2an	$⊢ ((φ \land p \in ℙ) \land q \in ℙ) \to (F (N) + N < q \leftrightarrow F (N) + N + 1 \leq q)$
38	37	biimpa	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land F (N) + N < q) \to F (N) + N + 1 \leq q$
39	29 38	eqbrtrd	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land F (N) + N < q) \to F (N) + 1 + N \leq q$
40	39	expcom	$⊢ F (N) + N < q \to (((φ \land p \in ℙ) \land q \in ℙ) \to F (N) + 1 + N \leq q)$
41	40	adantl	$⊢ (p < F (N) + 2 \land F (N) + N < q) \to (((φ \land p \in ℙ) \land q \in ℙ) \to F (N) + 1 + N \leq q)$
42	41	imp	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to F (N) + 1 + N \leq q$
43		df-2	$⊢ 2 = 1 + 1$
44	43	a1i	$⊢ φ \to 2 = 1 + 1$
45	44	oveq2d	$⊢ φ \to F (N) + 2 = F (N) + 1 + 1$
46	24 25 25	addassd	$⊢ φ \to F (N) + 1 + 1 = F (N) + 1 + 1$
47	45 46	eqtr4d	$⊢ φ \to F (N) + 2 = F (N) + 1 + 1$
48	47	adantr	$⊢ (φ \land p \in ℙ) \to F (N) + 2 = F (N) + 1 + 1$
49	48	breq2d	$⊢ (φ \land p \in ℙ) \to (p < F (N) + 2 \leftrightarrow p < F (N) + 1 + 1)$
50		prmz	$⊢ p \in ℙ \to p \in ℤ$
51	30	peano2zd	$⊢ φ \to F (N) + 1 \in ℤ$
52		zleltp1	$⊢ (p \in ℤ \land F (N) + 1 \in ℤ) \to (p \leq F (N) + 1 \leftrightarrow p < F (N) + 1 + 1)$
53	50 51 52	syl2anr	$⊢ (φ \land p \in ℙ) \to (p \leq F (N) + 1 \leftrightarrow p < F (N) + 1 + 1)$
54	53	biimprd	$⊢ (φ \land p \in ℙ) \to (p < F (N) + 1 + 1 \to p \leq F (N) + 1)$
55	49 54	sylbid	$⊢ (φ \land p \in ℙ) \to (p < F (N) + 2 \to p \leq F (N) + 1)$
56	55	adantr	$⊢ ((φ \land p \in ℙ) \land q \in ℙ) \to (p < F (N) + 2 \to p \leq F (N) + 1)$
57	56	com12	$⊢ p < F (N) + 2 \to (((φ \land p \in ℙ) \land q \in ℙ) \to p \leq F (N) + 1)$
58	57	adantr	$⊢ (p < F (N) + 2 \land F (N) + N < q) \to (((φ \land p \in ℙ) \land q \in ℙ) \to p \leq F (N) + 1)$
59	58	imp	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to p \leq F (N) + 1$
60	6 10 13 23 42 59	lesub3d	$⊢ ((p < F (N) + 2 \land F (N) + N < q) \land ((φ \land p \in ℙ) \land q \in ℙ)) \to N \leq q - p$
61	60	ex	$⊢ (p < F (N) + 2 \land F (N) + N < q) \to (((φ \land p \in ℙ) \land q \in ℙ) \to N \leq q - p)$
62	61	3adant3	$⊢ (p < F (N) + 2 \land F (N) + N < q \land \forall z \in (p + 1 ..^q) z \notin ℙ) \to (((φ \land p \in ℙ) \land q \in ℙ) \to N \leq q - p)$
63	62	impcom	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land (p < F (N) + 2 \land F (N) + N < q \land \forall z \in (p + 1 ..^q) z \notin ℙ)) \to N \leq q - p$
64		simpr3	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land (p < F (N) + 2 \land F (N) + N < q \land \forall z \in (p + 1 ..^q) z \notin ℙ)) \to \forall z \in (p + 1 ..^q) z \notin ℙ$
65	63 64	jca	$⊢ (((φ \land p \in ℙ) \land q \in ℙ) \land (p < F (N) + 2 \land F (N) + N < q \land \forall z \in (p + 1 ..^q) z \notin ℙ)) \to (N \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$
66	1 2 3	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 ℙ)$
67	65 66	reximddv2	$⊢ φ \to \exists p \in ℙ \exists q \in ℙ (N \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$

Metamath Proof Explorer

Theorem prmgaplem8

Proof