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