# Metamath Proof Explorer

## Theorem fzosubel2

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

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

### Proof

Step Hyp Ref Expression
1 fzosubel ${⊢}\left({A}\in \left({B}+{C}..^{B}+{D}\right)\wedge {B}\in ℤ\right)\to {A}-{B}\in \left({B}+{C}-{B}..^{B}+{D}-{B}\right)$
2 1 3ad2antr1 ${⊢}\left({A}\in \left({B}+{C}..^{B}+{D}\right)\wedge \left({B}\in ℤ\wedge {C}\in ℤ\wedge {D}\in ℤ\right)\right)\to {A}-{B}\in \left({B}+{C}-{B}..^{B}+{D}-{B}\right)$
3 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
4 zcn ${⊢}{C}\in ℤ\to {C}\in ℂ$
5 zcn ${⊢}{D}\in ℤ\to {D}\in ℂ$
6 pncan2 ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}+{C}-{B}={C}$
7 6 3adant3 ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {D}\in ℂ\right)\to {B}+{C}-{B}={C}$
8 pncan2 ${⊢}\left({B}\in ℂ\wedge {D}\in ℂ\right)\to {B}+{D}-{B}={D}$
9 8 3adant2 ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {D}\in ℂ\right)\to {B}+{D}-{B}={D}$
10 7 9 oveq12d ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {D}\in ℂ\right)\to \left({B}+{C}-{B}..^{B}+{D}-{B}\right)=\left({C}..^{D}\right)$
11 3 4 5 10 syl3an ${⊢}\left({B}\in ℤ\wedge {C}\in ℤ\wedge {D}\in ℤ\right)\to \left({B}+{C}-{B}..^{B}+{D}-{B}\right)=\left({C}..^{D}\right)$
12 11 adantl ${⊢}\left({A}\in \left({B}+{C}..^{B}+{D}\right)\wedge \left({B}\in ℤ\wedge {C}\in ℤ\wedge {D}\in ℤ\right)\right)\to \left({B}+{C}-{B}..^{B}+{D}-{B}\right)=\left({C}..^{D}\right)$
13 2 12 eleqtrd ${⊢}\left({A}\in \left({B}+{C}..^{B}+{D}\right)\wedge \left({B}\in ℤ\wedge {C}\in ℤ\wedge {D}\in ℤ\right)\right)\to {A}-{B}\in \left({C}..^{D}\right)$