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 ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 ∨ 𝑦 = 𝑥 )

Proof

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