Metamath Proof Explorer


Theorem uzinico3

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 +∞