# Metamath Proof Explorer

## Theorem prmgaplem8

Description: Lemma for prmgap . (Contributed by AV, 13-Aug-2020)

Ref Expression
Hypotheses prmgaplem7.n ${⊢}{\phi }\to {N}\in ℕ$
prmgaplem7.f ${⊢}{\phi }\to {F}\in \left({ℕ}^{ℕ}\right)$
prmgaplem7.i ${⊢}{\phi }\to \forall {i}\in \left(2\dots {N}\right)\phantom{\rule{.4em}{0ex}}1<\left({F}\left({N}\right)+{i}\right)\mathrm{gcd}{i}$
Assertion prmgaplem8 ${⊢}{\phi }\to \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({N}\le {q}-{p}\wedge \forall {z}\in \left({p}+1..^{q}\right)\phantom{\rule{.4em}{0ex}}{z}\notin ℙ\right)$

### Proof

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