Metamath Proof Explorer

Theorem prmgaplem8

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

Ref Expression
Hypotheses prmgaplem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmgaplem7.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℕ ↑m ℕ ) )
prmgaplem7.i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) )
Assertion prmgaplem8 ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )

Proof

Step Hyp Ref Expression
1 prmgaplem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 prmgaplem7.f ⊢ ( 𝜑 → 𝐹 ∈ ( ℕ ↑m ℕ ) )
3 prmgaplem7.i ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 2 ... 𝑁 ) 1 < ( ( ( 𝐹 ‘ 𝑁 ) + 𝑖 ) gcd 𝑖 ) )
4 prmnn ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ )
5 4 nnred ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℝ )
6 5 ad2antll ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑞 ∈ ℝ )
7 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
8 7 nnred ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
9 8 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑝 ∈ ℝ )
10 9 adantl ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑝 ∈ ℝ )
11 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑁 ∈ ℝ )
13 12 adantl ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑁 ∈ ℝ )
14 elmapi ⊢ ( 𝐹 ∈ ( ℕ ↑m ℕ ) → 𝐹 : ℕ ⟶ ℕ )
15 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℕ )
16 15 ex ⊢ ( 𝐹 : ℕ ⟶ ℕ → ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) )
17 2 14 16 3syl ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ∈ ℕ ) )
18 1 17 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℕ )
19 18 nnred ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
21 20 adantl ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
22 1red ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 1 ∈ ℝ )
23 21 22 readdcld ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → ( ( 𝐹 ‘ 𝑁 ) + 1 ) ∈ ℝ )
24 18 nncnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
25 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
26 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
27 24 25 26 add32d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) = ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) = ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) )
29 28 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) = ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) )
30 18 nnzd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℤ )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℤ )
32 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
34 31 33 zaddcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℤ )
35 prmz ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
36 zltp1le ⊢ ( ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ↔ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ≤ 𝑞 ) )
37 34 35 36 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ↔ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ≤ 𝑞 ) )
38 37 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) + 1 ) ≤ 𝑞 )
39 29 38 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) ≤ 𝑞 )
40 39 expcom ⊢ ( ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) ≤ 𝑞 ) )
41 40 adantl ⊢ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) ≤ 𝑞 ) )
42 41 imp ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 𝑁 ) ≤ 𝑞 )
43 df-2 ⊢ 2 = ( 1 + 1 )
44 43 a1i ⊢ ( 𝜑 → 2 = ( 1 + 1 ) )
45 44 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) + 2 ) = ( ( 𝐹 ‘ 𝑁 ) + ( 1 + 1 ) ) )
46 24 25 25 addassd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) = ( ( 𝐹 ‘ 𝑁 ) + ( 1 + 1 ) ) )
47 45 46 eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) + 2 ) = ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝐹 ‘ 𝑁 ) + 2 ) = ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) )
49 48 breq2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ↔ 𝑝 < ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) ) )
50 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
51 30 peano2zd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) + 1 ) ∈ ℤ )
52 zleltp1 ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ∈ ℤ ) → ( 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ↔ 𝑝 < ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) ) )
53 50 51 52 syl2anr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ↔ 𝑝 < ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) ) )
54 53 biimprd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 < ( ( ( 𝐹 ‘ 𝑁 ) + 1 ) + 1 ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ) )
55 49 54 sylbid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ) )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ) )
57 56 com12 ⊢ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ) )
58 57 adantr ⊢ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) ) )
59 58 imp ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑝 ≤ ( ( 𝐹 ‘ 𝑁 ) + 1 ) )
60 6 10 13 23 42 59 lesub3d ⊢ ( ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) ∧ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ) → 𝑁 ≤ ( 𝑞 − 𝑝 ) )
61 60 ex ⊢ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ) → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑁 ≤ ( 𝑞 − 𝑝 ) ) )
62 61 3adant3 ⊢ ( ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) → ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑁 ≤ ( 𝑞 − 𝑝 ) ) )
63 62 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) → 𝑁 ≤ ( 𝑞 − 𝑝 ) )
64 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) → ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )
65 63 64 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) ) → ( 𝑁 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
66 1 2 3 prmgaplem7 ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 < ( ( 𝐹 ‘ 𝑁 ) + 2 ) ∧ ( ( 𝐹 ‘ 𝑁 ) + 𝑁 ) < 𝑞 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
67 65 66 reximddv2 ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )