Theorem addmodlteqALT

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq based on the "divides" relation. (Contributed by AV, 14-Mar-2021) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	addmodlteqALT	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) )
2		elfzoelz	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
3		simplrr	⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → 𝑁 ∈ ℕ )
4		nn0z	⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
5	4	ad2antrl	⊢ ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝐼 ∈ ℤ )
6		zaddcl	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝐼 + 𝑆 ) ∈ ℤ )
7	5 6	sylan	⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝐼 + 𝑆 ) ∈ ℤ )
8		zaddcl	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝐽 + 𝑆 ) ∈ ℤ )
9	8	adantlr	⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝐽 + 𝑆 ) ∈ ℤ )
10	3 7 9	3jca	⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) )
11	10	exp31	⊢ ( 𝐽 ∈ ℤ → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
12	2 11	syl	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
13	12	com12	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
14	13	3adant3	⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
15	1 14	sylbi	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
16	15	3imp	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) )
17		moddvds	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ) )
18	16 17	syl	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ) )
19		elfzoel2	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
20		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
21	20	subid1d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 )
22	21	eqcomd	⊢ ( 𝑁 ∈ ℤ → 𝑁 = ( 𝑁 − 0 ) )
23	19 22	syl	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝑁 = ( 𝑁 − 0 ) )
24	23	3ad2ant1	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → 𝑁 = ( 𝑁 − 0 ) )
25		elfzoelz	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝐼 ∈ ℤ )
26	25	zcnd	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝐼 ∈ ℂ )
27	2	zcnd	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℂ )
28		zcn	⊢ ( 𝑆 ∈ ℤ → 𝑆 ∈ ℂ )
29		pnpcan2	⊢ ( ( 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) = ( 𝐼 − 𝐽 ) )
30	26 27 28 29	syl3an	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) = ( 𝐼 − 𝐽 ) )
31	24 30	breq12d	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ↔ ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ) )
32		fzocongeq	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ↔ 𝐼 = 𝐽 ) )
33	32	3adant3	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ↔ 𝐼 = 𝐽 ) )
34	18 31 33	3bitrd	⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )