Metamath Proof Explorer

Theorem fzoaddel2

Description: Translate membership in a shifted-down half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzoaddel2 ⊢ A ∈ 0 ..^ B − C ∧ B ∈ ℤ ∧ C ∈ ℤ → A + C ∈ C ..^ B

Proof

Step Hyp Ref Expression
1 fzoaddel ⊢ A ∈ 0 ..^ B − C ∧ C ∈ ℤ → A + C ∈ 0 + C ..^ B - C + C
2 1 3adant2 ⊢ A ∈ 0 ..^ B − C ∧ B ∈ ℤ ∧ C ∈ ℤ → A + C ∈ 0 + C ..^ B - C + C
3 zcn ⊢ B ∈ ℤ → B ∈ ℂ
4 zcn ⊢ C ∈ ℤ → C ∈ ℂ
5 addlid ⊢ C ∈ ℂ → 0 + C = C
6 5 adantl ⊢ B ∈ ℂ ∧ C ∈ ℂ → 0 + C = C
7 npcan ⊢ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = B
8 6 7 oveq12d ⊢ B ∈ ℂ ∧ C ∈ ℂ → 0 + C ..^ B - C + C = C ..^ B
9 3 4 8 syl2an ⊢ B ∈ ℤ ∧ C ∈ ℤ → 0 + C ..^ B - C + C = C ..^ B
10 9 3adant1 ⊢ A ∈ 0 ..^ B − C ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 + C ..^ B - C + C = C ..^ B
11 2 10 eleqtrd ⊢ A ∈ 0 ..^ B − C ∧ B ∈ ℤ ∧ C ∈ ℤ → A + C ∈ C ..^ B