Metamath Proof Explorer


Theorem fzo0addel

Description: Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020)

Ref Expression
Assertion fzo0addel A0..^CDA+DD..^C+D

Proof

Step Hyp Ref Expression
1 fzoaddel A0..^CDA+D0+D..^C+D
2 zcn DD
3 addlid D0+D=D
4 3 eqcomd DD=0+D
5 2 4 syl DD=0+D
6 5 adantl A0..^CDD=0+D
7 6 oveq1d A0..^CDD..^C+D=0+D..^C+D
8 1 7 eleqtrrd A0..^CDA+DD..^C+D