modaddid

Description: The sums of two nonnegative integers less than the modulus and an integer are equal iff the two nonnegative integers are equal. (Contributed by AV, 14-Nov-2025)

		Ref	Expression
	Hypothesis	modaddid.i	$⊢ I = (0 ..^N)$
	Assertion	modaddid	$⊢ (N \in ℤ_{\geq 3} \land (X \in I \land Y \in I) \land K \in ℤ) \to ((X + K) \mod N = (Y + K) \mod N \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		modaddid.i	$⊢ I = (0 ..^N)$
2		elfzoelz	$⊢ X \in (0 ..^N) \to X \in ℤ$
3	2	zred	$⊢ X \in (0 ..^N) \to X \in ℝ$
4	3 1	eleq2s	$⊢ X \in I \to X \in ℝ$
5		elfzoelz	$⊢ Y \in (0 ..^N) \to Y \in ℤ$
6	5	zred	$⊢ Y \in (0 ..^N) \to Y \in ℝ$
7	6 1	eleq2s	$⊢ Y \in I \to Y \in ℝ$
8	4 7	anim12i	$⊢ (X \in I \land Y \in I) \to (X \in ℝ \land Y \in ℝ)$
9	8	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (X \in I \land Y \in I) \land K \in ℤ) \to (X \in ℝ \land Y \in ℝ)$
10		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
11	10	nnrpd	$⊢ N \in ℤ_{\geq 3} \to N \in ℝ^{+}$
12		zre	$⊢ K \in ℤ \to K \in ℝ$
13	11 12	anim12ci	$⊢ (N \in ℤ_{\geq 3} \land K \in ℤ) \to (K \in ℝ \land N \in ℝ^{+})$
14		modaddb	$⊢ ((X \in ℝ \land Y \in ℝ) \land (K \in ℝ \land N \in ℝ^{+})) \to (X \mod N = Y \mod N \leftrightarrow (X + K) \mod N = (Y + K) \mod N)$
15	9 13 14	3imp3i2an	$⊢ (N \in ℤ_{\geq 3} \land (X \in I \land Y \in I) \land K \in ℤ) \to (X \mod N = Y \mod N \leftrightarrow (X + K) \mod N = (Y + K) \mod N)$
16		zmodidfzoimp	$⊢ X \in (0 ..^N) \to X \mod N = X$
17	16 1	eleq2s	$⊢ X \in I \to X \mod N = X$
18		zmodidfzoimp	$⊢ Y \in (0 ..^N) \to Y \mod N = Y$
19	18 1	eleq2s	$⊢ Y \in I \to Y \mod N = Y$
20	17 19	eqeqan12d	$⊢ (X \in I \land Y \in I) \to (X \mod N = Y \mod N \leftrightarrow X = Y)$
21	20	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (X \in I \land Y \in I) \land K \in ℤ) \to (X \mod N = Y \mod N \leftrightarrow X = Y)$
22	15 21	bitr3d	$⊢ (N \in ℤ_{\geq 3} \land (X \in I \land Y \in I) \land K \in ℤ) \to ((X + K) \mod N = (Y + K) \mod N \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem modaddid

Proof