This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴 ) → ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐵 ) ) )

Proof

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