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	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \leftrightarrow I = J)$

Proof

Step	Hyp	Ref	Expression
1		elfzo0	$⊢ I \in (0 ..^N) \leftrightarrow (I \in ℕ_{0} \land N \in ℕ \land I < N)$
2		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
3		simplrr	$⊢ ((J \in ℤ \land (I \in ℕ_{0} \land N \in ℕ)) \land S \in ℤ) \to N \in ℕ$
4		nn0z	$⊢ I \in ℕ_{0} \to I \in ℤ$
5	4	ad2antrl	$⊢ (J \in ℤ \land (I \in ℕ_{0} \land N \in ℕ)) \to I \in ℤ$
6		zaddcl	$⊢ (I \in ℤ \land S \in ℤ) \to I + S \in ℤ$
7	5 6	sylan	$⊢ ((J \in ℤ \land (I \in ℕ_{0} \land N \in ℕ)) \land S \in ℤ) \to I + S \in ℤ$
8		zaddcl	$⊢ (J \in ℤ \land S \in ℤ) \to J + S \in ℤ$
9	8	adantlr	$⊢ ((J \in ℤ \land (I \in ℕ_{0} \land N \in ℕ)) \land S \in ℤ) \to J + S \in ℤ$
10	3 7 9	3jca	$⊢ ((J \in ℤ \land (I \in ℕ_{0} \land N \in ℕ)) \land S \in ℤ) \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)$
11	10	exp31	$⊢ J \in ℤ \to ((I \in ℕ_{0} \land N \in ℕ) \to (S \in ℤ \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)))$
12	2 11	syl	$⊢ J \in (0 ..^N) \to ((I \in ℕ_{0} \land N \in ℕ) \to (S \in ℤ \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)))$
13	12	com12	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to (J \in (0 ..^N) \to (S \in ℤ \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)))$
14	13	3adant3	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to (J \in (0 ..^N) \to (S \in ℤ \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)))$
15	1 14	sylbi	$⊢ I \in (0 ..^N) \to (J \in (0 ..^N) \to (S \in ℤ \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)))$
16	15	3imp	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ)$
17		moddvds	$⊢ (N \in ℕ \land I + S \in ℤ \land J + S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \leftrightarrow N ∥ (I + S - (J + S)))$
18	16 17	syl	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \leftrightarrow N ∥ (I + S - (J + S)))$
19		elfzoel2	$⊢ I \in (0 ..^N) \to N \in ℤ$
20		zcn	$⊢ N \in ℤ \to N \in ℂ$
21	20	subid1d	$⊢ N \in ℤ \to N - 0 = N$
22	21	eqcomd	$⊢ N \in ℤ \to N = N - 0$
23	19 22	syl	$⊢ I \in (0 ..^N) \to N = N - 0$
24	23	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to N = N - 0$
25		elfzoelz	$⊢ I \in (0 ..^N) \to I \in ℤ$
26	25	zcnd	$⊢ I \in (0 ..^N) \to I \in ℂ$
27	2	zcnd	$⊢ J \in (0 ..^N) \to J \in ℂ$
28		zcn	$⊢ S \in ℤ \to S \in ℂ$
29		pnpcan2	$⊢ (I \in ℂ \land J \in ℂ \land S \in ℂ) \to I + S - (J + S) = I - J$
30	26 27 28 29	syl3an	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to I + S - (J + S) = I - J$
31	24 30	breq12d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (N ∥ (I + S - (J + S)) \leftrightarrow (N - 0) ∥ (I - J))$
32		fzocongeq	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to ((N - 0) ∥ (I - J) \leftrightarrow I = J)$
33	32	3adant3	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((N - 0) ∥ (I - J) \leftrightarrow I = J)$
34	18 31 33	3bitrd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \leftrightarrow I = J)$

Metamath Proof Explorer

Theorem addmodlteqALT

Proof