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 = ( ZZ>= ` M )
Assertion uzsup 
|- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )

Proof

Step Hyp Ref Expression
1 uzsup.1 
 |-  Z = ( ZZ>= ` M )
2 simpl 
 |-  ( ( M e. ZZ /\ x e. RR ) -> M e. ZZ )
3 flcl 
 |-  ( x e. RR -> ( |_ ` x ) e. ZZ )
4 3 peano2zd 
 |-  ( x e. RR -> ( ( |_ ` x ) + 1 ) e. ZZ )
5 id 
 |-  ( M e. ZZ -> M e. ZZ )
6 ifcl 
 |-  ( ( ( ( |_ ` x ) + 1 ) e. ZZ /\ M e. ZZ ) -> if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. ZZ )
7 4 5 6 syl2anr 
 |-  ( ( M e. ZZ /\ x e. RR ) -> if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. ZZ )
8 zre 
 |-  ( M e. ZZ -> M e. RR )
9 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
10 peano2re 
 |-  ( ( |_ ` x ) e. RR -> ( ( |_ ` x ) + 1 ) e. RR )
11 9 10 syl 
 |-  ( x e. RR -> ( ( |_ ` x ) + 1 ) e. RR )
12 max1 
 |-  ( ( M e. RR /\ ( ( |_ ` x ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) )
13 8 11 12 syl2an 
 |-  ( ( M e. ZZ /\ x e. RR ) -> M <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) )
14 eluz2 
 |-  ( if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. ZZ /\ M <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) ) )
15 2 7 13 14 syl3anbrc 
 |-  ( ( M e. ZZ /\ x e. RR ) -> if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. ( ZZ>= ` M ) )
16 15 1 eleqtrrdi 
 |-  ( ( M e. ZZ /\ x e. RR ) -> if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. Z )
17 simpr 
 |-  ( ( M e. ZZ /\ x e. RR ) -> x e. RR )
18 11 adantl 
 |-  ( ( M e. ZZ /\ x e. RR ) -> ( ( |_ ` x ) + 1 ) e. RR )
19 7 zred 
 |-  ( ( M e. ZZ /\ x e. RR ) -> if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) e. RR )
20 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
21 20 adantl 
 |-  ( ( M e. ZZ /\ x e. RR ) -> x <_ ( ( |_ ` x ) + 1 ) )
22 max2 
 |-  ( ( M e. RR /\ ( ( |_ ` x ) + 1 ) e. RR ) -> ( ( |_ ` x ) + 1 ) <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) )
23 8 11 22 syl2an 
 |-  ( ( M e. ZZ /\ x e. RR ) -> ( ( |_ ` x ) + 1 ) <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) )
24 17 18 19 21 23 letrd 
 |-  ( ( M e. ZZ /\ x e. RR ) -> 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 ) e. Z /\ x <_ if ( M <_ ( ( |_ ` x ) + 1 ) , ( ( |_ ` x ) + 1 ) , M ) ) -> E. n e. Z x <_ n )
27 16 24 26 syl2anc 
 |-  ( ( M e. ZZ /\ x e. RR ) -> E. n e. Z x <_ n )
28 27 ralrimiva 
 |-  ( M e. ZZ -> A. x e. RR E. n e. Z x <_ n )
29 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
30 1 29 eqsstri 
 |-  Z C_ ZZ
31 zssre 
 |-  ZZ C_ RR
32 30 31 sstri 
 |-  Z C_ RR
33 ressxr 
 |-  RR C_ RR*
34 32 33 sstri 
 |-  Z C_ RR*
35 supxrunb1 
 |-  ( Z C_ RR* -> ( A. x e. RR E. n e. Z x <_ n <-> sup ( Z , RR* , < ) = +oo ) )
36 34 35 ax-mp 
 |-  ( A. x e. RR E. n e. Z x <_ n <-> sup ( Z , RR* , < ) = +oo )
37 28 36 sylib 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )