Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | zmodfz | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zmodcl | |
|
2 | 1 | nn0zd | |
3 | 1 | nn0ge0d | |
4 | zre | |
|
5 | nnrp | |
|
6 | modlt | |
|
7 | 4 5 6 | syl2an | |
8 | 0z | |
|
9 | nnz | |
|
10 | 9 | adantl | |
11 | elfzm11 | |
|
12 | 8 10 11 | sylancr | |
13 | 2 3 7 12 | mpbir3and | |