Metamath Proof Explorer

Theorem prmgaplem5

Description: Lemma for prmgap : for each integer greater than 2 there is a smaller prime closest to this integer, i.e. there is a smaller prime and no other prime is between this prime and the integer. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion prmgaplem5 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )

Proof

Step Hyp Ref Expression
1 elrabi ⊢ ( 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑟 ∈ ℙ )
2 1 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) → 𝑟 ∈ ℙ )
3 breq1 ⊢ ( 𝑝 = 𝑟 → ( 𝑝 < 𝑁 ↔ 𝑟 < 𝑁 ) )
4 oveq1 ⊢ ( 𝑝 = 𝑟 → ( 𝑝 + 1 ) = ( 𝑟 + 1 ) )
5 4 oveq1d ⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 + 1 ) ..^ 𝑁 ) = ( ( 𝑟 + 1 ) ..^ 𝑁 ) )
6 5 raleqdv ⊢ ( 𝑝 = 𝑟 → ( ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ↔ ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )
7 3 6 anbi12d ⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) ↔ ( 𝑟 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) ) )
8 7 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) ∧ 𝑝 = 𝑟 ) → ( ( 𝑝 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) ↔ ( 𝑟 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) ) )
9 breq1 ⊢ ( 𝑞 = 𝑟 → ( 𝑞 < 𝑁 ↔ 𝑟 < 𝑁 ) )
10 9 elrab ⊢ ( 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ↔ ( 𝑟 ∈ ℙ ∧ 𝑟 < 𝑁 ) )
11 10 simprbi ⊢ ( 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑟 < 𝑁 )
12 11 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) → 𝑟 < 𝑁 )
13 elfzo2 ⊢ ( 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) ↔ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) )
14 breq1 ⊢ ( 𝑞 = 𝑧 → ( 𝑞 < 𝑁 ↔ 𝑧 < 𝑁 ) )
15 simpl ⊢ ( ( 𝑧 ∈ ℙ ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → 𝑧 ∈ ℙ )
16 simpr3 ⊢ ( ( 𝑧 ∈ ℙ ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → 𝑧 < 𝑁 )
17 14 15 16 elrabd ⊢ ( ( 𝑧 ∈ ℙ ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } )
18 17 adantrl ⊢ ( ( 𝑧 ∈ ℙ ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) ) → 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } )
19 eluz2 ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ↔ ( ( 𝑟 + 1 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( 𝑟 + 1 ) ≤ 𝑧 ) )
20 prmz ⊢ ( 𝑟 ∈ ℙ → 𝑟 ∈ ℤ )
21 zltp1le ⊢ ( ( 𝑟 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑟 < 𝑧 ↔ ( 𝑟 + 1 ) ≤ 𝑧 ) )
22 20 21 sylan ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ ) → ( 𝑟 < 𝑧 ↔ ( 𝑟 + 1 ) ≤ 𝑧 ) )
23 prmnn ⊢ ( 𝑟 ∈ ℙ → 𝑟 ∈ ℕ )
24 23 nnred ⊢ ( 𝑟 ∈ ℙ → 𝑟 ∈ ℝ )
25 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
26 ltnle ⊢ ( ( 𝑟 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑟 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑟 ) )
27 26 biimpd ⊢ ( ( 𝑟 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑟 < 𝑧 → ¬ 𝑧 ≤ 𝑟 ) )
28 24 25 27 syl2an ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ ) → ( 𝑟 < 𝑧 → ¬ 𝑧 ≤ 𝑟 ) )
29 pm2.21 ⊢ ( ¬ 𝑧 ≤ 𝑟 → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) )
30 28 29 syl6 ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ ) → ( 𝑟 < 𝑧 → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
31 22 30 sylbird ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑟 + 1 ) ≤ 𝑧 → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
32 31 expcom ⊢ ( 𝑧 ∈ ℤ → ( 𝑟 ∈ ℙ → ( ( 𝑟 + 1 ) ≤ 𝑧 → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) ) )
33 32 com23 ⊢ ( 𝑧 ∈ ℤ → ( ( 𝑟 + 1 ) ≤ 𝑧 → ( 𝑟 ∈ ℙ → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) ) )
34 33 a1i ⊢ ( ( 𝑟 + 1 ) ∈ ℤ → ( 𝑧 ∈ ℤ → ( ( 𝑟 + 1 ) ≤ 𝑧 → ( 𝑟 ∈ ℙ → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) ) ) )
35 34 3imp ⊢ ( ( ( 𝑟 + 1 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ ( 𝑟 + 1 ) ≤ 𝑧 ) → ( 𝑟 ∈ ℙ → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
36 19 35 sylbi ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) → ( 𝑟 ∈ ℙ → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
37 36 3ad2ant1 ⊢ ( ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) → ( 𝑟 ∈ ℙ → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
38 1 37 syl5com ⊢ ( 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → ( ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
39 38 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) → ( ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) ) )
40 39 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) )
41 40 adantl ⊢ ( ( 𝑧 ∈ ℙ ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) ) → ( 𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ ) )
42 18 41 embantd ⊢ ( ( 𝑧 ∈ ℙ ∧ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → 𝑧 ∉ ℙ ) )
43 42 ex ⊢ ( 𝑧 ∈ ℙ → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → 𝑧 ∉ ℙ ) ) )
44 df-nel ⊢ ( 𝑧 ∉ ℙ ↔ ¬ 𝑧 ∈ ℙ )
45 2a1 ⊢ ( 𝑧 ∉ ℙ → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → 𝑧 ∉ ℙ ) ) )
46 44 45 sylbir ⊢ ( ¬ 𝑧 ∈ ℙ → ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → 𝑧 ∉ ℙ ) ) )
47 43 46 pm2.61i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → 𝑧 ∉ ℙ ) )
48 47 impancom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) ) → ( ( 𝑧 ∈ ( ℤ≥ ‘ ( 𝑟 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁 ) → 𝑧 ∉ ℙ ) )
49 13 48 syl5bi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) ) → ( 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) → 𝑧 ∉ ℙ ) )
50 49 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) → ( ( 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } → 𝑧 ≤ 𝑟 ) → ( 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) → 𝑧 ∉ ℙ ) ) )
51 50 ralimdv2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) → ( ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 → ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )
52 51 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) → ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ )
53 12 52 jca ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) → ( 𝑟 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑟 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )
54 2 8 53 rspcedvd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ) ∧ ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )
55 eqid ⊢ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } = { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 }
56 55 prmgaplem3 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑟 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } ∀ 𝑧 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 < 𝑁 } 𝑧 ≤ 𝑟 )
57 54 56 r19.29a ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∈ ℙ ( 𝑝 < 𝑁 ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑁 ) 𝑧 ∉ ℙ ) )