Metamath Proof Explorer

Theorem uzsup

Description: An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

Ref Expression
Hypothesis uzsup.1 ⊢ Z = ℤ ≥ M
Assertion uzsup ⊢ M ∈ ℤ → sup Z ℝ * < = +∞

Proof

Step Hyp Ref Expression
1 uzsup.1 ⊢ Z = ℤ ≥ M
2 simpl ⊢ M ∈ ℤ ∧ x ∈ ℝ → M ∈ ℤ
3 flcl ⊢ x ∈ ℝ → x ∈ ℤ
4 3 peano2zd ⊢ x ∈ ℝ → x + 1 ∈ ℤ
5 id ⊢ M ∈ ℤ → M ∈ ℤ
6 ifcl ⊢ x + 1 ∈ ℤ ∧ M ∈ ℤ → if M ≤ x + 1 x + 1 M ∈ ℤ
7 4 5 6 syl2anr ⊢ M ∈ ℤ ∧ x ∈ ℝ → if M ≤ x + 1 x + 1 M ∈ ℤ
8 zre ⊢ M ∈ ℤ → M ∈ ℝ
9 reflcl ⊢ x ∈ ℝ → x ∈ ℝ
10 peano2re ⊢ x ∈ ℝ → x + 1 ∈ ℝ
11 9 10 syl ⊢ x ∈ ℝ → x + 1 ∈ ℝ
12 max1 ⊢ M ∈ ℝ ∧ x + 1 ∈ ℝ → M ≤ if M ≤ x + 1 x + 1 M
13 8 11 12 syl2an ⊢ M ∈ ℤ ∧ x ∈ ℝ → M ≤ if M ≤ x + 1 x + 1 M
14 eluz2 ⊢ if M ≤ x + 1 x + 1 M ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ if M ≤ x + 1 x + 1 M ∈ ℤ ∧ M ≤ if M ≤ x + 1 x + 1 M
15 2 7 13 14 syl3anbrc ⊢ M ∈ ℤ ∧ x ∈ ℝ → if M ≤ x + 1 x + 1 M ∈ ℤ ≥ M
16 15 1 eleqtrrdi ⊢ M ∈ ℤ ∧ x ∈ ℝ → if M ≤ x + 1 x + 1 M ∈ Z
17 simpr ⊢ M ∈ ℤ ∧ x ∈ ℝ → x ∈ ℝ
18 11 adantl ⊢ M ∈ ℤ ∧ x ∈ ℝ → x + 1 ∈ ℝ
19 7 zred ⊢ M ∈ ℤ ∧ x ∈ ℝ → if M ≤ x + 1 x + 1 M ∈ ℝ
20 fllep1 ⊢ x ∈ ℝ → x ≤ x + 1
21 20 adantl ⊢ M ∈ ℤ ∧ x ∈ ℝ → x ≤ x + 1
22 max2 ⊢ M ∈ ℝ ∧ x + 1 ∈ ℝ → x + 1 ≤ if M ≤ x + 1 x + 1 M
23 8 11 22 syl2an ⊢ M ∈ ℤ ∧ x ∈ ℝ → x + 1 ≤ if M ≤ x + 1 x + 1 M
24 17 18 19 21 23 letrd ⊢ M ∈ ℤ ∧ x ∈ ℝ → x ≤ if M ≤ x + 1 x + 1 M
25 breq2 ⊢ n = if M ≤ x + 1 x + 1 M → x ≤ n ↔ x ≤ if M ≤ x + 1 x + 1 M
26 25 rspcev ⊢ if M ≤ x + 1 x + 1 M ∈ Z ∧ x ≤ if M ≤ x + 1 x + 1 M → ∃ n ∈ Z x ≤ n
27 16 24 26 syl2anc ⊢ M ∈ ℤ ∧ x ∈ ℝ → ∃ n ∈ Z x ≤ n
28 27 ralrimiva ⊢ M ∈ ℤ → ∀ x ∈ ℝ ∃ n ∈ Z x ≤ n
29 uzssz ⊢ ℤ ≥ M ⊆ ℤ
30 1 29 eqsstri ⊢ Z ⊆ ℤ
31 zssre ⊢ ℤ ⊆ ℝ
32 30 31 sstri ⊢ Z ⊆ ℝ
33 ressxr ⊢ ℝ ⊆ ℝ *
34 32 33 sstri ⊢ Z ⊆ ℝ *
35 supxrunb1 ⊢ Z ⊆ ℝ * → ∀ x ∈ ℝ ∃ n ∈ Z x ≤ n ↔ sup Z ℝ * < = +∞
36 34 35 ax-mp ⊢ ∀ x ∈ ℝ ∃ n ∈ Z x ≤ n ↔ sup Z ℝ * < = +∞
37 28 36 sylib ⊢ M ∈ ℤ → sup Z ℝ * < = +∞