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 ⊢ A ∈ B + C ..^ B + D ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ → A − B ∈ C ..^ D

Proof

Step Hyp Ref Expression
1 fzosubel ⊢ A ∈ B + C ..^ B + D ∧ B ∈ ℤ → A − B ∈ B + C - B ..^ B + D - B
2 1 3ad2antr1 ⊢ A ∈ B + C ..^ B + D ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ → A − B ∈ B + C - B ..^ B + D - B
3 zcn ⊢ B ∈ ℤ → B ∈ ℂ
4 zcn ⊢ C ∈ ℤ → C ∈ ℂ
5 zcn ⊢ D ∈ ℤ → D ∈ ℂ
6 pncan2 ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C - B = C
7 6 3adant3 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + C - B = C
8 pncan2 ⊢ B ∈ ℂ ∧ D ∈ ℂ → B + D - B = D
9 8 3adant2 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + D - B = D
10 7 9 oveq12d ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B + C - B ..^ B + D - B = C ..^ D
11 3 4 5 10 syl3an ⊢ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ → B + C - B ..^ B + D - B = C ..^ D
12 11 adantl ⊢ A ∈ B + C ..^ B + D ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ → B + C - B ..^ B + D - B = C ..^ D
13 2 12 eleqtrd ⊢ A ∈ B + C ..^ B + D ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ → A − B ∈ C ..^ D