Theorem 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	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	modaddid	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑋 + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		modaddid.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
2		elfzoelz	⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ℤ )
3	2	zred	⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → 𝑋 ∈ ℝ )
4	3 1	eleq2s	⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ℝ )
5		elfzoelz	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℤ )
6	5	zred	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → 𝑌 ∈ ℝ )
7	6 1	eleq2s	⊢ ( 𝑌 ∈ 𝐼 → 𝑌 ∈ ℝ )
8	4 7	anim12i	⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) )
9	8	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) )
10		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
11	10	nnrpd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ+ )
12		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
13	11 12	anim12ci	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
14		modaddb	⊢ ( ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) → ( ( 𝑋 mod 𝑁 ) = ( 𝑌 mod 𝑁 ) ↔ ( ( 𝑋 + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ) )
15	9 13 14	3imp3i2an	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑋 mod 𝑁 ) = ( 𝑌 mod 𝑁 ) ↔ ( ( 𝑋 + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ) )
16		zmodidfzoimp	⊢ ( 𝑋 ∈ ( 0 ..^ 𝑁 ) → ( 𝑋 mod 𝑁 ) = 𝑋 )
17	16 1	eleq2s	⊢ ( 𝑋 ∈ 𝐼 → ( 𝑋 mod 𝑁 ) = 𝑋 )
18		zmodidfzoimp	⊢ ( 𝑌 ∈ ( 0 ..^ 𝑁 ) → ( 𝑌 mod 𝑁 ) = 𝑌 )
19	18 1	eleq2s	⊢ ( 𝑌 ∈ 𝐼 → ( 𝑌 mod 𝑁 ) = 𝑌 )
20	17 19	eqeqan12d	⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑋 mod 𝑁 ) = ( 𝑌 mod 𝑁 ) ↔ 𝑋 = 𝑌 ) )
21	20	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝑋 mod 𝑁 ) = ( 𝑌 mod 𝑁 ) ↔ 𝑋 = 𝑌 ) )
22	15 21	bitr3d	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝑋 + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ↔ 𝑋 = 𝑌 ) )