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∈ℤ→supZℝ*<=+∞

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∈ℤ→ifM≤x+1x+1M∈ℤ
7 4 5 6 syl2anr ⊢M∈ℤ∧x∈ℝ→ifM≤x+1x+1M∈ℤ
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≤ifM≤x+1x+1M
13 8 11 12 syl2an ⊢M∈ℤ∧x∈ℝ→M≤ifM≤x+1x+1M
14 eluz2 ⊢ifM≤x+1x+1M∈ℤ≥M↔M∈ℤ∧ifM≤x+1x+1M∈ℤ∧M≤ifM≤x+1x+1M
15 2 7 13 14 syl3anbrc ⊢M∈ℤ∧x∈ℝ→ifM≤x+1x+1M∈ℤ≥M
16 15 1 eleqtrrdi ⊢M∈ℤ∧x∈ℝ→ifM≤x+1x+1M∈Z
17 simpr ⊢M∈ℤ∧x∈ℝ→x∈ℝ
18 11 adantl ⊢M∈ℤ∧x∈ℝ→x+1∈ℝ
19 7 zred ⊢M∈ℤ∧x∈ℝ→ifM≤x+1x+1M∈ℝ
20 fllep1 ⊢x∈ℝ→x≤x+1
21 20 adantl ⊢M∈ℤ∧x∈ℝ→x≤x+1
22 max2 ⊢M∈ℝ∧x+1∈ℝ→x+1≤ifM≤x+1x+1M
23 8 11 22 syl2an ⊢M∈ℤ∧x∈ℝ→x+1≤ifM≤x+1x+1M
24 17 18 19 21 23 letrd ⊢M∈ℤ∧x∈ℝ→x≤ifM≤x+1x+1M
25 breq2 ⊢n=ifM≤x+1x+1M→x≤n↔x≤ifM≤x+1x+1M
26 25 rspcev ⊢ifM≤x+1x+1M∈Z∧x≤ifM≤x+1x+1M→∃n∈Zx≤n
27 16 24 26 syl2anc ⊢M∈ℤ∧x∈ℝ→∃n∈Zx≤n
28 27 ralrimiva ⊢M∈ℤ→∀x∈ℝ∃n∈Zx≤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∈Zx≤n↔supZℝ*<=+∞
36 34 35 ax-mp ⊢∀x∈ℝ∃n∈Zx≤n↔supZℝ*<=+∞
37 28 36 sylib ⊢M∈ℤ→supZℝ*<=+∞