# 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 ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {A}-{B}\in \left(0..^{D}\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {A}\in \left({B}..^{B}+{D}\right)$
2 elfzoel1 ${⊢}{A}\in \left({B}..^{B}+{D}\right)\to {B}\in ℤ$
3 2 adantr ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {B}\in ℤ$
4 3 zcnd ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {B}\in ℂ$
5 4 addid1d ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {B}+0={B}$
6 5 oveq1d ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to \left({B}+0..^{B}+{D}\right)=\left({B}..^{B}+{D}\right)$
7 1 6 eleqtrrd ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {A}\in \left({B}+0..^{B}+{D}\right)$
8 0zd ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to 0\in ℤ$
9 simpr ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {D}\in ℤ$
10 fzosubel2 ${⊢}\left({A}\in \left({B}+0..^{B}+{D}\right)\wedge \left({B}\in ℤ\wedge 0\in ℤ\wedge {D}\in ℤ\right)\right)\to {A}-{B}\in \left(0..^{D}\right)$
11 7 3 8 9 10 syl13anc ${⊢}\left({A}\in \left({B}..^{B}+{D}\right)\wedge {D}\in ℤ\right)\to {A}-{B}\in \left(0..^{D}\right)$