This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) ↔ 𝑋 = 𝑌 ) )