Metamath Proof Explorer


Theorem smndex1ibas

Description: The modulo function I is an endofunction on NN0 . (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 smndex1ibas I Base M

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 eqid x 0 x mod N = x 0 x mod N
5 nn0z x 0 x
6 2 a1i x 0 N
7 5 6 zmodcld x 0 x mod N 0
8 4 7 fmpti x 0 x mod N : 0 0
9 nn0ex 0 V
10 9 9 elmap x 0 x mod N 0 0 x 0 x mod N : 0 0
11 8 10 mpbir x 0 x mod N 0 0
12 eqid Base M = Base M
13 1 12 efmndbas Base M = 0 0
14 11 3 13 3eltr4i I Base M