Metamath Proof Explorer

Theorem fzo0addel

Description: Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020)

Ref Expression
Assertion fzo0addel ⊢ A ∈ 0 ..^ C ∧ D ∈ ℤ → A + D ∈ D ..^ C + D

Proof

Step Hyp Ref Expression
1 fzoaddel ⊢ A ∈ 0 ..^ C ∧ D ∈ ℤ → A + D ∈ 0 + D ..^ C + D
2 zcn ⊢ D ∈ ℤ → D ∈ ℂ
3 addid2 ⊢ D ∈ ℂ → 0 + D = D
4 3 eqcomd ⊢ D ∈ ℂ → D = 0 + D
5 2 4 syl ⊢ D ∈ ℤ → D = 0 + D
6 5 adantl ⊢ A ∈ 0 ..^ C ∧ D ∈ ℤ → D = 0 + D
7 6 oveq1d ⊢ A ∈ 0 ..^ C ∧ D ∈ ℤ → D ..^ C + D = 0 + D ..^ C + D
8 1 7 eleqtrrd ⊢ A ∈ 0 ..^ C ∧ D ∈ ℤ → A + D ∈ D ..^ C + D