Description: Translate membership in a 0-based half-open integer range. (Contributed by AV, 30-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | fzo0addel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzoaddel | |
|
2 | zcn | |
|
3 | addlid | |
|
4 | 3 | eqcomd | |
5 | 2 4 | syl | |
6 | 5 | adantl | |
7 | 6 | oveq1d | |
8 | 1 7 | eleqtrrd | |