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 ℕ$
	smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
Assertion	smndex1iidm	$⊢ I \circ I = I$

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

Metamath Proof Explorer