Metamath Proof Explorer

Theorem eluzuzle

Description: An integer in an upper set of integers is an element of an upper set of integers with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018)

Ref Expression
Assertion eluzuzle 
|- ( ( B e. ZZ /\ B <_ A ) -> ( C e. ( ZZ>= ` A ) -> C e. ( ZZ>= ` B ) ) )

Proof

Step Hyp Ref Expression
1 eluz2 
 |-  ( C e. ( ZZ>= ` A ) <-> ( A e. ZZ /\ C e. ZZ /\ A <_ C ) )
2 simpll 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> B e. ZZ )
3 simpr2 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> C e. ZZ )
4 zre 
 |-  ( B e. ZZ -> B e. RR )
5 4 ad2antrr 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> B e. RR )
6 zre 
 |-  ( A e. ZZ -> A e. RR )
7 6 3ad2ant1 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ A <_ C ) -> A e. RR )
8 7 adantl 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> A e. RR )
9 zre 
 |-  ( C e. ZZ -> C e. RR )
10 9 3ad2ant2 
 |-  ( ( A e. ZZ /\ C e. ZZ /\ A <_ C ) -> C e. RR )
11 10 adantl 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> C e. RR )
12 simplr 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> B <_ A )
13 simpr3 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> A <_ C )
14 5 8 11 12 13 letrd 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> B <_ C )
15 eluz2 
 |-  ( C e. ( ZZ>= ` B ) <-> ( B e. ZZ /\ C e. ZZ /\ B <_ C ) )
16 2 3 14 15 syl3anbrc 
 |-  ( ( ( B e. ZZ /\ B <_ A ) /\ ( A e. ZZ /\ C e. ZZ /\ A <_ C ) ) -> C e. ( ZZ>= ` B ) )
17 16 ex 
 |-  ( ( B e. ZZ /\ B <_ A ) -> ( ( A e. ZZ /\ C e. ZZ /\ A <_ C ) -> C e. ( ZZ>= ` B ) ) )
18 1 17 biimtrid 
 |-  ( ( B e. ZZ /\ B <_ A ) -> ( C e. ( ZZ>= ` A ) -> C e. ( ZZ>= ` B ) ) )