This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion uzsup ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )

Proof

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