Metamath Proof Explorer

Theorem fzocatel

Description: Translate membership in a half-open integer range. (Contributed by Thierry Arnoux, 28-Sep-2018)

Ref Expression
Assertion fzocatel ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → A − B ∈ 0 ..^ C

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A ∈ 0 ..^ B
2 fzospliti ⊢ A ∈ 0 ..^ B + C ∧ B ∈ ℤ → A ∈ 0 ..^ B ∨ A ∈ B ..^ B + C
3 2 ad2ant2r ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ 0 ..^ B ∨ A ∈ B ..^ B + C
4 3 ord ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A ∈ 0 ..^ B → A ∈ B ..^ B + C
5 1 4 mpd ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ B ..^ B + C
6 simprl ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℤ
7 fzosubel ⊢ A ∈ B ..^ B + C ∧ B ∈ ℤ → A − B ∈ B − B ..^ B + C - B
8 5 6 7 syl2anc ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → A − B ∈ B − B ..^ B + C - B
9 zcn ⊢ B ∈ ℤ → B ∈ ℂ
10 9 subidd ⊢ B ∈ ℤ → B − B = 0
11 6 10 syl ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → B − B = 0
12 6 zcnd ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℂ
13 simprr ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → C ∈ ℤ
14 13 zcnd ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → C ∈ ℂ
15 12 14 pncan2d ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → B + C - B = C
16 11 15 oveq12d ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → B − B ..^ B + C - B = 0 ..^ C
17 8 16 eleqtrd ⊢ A ∈ 0 ..^ B + C ∧ ¬ A ∈ 0 ..^ B ∧ B ∈ ℤ ∧ C ∈ ℤ → A − B ∈ 0 ..^ C