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\in \mathbb{N}$$
	smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
Assertion	smndex1iidm	$$⊢I\circ 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\in \mathbb{N}$$
3		smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
4		nn0re	$$⊢y\in {\mathbb{N}}_0\to y\in ℝ$$
5		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
6	2 5	ax-mp	$$⊢N\in {ℝ}^{+}$$
7		modabs2	$$⊢\left(y\in ℝ\wedge N\in {ℝ}^{+}\right)\to \left(y\mathrm{mod}N\right)\mathrm{mod}N=y\mathrm{mod}N$$
8	4 6 7	sylancl	$$⊢y\in {\mathbb{N}}_0\to \left(y\mathrm{mod}N\right)\mathrm{mod}N=y\mathrm{mod}N$$
9	8	eqcomd	$$⊢y\in {\mathbb{N}}_0\to y\mathrm{mod}N=\left(y\mathrm{mod}N\right)\mathrm{mod}N$$
10	9	mpteq2ia	$$⊢\left(y\in {\mathbb{N}}_0⟼y\mathrm{mod}N\right)=\left(y\in {\mathbb{N}}_0⟼\left(y\mathrm{mod}N\right)\mathrm{mod}N\right)$$
11		oveq1	$$⊢x=y\to x\mathrm{mod}N=y\mathrm{mod}N$$
12	11	cbvmptv	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)=\left(y\in {\mathbb{N}}_0⟼y\mathrm{mod}N\right)$$
13	3 12	eqtri	$$⊢I=\left(y\in {\mathbb{N}}_0⟼y\mathrm{mod}N\right)$$
14		nn0z	$$⊢y\in {\mathbb{N}}_0\to y\in \mathbb{Z}$$
15	14	anim2i	$$⊢\left(N\in \mathbb{N}\wedge y\in {\mathbb{N}}_0\right)\to \left(N\in \mathbb{N}\wedge y\in \mathbb{Z}\right)$$
16	15	ancomd	$$⊢\left(N\in \mathbb{N}\wedge y\in {\mathbb{N}}_0\right)\to \left(y\in \mathbb{Z}\wedge N\in \mathbb{N}\right)$$
17		zmodcl	$$⊢\left(y\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to y\mathrm{mod}N\in {\mathbb{N}}_0$$
18	16 17	syl	$$⊢\left(N\in \mathbb{N}\wedge y\in {\mathbb{N}}_0\right)\to y\mathrm{mod}N\in {\mathbb{N}}_0$$
19	13	a1i	$$⊢N\in \mathbb{N}\to I=\left(y\in {\mathbb{N}}_0⟼y\mathrm{mod}N\right)$$
20	3	a1i	$$⊢N\in \mathbb{N}\to I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
21		oveq1	$$⊢x=y\mathrm{mod}N\to x\mathrm{mod}N=\left(y\mathrm{mod}N\right)\mathrm{mod}N$$
22	18 19 20 21	fmptco	$$⊢N\in \mathbb{N}\to I\circ I=\left(y\in {\mathbb{N}}_0⟼\left(y\mathrm{mod}N\right)\mathrm{mod}N\right)$$
23	2 22	ax-mp	$$⊢I\circ I=\left(y\in {\mathbb{N}}_0⟼\left(y\mathrm{mod}N\right)\mathrm{mod}N\right)$$
24	10 13 23	3eqtr4ri	$$⊢I\circ I=I$$