# 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 ${⊢}\left({B}\in ℤ\wedge {B}\le {A}\right)\to \left({C}\in {ℤ}_{\ge {A}}\to {C}\in {ℤ}_{\ge {B}}\right)$

### Proof

Step Hyp Ref Expression
1 eluz2 ${⊢}{C}\in {ℤ}_{\ge {A}}↔\left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)$
2 simpll ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {B}\in ℤ$
3 simpr2 ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {C}\in ℤ$
4 zre ${⊢}{B}\in ℤ\to {B}\in ℝ$
5 4 ad2antrr ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {B}\in ℝ$
6 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
7 6 3ad2ant1 ${⊢}\left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\to {A}\in ℝ$
8 7 adantl ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {A}\in ℝ$
9 zre ${⊢}{C}\in ℤ\to {C}\in ℝ$
10 9 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\to {C}\in ℝ$
11 10 adantl ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {C}\in ℝ$
12 simplr ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {B}\le {A}$
13 simpr3 ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {A}\le {C}$
14 5 8 11 12 13 letrd ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {B}\le {C}$
15 eluz2 ${⊢}{C}\in {ℤ}_{\ge {B}}↔\left({B}\in ℤ\wedge {C}\in ℤ\wedge {B}\le {C}\right)$
16 2 3 14 15 syl3anbrc ${⊢}\left(\left({B}\in ℤ\wedge {B}\le {A}\right)\wedge \left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\right)\to {C}\in {ℤ}_{\ge {B}}$
17 16 ex ${⊢}\left({B}\in ℤ\wedge {B}\le {A}\right)\to \left(\left({A}\in ℤ\wedge {C}\in ℤ\wedge {A}\le {C}\right)\to {C}\in {ℤ}_{\ge {B}}\right)$
18 1 17 syl5bi ${⊢}\left({B}\in ℤ\wedge {B}\le {A}\right)\to \left({C}\in {ℤ}_{\ge {A}}\to {C}\in {ℤ}_{\ge {B}}\right)$