Metamath Proof Explorer

Theorem uzubioo

Description: The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses uzubioo.1 
|- ( ph -> M e. ZZ )
uzubioo.2 
|- Z = ( ZZ>= ` M )
uzubioo.3 
|- ( ph -> X e. RR )
Assertion uzubioo 
|- ( ph -> E. k e. ( X (,) +oo ) k e. Z )

Proof

Step Hyp Ref Expression
1 uzubioo.1 
 |-  ( ph -> M e. ZZ )
2 uzubioo.2 
 |-  Z = ( ZZ>= ` M )
3 uzubioo.3 
 |-  ( ph -> X e. RR )
4 3 rexrd 
 |-  ( ph -> X e. RR* )
5 pnfxr 
 |-  +oo e. RR*
6 5 a1i 
 |-  ( ph -> +oo e. RR* )
7 3 ceilcld 
 |-  ( ph -> ( |^ ` X ) e. ZZ )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 7 8 zaddcld 
 |-  ( ph -> ( ( |^ ` X ) + 1 ) e. ZZ )
10 9 zred 
 |-  ( ph -> ( ( |^ ` X ) + 1 ) e. RR )
11 1 zred 
 |-  ( ph -> M e. RR )
12 10 11 ifcld 
 |-  ( ph -> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. RR )
13 7 zred 
 |-  ( ph -> ( |^ ` X ) e. RR )
14 3 ceilged 
 |-  ( ph -> X <_ ( |^ ` X ) )
15 13 ltp1d 
 |-  ( ph -> ( |^ ` X ) < ( ( |^ ` X ) + 1 ) )
16 3 13 10 14 15 lelttrd 
 |-  ( ph -> X < ( ( |^ ` X ) + 1 ) )
17 11 10 max2d 
 |-  ( ph -> ( ( |^ ` X ) + 1 ) <_ if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) )
18 3 10 12 16 17 ltletrd 
 |-  ( ph -> X < if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) )
19 12 ltpnfd 
 |-  ( ph -> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) < +oo )
20 4 6 12 18 19 eliood 
 |-  ( ph -> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. ( X (,) +oo ) )
21 9 1 ifcld 
 |-  ( ph -> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. ZZ )
22 max1 
 |-  ( ( M e. RR /\ ( ( |^ ` X ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) )
23 11 10 22 syl2anc 
 |-  ( ph -> M <_ if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) )
24 2 1 21 23 eluzd 
 |-  ( ph -> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. Z )
25 eleq1 
 |-  ( k = if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) -> ( k e. Z <-> if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. Z ) )
26 25 rspcev 
 |-  ( ( if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. ( X (,) +oo ) /\ if ( M <_ ( ( |^ ` X ) + 1 ) , ( ( |^ ` X ) + 1 ) , M ) e. Z ) -> E. k e. ( X (,) +oo ) k e. Z )
27 20 24 26 syl2anc 
 |-  ( ph -> E. k e. ( X (,) +oo ) k e. Z )