Metamath Proof Explorer

Theorem fzosubel3

Description: Membership in a translated half-open integer range when the original range is zero-based. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzosubel3 ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → A − B ∈ 0 ..^ D

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → A ∈ B ..^ B + D
2 elfzoel1 ⊢ A ∈ B ..^ B + D → B ∈ ℤ
3 2 adantr ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → B ∈ ℤ
4 3 zcnd ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → B ∈ ℂ
5 4 addid1d ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → B + 0 = B
6 5 oveq1d ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → B + 0 ..^ B + D = B ..^ B + D
7 1 6 eleqtrrd ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → A ∈ B + 0 ..^ B + D
8 0zd ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → 0 ∈ ℤ
9 simpr ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → D ∈ ℤ
10 fzosubel2 ⊢ A ∈ B + 0 ..^ B + D ∧ B ∈ ℤ ∧ 0 ∈ ℤ ∧ D ∈ ℤ → A − B ∈ 0 ..^ D
11 7 3 8 9 10 syl13anc ⊢ A ∈ B ..^ B + D ∧ D ∈ ℤ → A − B ∈ 0 ..^ D