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 ) )