Metamath Proof Explorer


Theorem zmodid2

Description: Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion zmodid2 M N M mod N = M M 0 N 1

Proof

Step Hyp Ref Expression
1 zre M M
2 nnrp N N +
3 modid2 M N + M mod N = M 0 M M < N
4 1 2 3 syl2an M N M mod N = M 0 M M < N
5 nnz N N
6 0z 0
7 elfzm11 0 N M 0 N 1 M 0 M M < N
8 6 7 mpan N M 0 N 1 M 0 M M < N
9 3anass M 0 M M < N M 0 M M < N
10 8 9 bitrdi N M 0 N 1 M 0 M M < N
11 5 10 syl N M 0 N 1 M 0 M M < N
12 ibar M 0 M M < N M 0 M M < N
13 12 bicomd M M 0 M M < N 0 M M < N
14 11 13 sylan9bbr M N M 0 N 1 0 M M < N
15 4 14 bitr4d M N M mod N = M M 0 N 1