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 ⊢S=n∈ℕ|1<n∧∀m∈ℕnm∈ℕ→m=1∨m=n
Assertion infpn2 ⊢S≈ℕ

Proof

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