Metamath Proof Explorer


Theorem smndex1iidm

Description: The modulo function I is idempotent. (Contributed by AV, 12-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
smndex1ibas.n N
smndex1ibas.i I = x 0 x mod N
Assertion smndex1iidm I I = I

Proof

Step Hyp Ref Expression
1 smndex1ibas.m Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2 smndex1ibas.n N
3 smndex1ibas.i I = x 0 x mod N
4 nn0re y 0 y
5 nnrp N N +
6 2 5 ax-mp N +
7 modabs2 y N + y mod N mod N = y mod N
8 4 6 7 sylancl y 0 y mod N mod N = y mod N
9 8 eqcomd y 0 y mod N = y mod N mod N
10 9 mpteq2ia y 0 y mod N = y 0 y mod N mod N
11 oveq1 x = y x mod N = y mod N
12 11 cbvmptv x 0 x mod N = y 0 y mod N
13 3 12 eqtri I = y 0 y mod N
14 nn0z y 0 y
15 14 anim2i N y 0 N y
16 15 ancomd N y 0 y N
17 zmodcl y N y mod N 0
18 16 17 syl N y 0 y mod N 0
19 13 a1i N I = y 0 y mod N
20 3 a1i N I = x 0 x mod N
21 oveq1 x = y mod N x mod N = y mod N mod N
22 18 19 20 21 fmptco N I I = y 0 y mod N mod N
23 2 22 ax-mp I I = y 0 y mod N mod N
24 10 13 23 3eqtr4ri I I = I