Metamath Proof Explorer

Theorem infpn2

Description: There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn , so by unben it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005)

Ref Expression
Hypothesis infpn2.1 ⊢ 𝑆 = { 𝑛 ∈ ℕ ∣ ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) }
Assertion infpn2 𝑆 ≈ ℕ

Proof

Step Hyp Ref Expression
1 infpn2.1 ⊢ 𝑆 = { 𝑛 ∈ ℕ ∣ ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) }
2 1 ssrab3 ⊢ 𝑆 ⊆ ℕ
3 infpn ⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
4 nnge1 ⊢ ( 𝑗 ∈ ℕ → 1 ≤ 𝑗 )
5 4 adantr ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑗 )
6 1re ⊢ 1 ∈ ℝ
7 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
8 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
9 lelttr ⊢ ( ( 1 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 1 ≤ 𝑗 ∧ 𝑗 < 𝑘 ) → 1 < 𝑘 ) )
10 6 7 8 9 mp3an3an ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 1 ≤ 𝑗 ∧ 𝑗 < 𝑘 ) → 1 < 𝑘 ) )
11 5 10 mpand ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑗 < 𝑘 → 1 < 𝑘 ) )
12 11 ancld ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑗 < 𝑘 → ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ) )
13 12 anim1d ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ( ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
14 anass ⊢ ( ( ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ↔ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
15 13 14 imbitrdi ⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
16 15 reximdva ⊢ ( 𝑗 ∈ ℕ → ( ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
17 3 16 mpd ⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
18 breq2 ⊢ ( 𝑛 = 𝑘 → ( 1 < 𝑛 ↔ 1 < 𝑘 ) )
19 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 / 𝑚 ) = ( 𝑘 / 𝑚 ) )
20 19 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 / 𝑚 ) ∈ ℕ ↔ ( 𝑘 / 𝑚 ) ∈ ℕ ) )
21 equequ2 ⊢ ( 𝑛 = 𝑘 → ( 𝑚 = 𝑛 ↔ 𝑚 = 𝑘 ) )
22 21 orbi2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ↔ ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) )
23 20 22 imbi12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ↔ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
24 23 ralbidv ⊢ ( 𝑛 = 𝑘 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
25 18 24 anbi12d ⊢ ( 𝑛 = 𝑘 → ( ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) ↔ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
26 25 1 elrab2 ⊢ ( 𝑘 ∈ 𝑆 ↔ ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
27 26 anbi1i ⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘 ) ↔ ( ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ∧ 𝑗 < 𝑘 ) )
28 anass ⊢ ( ( ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ∧ 𝑗 < 𝑘 ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ) )
29 ancom ⊢ ( ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ↔ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
30 29 anbi2i ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
31 27 28 30 3bitri ⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘 ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
32 31 rexbii2 ⊢ ( ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 ↔ ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
33 17 32 sylibr ⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 )
34 33 rgen ⊢ ∀ 𝑗 ∈ ℕ ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘
35 unben ⊢ ( ( 𝑆 ⊆ ℕ ∧ ∀ 𝑗 ∈ ℕ ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 ) → 𝑆 ≈ ℕ )
36 2 34 35 mp2an ⊢ 𝑆 ≈ ℕ