Metamath Proof Explorer


Theorem fzo0addelr

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

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

Proof

Step Hyp Ref Expression
1 fzo0addel A0..^CDA+DD..^C+D
2 zcn DD
3 elfzoel2 A0..^CC
4 3 zcnd A0..^CC
5 addcom DCD+C=C+D
6 2 4 5 syl2anr A0..^CDD+C=C+D
7 6 oveq2d A0..^CDD..^D+C=D..^C+D
8 1 7 eleqtrrd A0..^CDA+DD..^D+C