Description: Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | fzo0addelr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzo0addel | |
|
2 | zcn | |
|
3 | elfzoel2 | |
|
4 | 3 | zcnd | |
5 | addcom | |
|
6 | 2 4 5 | syl2anr | |
7 | 6 | oveq2d | |
8 | 1 7 | eleqtrrd | |