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 ⊢∀yy∈ℝ→y<x→∃z∈ℕy<z→x−1∈ℝ→x−1<x→∃z∈ℕx−1<z
12 3 11 syl7 ⊢∀yy∈ℝ→y<x→∃z∈ℕy<z→x−1∈ℝ→x∈ℝ→∃z∈ℕx−1<z
13 2 12 syl5 ⊢∀yy∈ℝ→y<x→∃z∈ℕy<z→x∈ℝ→x∈ℝ→∃z∈ℕx−1<z
14 13 pm2.43d ⊢∀yy∈ℝ→y<x→∃z∈ℕy<z→x∈ℝ→∃z∈ℕx−1<z
15 df-rex ⊢∃z∈ℕx−1<z↔∃zz∈ℕ∧x−1<z
16 14 15 imbitrdi ⊢∀yy∈ℝ→y<x→∃z∈ℕy<z→x∈ℝ→∃zz∈ℕ∧x−1<z
17 16 com12 ⊢x∈ℝ→∀yy∈ℝ→y<x→∃z∈ℕy<z→∃zz∈ℕ∧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∈ℝ→∃zz∈ℕ∧x−1<z↔∃zz∈ℕ∧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→∃yy∈ℕ∧x<y
31 25 30 sylan ⊢z∈ℕ∧x<z+1→∃yy∈ℕ∧x<y
32 31 exlimiv ⊢∃zz∈ℕ∧x<z+1→∃yy∈ℕ∧x<y
33 24 32 syl6bi ⊢x∈ℝ→∃zz∈ℕ∧x−1<z→∃yy∈ℕ∧x<y
34 17 33 syld ⊢x∈ℝ→∀yy∈ℝ→y<x→∃z∈ℕy<z→∃yy∈ℕ∧x<y
35 df-ral ⊢∀y∈ℝy<x→∃z∈ℕy<z↔∀yy∈ℝ→y<x→∃z∈ℕy<z
36 df-ral ⊢∀y∈ℕ¬x<y↔∀yy∈ℕ→¬x<y
37 alinexa ⊢∀yy∈ℕ→¬x<y↔¬∃yy∈ℕ∧x<y
38 36 37 bitr2i ⊢¬∃yy∈ℕ∧x<y↔∀y∈ℕ¬x<y
39 38 con1bii ⊢¬∀y∈ℕ¬x<y↔∃yy∈ℕ∧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