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 ∈ ℤ ∧ B ≤ A → C ∈ ℤ ≥ A → C ∈ ℤ ≥ B

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ C ∈ ℤ ≥ A ↔ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C
2 simpll ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → B ∈ ℤ
3 simpr2 ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → C ∈ ℤ
4 zre ⊢ B ∈ ℤ → B ∈ ℝ
5 4 ad2antrr ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → B ∈ ℝ
6 zre ⊢ A ∈ ℤ → A ∈ ℝ
7 6 3ad2ant1 ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → A ∈ ℝ
8 7 adantl ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → A ∈ ℝ
9 zre ⊢ C ∈ ℤ → C ∈ ℝ
10 9 3ad2ant2 ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → C ∈ ℝ
11 10 adantl ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → C ∈ ℝ
12 simplr ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → B ≤ A
13 simpr3 ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → A ≤ C
14 5 8 11 12 13 letrd ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → B ≤ C
15 eluz2 ⊢ C ∈ ℤ ≥ B ↔ B ∈ ℤ ∧ C ∈ ℤ ∧ B ≤ C
16 2 3 14 15 syl3anbrc ⊢ B ∈ ℤ ∧ B ≤ A ∧ A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → C ∈ ℤ ≥ B
17 16 ex ⊢ B ∈ ℤ ∧ B ≤ A → A ∈ ℤ ∧ C ∈ ℤ ∧ A ≤ C → C ∈ ℤ ≥ B
18 1 17 biimtrid ⊢ B ∈ ℤ ∧ B ≤ A → C ∈ ℤ ≥ A → C ∈ ℤ ≥ B