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 | ⊢ ( 𝜑 → 𝑀 ∈ ℤ ) | |
| uzinico3.2 | ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) | ||
| Assertion | uzinico3 | ⊢ ( 𝜑 → 𝑍 = ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uzinico3.1 | ⊢ ( 𝜑 → 𝑀 ∈ ℤ ) | |
| 2 | uzinico3.2 | ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) | |
| 3 | 1 | uzidd | ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
| 4 | 3 | uzinico2 | ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑀 [,) +∞ ) ) ) |
| 5 | 2 | a1i | ⊢ ( 𝜑 → 𝑍 = ( ℤ≥ ‘ 𝑀 ) ) |
| 6 | 5 | ineq1d | ⊢ ( 𝜑 → ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑀 [,) +∞ ) ) ) |
| 7 | 5 6 | eqeq12d | ⊢ ( 𝜑 → ( 𝑍 = ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ↔ ( ℤ≥ ‘ 𝑀 ) = ( ( ℤ≥ ‘ 𝑀 ) ∩ ( 𝑀 [,) +∞ ) ) ) ) |
| 8 | 4 7 | mpbird | ⊢ ( 𝜑 → 𝑍 = ( 𝑍 ∩ ( 𝑀 [,) +∞ ) ) ) |