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 ( 𝑍 , ℝ* , < ) = +∞ )