Metamath Proof Explorer

Theorem nnunb

Description: The set of positive integers is unbounded above. Theorem I.28 of Apostol p. 26. (Contributed by NM, 21-Jan-1997)

Ref Expression
Assertion nnunb ⊢ ¬ ∃ x ∈ ℝ ∀ y ∈ ℕ y < x ∨ y = x

Proof

Step Hyp Ref Expression
1 pm3.24 ⊢ ¬ ∀ y ∈ ℕ ¬ x < y ∧ ¬ ∀ y ∈ ℕ ¬ x < y
2 peano2rem ⊢ x ∈ ℝ → x − 1 ∈ ℝ
3 ltm1 ⊢ x ∈ ℝ → x − 1 < x
4 ovex ⊢ x − 1 ∈ V
5 eleq1 ⊢ y = x − 1 → y ∈ ℝ ↔ x − 1 ∈ ℝ
6 breq1 ⊢ y = x − 1 → y < x ↔ x − 1 < x
7 breq1 ⊢ y = x − 1 → y < z ↔ x − 1 < z
8 7 rexbidv ⊢ y = x − 1 → ∃ z ∈ ℕ y < z ↔ ∃ z ∈ ℕ x − 1 < z
9 6 8 imbi12d ⊢ y = x − 1 → y < x → ∃ z ∈ ℕ y < z ↔ x − 1 < x → ∃ z ∈ ℕ x − 1 < z
10 5 9 imbi12d ⊢ y = x − 1 → y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z ↔ x − 1 ∈ ℝ → x − 1 < x → ∃ z ∈ ℕ x − 1 < z
11 4 10 spcv ⊢ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → x − 1 ∈ ℝ → x − 1 < x → ∃ z ∈ ℕ x − 1 < z
12 3 11 syl7 ⊢ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → x − 1 ∈ ℝ → x ∈ ℝ → ∃ z ∈ ℕ x − 1 < z
13 2 12 syl5 ⊢ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → x ∈ ℝ → x ∈ ℝ → ∃ z ∈ ℕ x − 1 < z
14 13 pm2.43d ⊢ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → x ∈ ℝ → ∃ z ∈ ℕ x − 1 < z
15 df-rex ⊢ ∃ z ∈ ℕ x − 1 < z ↔ ∃ z z ∈ ℕ ∧ x − 1 < z
16 14 15 syl6ib ⊢ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → x ∈ ℝ → ∃ z z ∈ ℕ ∧ x − 1 < z
17 16 com12 ⊢ x ∈ ℝ → ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → ∃ z z ∈ ℕ ∧ x − 1 < z
18 nnre ⊢ z ∈ ℕ → z ∈ ℝ
19 1re ⊢ 1 ∈ ℝ
20 ltsubadd ⊢ x ∈ ℝ ∧ 1 ∈ ℝ ∧ z ∈ ℝ → x − 1 < z ↔ x < z + 1
21 19 20 mp3an2 ⊢ x ∈ ℝ ∧ z ∈ ℝ → x − 1 < z ↔ x < z + 1
22 18 21 sylan2 ⊢ x ∈ ℝ ∧ z ∈ ℕ → x − 1 < z ↔ x < z + 1
23 22 pm5.32da ⊢ x ∈ ℝ → z ∈ ℕ ∧ x − 1 < z ↔ z ∈ ℕ ∧ x < z + 1
24 23 exbidv ⊢ x ∈ ℝ → ∃ z z ∈ ℕ ∧ x − 1 < z ↔ ∃ z z ∈ ℕ ∧ x < z + 1
25 peano2nn ⊢ z ∈ ℕ → z + 1 ∈ ℕ
26 ovex ⊢ z + 1 ∈ V
27 eleq1 ⊢ y = z + 1 → y ∈ ℕ ↔ z + 1 ∈ ℕ
28 breq2 ⊢ y = z + 1 → x < y ↔ x < z + 1
29 27 28 anbi12d ⊢ y = z + 1 → y ∈ ℕ ∧ x < y ↔ z + 1 ∈ ℕ ∧ x < z + 1
30 26 29 spcev ⊢ z + 1 ∈ ℕ ∧ x < z + 1 → ∃ y y ∈ ℕ ∧ x < y
31 25 30 sylan ⊢ z ∈ ℕ ∧ x < z + 1 → ∃ y y ∈ ℕ ∧ x < y
32 31 exlimiv ⊢ ∃ z z ∈ ℕ ∧ x < z + 1 → ∃ y y ∈ ℕ ∧ x < y
33 24 32 syl6bi ⊢ x ∈ ℝ → ∃ z z ∈ ℕ ∧ x − 1 < z → ∃ y y ∈ ℕ ∧ x < y
34 17 33 syld ⊢ x ∈ ℝ → ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z → ∃ y y ∈ ℕ ∧ x < y
35 df-ral ⊢ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z ↔ ∀ y y ∈ ℝ → y < x → ∃ z ∈ ℕ y < z
36 df-ral ⊢ ∀ y ∈ ℕ ¬ x < y ↔ ∀ y y ∈ ℕ → ¬ x < y
37 alinexa ⊢ ∀ y y ∈ ℕ → ¬ x < y ↔ ¬ ∃ y y ∈ ℕ ∧ x < y
38 36 37 bitr2i ⊢ ¬ ∃ y y ∈ ℕ ∧ x < y ↔ ∀ y ∈ ℕ ¬ x < y
39 38 con1bii ⊢ ¬ ∀ y ∈ ℕ ¬ x < y ↔ ∃ y y ∈ ℕ ∧ x < y
40 34 35 39 3imtr4g ⊢ x ∈ ℝ → ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z → ¬ ∀ y ∈ ℕ ¬ x < y
41 40 anim2d ⊢ x ∈ ℝ → ∀ y ∈ ℕ ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z → ∀ y ∈ ℕ ¬ x < y ∧ ¬ ∀ y ∈ ℕ ¬ x < y
42 1 41 mtoi ⊢ x ∈ ℝ → ¬ ∀ y ∈ ℕ ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z
43 42 nrex ⊢ ¬ ∃ x ∈ ℝ ∀ y ∈ ℕ ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z
44 nnssre ⊢ ℕ ⊆ ℝ
45 1nn ⊢ 1 ∈ ℕ
46 45 ne0ii ⊢ ℕ ≠ ∅
47 sup2 ⊢ ℕ ⊆ ℝ ∧ ℕ ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ ℕ y < x ∨ y = x → ∃ x ∈ ℝ ∀ y ∈ ℕ ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z
48 44 46 47 mp3an12 ⊢ ∃ x ∈ ℝ ∀ y ∈ ℕ y < x ∨ y = x → ∃ x ∈ ℝ ∀ y ∈ ℕ ¬ x < y ∧ ∀ y ∈ ℝ y < x → ∃ z ∈ ℕ y < z
49 43 48 mto ⊢ ¬ ∃ x ∈ ℝ ∀ y ∈ ℕ y < x ∨ y = x