# Metamath Proof Explorer

## Theorem fzosubel

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

Ref Expression
Assertion fzosubel ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}-{D}\in \left({B}-{D}..^{C}-{D}\right)$

### Proof

Step Hyp Ref Expression
1 znegcl ${⊢}{D}\in ℤ\to -{D}\in ℤ$
2 fzoaddel ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge -{D}\in ℤ\right)\to {A}+\left(-{D}\right)\in \left({B}+\left(-{D}\right)..^{C}+\left(-{D}\right)\right)$
3 1 2 sylan2 ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}+\left(-{D}\right)\in \left({B}+\left(-{D}\right)..^{C}+\left(-{D}\right)\right)$
4 elfzoelz ${⊢}{A}\in \left({B}..^{C}\right)\to {A}\in ℤ$
5 4 adantr ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}\in ℤ$
6 5 zcnd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}\in ℂ$
7 simpr ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {D}\in ℤ$
8 7 zcnd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {D}\in ℂ$
9 6 8 negsubd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}+\left(-{D}\right)={A}-{D}$
10 elfzoel1 ${⊢}{A}\in \left({B}..^{C}\right)\to {B}\in ℤ$
11 10 adantr ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {B}\in ℤ$
12 11 zcnd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {B}\in ℂ$
13 12 8 negsubd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {B}+\left(-{D}\right)={B}-{D}$
14 elfzoel2 ${⊢}{A}\in \left({B}..^{C}\right)\to {C}\in ℤ$
15 14 adantr ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {C}\in ℤ$
16 15 zcnd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {C}\in ℂ$
17 16 8 negsubd ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {C}+\left(-{D}\right)={C}-{D}$
18 13 17 oveq12d ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to \left({B}+\left(-{D}\right)..^{C}+\left(-{D}\right)\right)=\left({B}-{D}..^{C}-{D}\right)$
19 3 9 18 3eltr3d ${⊢}\left({A}\in \left({B}..^{C}\right)\wedge {D}\in ℤ\right)\to {A}-{D}\in \left({B}-{D}..^{C}-{D}\right)$