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

Proof

Step Hyp Ref Expression
1 infpn2.1 ⊢ S = n ∈ ℕ | 1 < n ∧ ∀ m ∈ ℕ n m ∈ ℕ → m = 1 ∨ m = n
2 1 ssrab3 ⊢ S ⊆ ℕ
3 infpn ⊢ j ∈ ℕ → ∃ k ∈ ℕ j < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → 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 ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k → j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
14 anass ⊢ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ↔ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
15 13 14 imbitrdi ⊢ j ∈ ℕ ∧ k ∈ ℕ → j < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k → j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
16 15 reximdva ⊢ j ∈ ℕ → ∃ k ∈ ℕ j < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k → ∃ k ∈ ℕ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
17 3 16 mpd ⊢ j ∈ ℕ → ∃ k ∈ ℕ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
18 breq2 ⊢ n = k → 1 < n ↔ 1 < k
19 oveq1 ⊢ n = k → n m = k m
20 19 eleq1d ⊢ n = k → n m ∈ ℕ ↔ k m ∈ ℕ
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 → n m ∈ ℕ → m = 1 ∨ m = n ↔ k m ∈ ℕ → m = 1 ∨ m = k
24 23 ralbidv ⊢ n = k → ∀ m ∈ ℕ n m ∈ ℕ → m = 1 ∨ m = n ↔ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
25 18 24 anbi12d ⊢ n = k → 1 < n ∧ ∀ m ∈ ℕ n m ∈ ℕ → m = 1 ∨ m = n ↔ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
26 25 1 elrab2 ⊢ k ∈ S ↔ k ∈ ℕ ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
27 26 anbi1i ⊢ k ∈ S ∧ j < k ↔ k ∈ ℕ ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ∧ j < k
28 anass ⊢ k ∈ ℕ ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ∧ j < k ↔ k ∈ ℕ ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ∧ j < k
29 ancom ⊢ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ∧ j < k ↔ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
30 29 anbi2i ⊢ k ∈ ℕ ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k ∧ j < k ↔ k ∈ ℕ ∧ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
31 27 28 30 3bitri ⊢ k ∈ S ∧ j < k ↔ k ∈ ℕ ∧ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
32 31 rexbii2 ⊢ ∃ k ∈ S j < k ↔ ∃ k ∈ ℕ j < k ∧ 1 < k ∧ ∀ m ∈ ℕ k m ∈ ℕ → m = 1 ∨ m = k
33 17 32 sylibr ⊢ j ∈ ℕ → ∃ k ∈ S j < k
34 33 rgen ⊢ ∀ j ∈ ℕ ∃ k ∈ S j < k
35 unben ⊢ S ⊆ ℕ ∧ ∀ j ∈ ℕ ∃ k ∈ S j < k → S ≈ ℕ
36 2 34 35 mp2an ⊢ S ≈ ℕ