Metamath Proof Explorer


Theorem zmodfz

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion zmodfz ABAmodB0B1

Proof

Step Hyp Ref Expression
1 zmodcl ABAmodB0
2 1 nn0zd ABAmodB
3 1 nn0ge0d AB0AmodB
4 zre AA
5 nnrp BB+
6 modlt AB+AmodB<B
7 4 5 6 syl2an ABAmodB<B
8 0z 0
9 nnz BB
10 9 adantl ABB
11 elfzm11 0BAmodB0B1AmodB0AmodBAmodB<B
12 8 10 11 sylancr ABAmodB0B1AmodB0AmodBAmodB<B
13 2 3 7 12 mpbir3and ABAmodB0B1