Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
uzinico3
Metamath Proof Explorer
Description: An upper interval of integers doesn't change when it's intersected with
a left-closed, unbounded above interval, with the same lower bound.
(Contributed by Glauco Siliprandi , 2-Jan-2022)
Ref
Expression
Hypotheses
uzinico3.1
⊢ φ → M ∈ ℤ
uzinico3.2
⊢ Z = ℤ ≥ M
Assertion
uzinico3
⊢ φ → Z = Z ∩ M +∞
Proof
Step
Hyp
Ref
Expression
1
uzinico3.1
⊢ φ → M ∈ ℤ
2
uzinico3.2
⊢ Z = ℤ ≥ M
3
1
uzidd
⊢ φ → M ∈ ℤ ≥ M
4
3
uzinico2
⊢ φ → ℤ ≥ M = ℤ ≥ M ∩ M +∞
5
2
a1i
⊢ φ → Z = ℤ ≥ M
6
5
ineq1d
⊢ φ → Z ∩ M +∞ = ℤ ≥ M ∩ M +∞
7
5 6
eqeq12d
⊢ φ → Z = Z ∩ M +∞ ↔ ℤ ≥ M = ℤ ≥ M ∩ M +∞
8
4 7
mpbird
⊢ φ → Z = Z ∩ M +∞