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 
|- I = ( 0 ..^ N )
Assertion modaddid 
|- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. I /\ Y e. I ) /\ K e. ZZ ) -> ( ( ( X + K ) mod N ) = ( ( Y + K ) mod N ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 modaddid.i 
 |-  I = ( 0 ..^ N )
2 elfzoelz 
 |-  ( X e. ( 0 ..^ N ) -> X e. ZZ )
3 2 zred 
 |-  ( X e. ( 0 ..^ N ) -> X e. RR )
4 3 1 eleq2s 
 |-  ( X e. I -> X e. RR )
5 elfzoelz 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. ZZ )
6 5 zred 
 |-  ( Y e. ( 0 ..^ N ) -> Y e. RR )
7 6 1 eleq2s 
 |-  ( Y e. I -> Y e. RR )
8 4 7 anim12i 
 |-  ( ( X e. I /\ Y e. I ) -> ( X e. RR /\ Y e. RR ) )
9 8 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. I /\ Y e. I ) /\ K e. ZZ ) -> ( X e. RR /\ Y e. RR ) )
10 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
11 10 nnrpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR+ )
12 zre 
 |-  ( K e. ZZ -> K e. RR )
13 11 12 anim12ci 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. ZZ ) -> ( K e. RR /\ N e. RR+ ) )
14 modaddb 
 |-  ( ( ( X e. RR /\ Y e. RR ) /\ ( K e. RR /\ N e. RR+ ) ) -> ( ( X mod N ) = ( Y mod N ) <-> ( ( X + K ) mod N ) = ( ( Y + K ) mod N ) ) )
15 9 13 14 3imp3i2an 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. I /\ Y e. I ) /\ K e. ZZ ) -> ( ( X mod N ) = ( Y mod N ) <-> ( ( X + K ) mod N ) = ( ( Y + K ) mod N ) ) )
16 zmodidfzoimp 
 |-  ( X e. ( 0 ..^ N ) -> ( X mod N ) = X )
17 16 1 eleq2s 
 |-  ( X e. I -> ( X mod N ) = X )
18 zmodidfzoimp 
 |-  ( Y e. ( 0 ..^ N ) -> ( Y mod N ) = Y )
19 18 1 eleq2s 
 |-  ( Y e. I -> ( Y mod N ) = Y )
20 17 19 eqeqan12d 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( X mod N ) = ( Y mod N ) <-> X = Y ) )
21 20 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. I /\ Y e. I ) /\ K e. ZZ ) -> ( ( X mod N ) = ( Y mod N ) <-> X = Y ) )
22 15 21 bitr3d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. I /\ Y e. I ) /\ K e. ZZ ) -> ( ( ( X + K ) mod N ) = ( ( Y + K ) mod N ) <-> X = Y ) )