# 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}={ℤ}_{\ge {M}}$
Assertion uzsup ${⊢}{M}\in ℤ\to sup\left({Z},{ℝ}^{*},<\right)=\mathrm{+\infty }$

### Proof

Step Hyp Ref Expression
1 uzsup.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 simpl ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to {M}\in ℤ$
3 flcl ${⊢}{x}\in ℝ\to ⌊{x}⌋\in ℤ$
4 3 peano2zd ${⊢}{x}\in ℝ\to ⌊{x}⌋+1\in ℤ$
5 id ${⊢}{M}\in ℤ\to {M}\in ℤ$
6 ifcl ${⊢}\left(⌊{x}⌋+1\in ℤ\wedge {M}\in ℤ\right)\to if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in ℤ$
7 4 5 6 syl2anr ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in ℤ$
8 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
9 reflcl ${⊢}{x}\in ℝ\to ⌊{x}⌋\in ℝ$
10 peano2re ${⊢}⌊{x}⌋\in ℝ\to ⌊{x}⌋+1\in ℝ$
11 9 10 syl ${⊢}{x}\in ℝ\to ⌊{x}⌋+1\in ℝ$
12 max1 ${⊢}\left({M}\in ℝ\wedge ⌊{x}⌋+1\in ℝ\right)\to {M}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)$
13 8 11 12 syl2an ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to {M}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)$
14 eluz2 ${⊢}if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in ℤ\wedge {M}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\right)$
15 2 7 13 14 syl3anbrc ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in {ℤ}_{\ge {M}}$
16 15 1 eleqtrrdi ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in {Z}$
17 simpr ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to {x}\in ℝ$
18 11 adantl ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to ⌊{x}⌋+1\in ℝ$
19 7 zred ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in ℝ$
20 fllep1 ${⊢}{x}\in ℝ\to {x}\le ⌊{x}⌋+1$
21 20 adantl ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to {x}\le ⌊{x}⌋+1$
22 max2 ${⊢}\left({M}\in ℝ\wedge ⌊{x}⌋+1\in ℝ\right)\to ⌊{x}⌋+1\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)$
23 8 11 22 syl2an ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to ⌊{x}⌋+1\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)$
24 17 18 19 21 23 letrd ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to {x}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)$
25 breq2 ${⊢}{n}=if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\to \left({x}\le {n}↔{x}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\right)$
26 25 rspcev ${⊢}\left(if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\in {Z}\wedge {x}\le if\left({M}\le ⌊{x}⌋+1,⌊{x}⌋+1,{M}\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {n}$
27 16 24 26 syl2anc ${⊢}\left({M}\in ℤ\wedge {x}\in ℝ\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {n}$
28 27 ralrimiva ${⊢}{M}\in ℤ\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {n}$
29 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
30 1 29 eqsstri ${⊢}{Z}\subseteq ℤ$
31 zssre ${⊢}ℤ\subseteq ℝ$
32 30 31 sstri ${⊢}{Z}\subseteq ℝ$
33 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
34 32 33 sstri ${⊢}{Z}\subseteq {ℝ}^{*}$
35 supxrunb1 ${⊢}{Z}\subseteq {ℝ}^{*}\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {n}↔sup\left({Z},{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$
36 34 35 ax-mp ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\le {n}↔sup\left({Z},{ℝ}^{*},<\right)=\mathrm{+\infty }$
37 28 36 sylib ${⊢}{M}\in ℤ\to sup\left({Z},{ℝ}^{*},<\right)=\mathrm{+\infty }$