addmodlteq

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. A much shorter proof exists if the "divides" relation || can be used, see addmodlteqALT . (Contributed by AV, 20-Mar-2021)

		Ref	Expression
	Assertion	addmodlteq	$⊢ (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		elfzoelz	$⊢ I \in (0 ..^N) \to I \in ℤ$
2	1	zred	$⊢ I \in (0 ..^N) \to I \in ℝ$
3	2	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to I \in ℝ$
4		simp3	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to S \in ℤ$
5	4	zred	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to S \in ℝ$
6		elfzo0	$⊢ I \in (0 ..^N) \leftrightarrow (I \in ℕ_{0} \land N \in ℕ \land I < N)$
7	6	simp2bi	$⊢ I \in (0 ..^N) \to N \in ℕ$
8	7	nnrpd	$⊢ I \in (0 ..^N) \to N \in ℝ^{+}$
9	8	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to N \in ℝ^{+}$
10		modaddmod	$⊢ (I \in ℝ \land S \in ℝ \land N \in ℝ^{+}) \to ((I \mod N) + S) \mod N = (I + S) \mod N$
11	3 5 9 10	syl3anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I \mod N) + S) \mod N = (I + S) \mod N$
12	11	eqcomd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (I + S) \mod N = ((I \mod N) + S) \mod N$
13		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
14	13	zred	$⊢ J \in (0 ..^N) \to J \in ℝ$
15	14	3ad2ant2	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to J \in ℝ$
16		modaddmod	$⊢ (J \in ℝ \land S \in ℝ \land N \in ℝ^{+}) \to ((J \mod N) + S) \mod N = (J + S) \mod N$
17	15 5 9 16	syl3anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((J \mod N) + S) \mod N = (J + S) \mod N$
18	17	eqcomd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (J + S) \mod N = ((J \mod N) + S) \mod N$
19	12 18	eqeq12d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \leftrightarrow ((I \mod N) + S) \mod N = ((J \mod N) + S) \mod N)$
20		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
21		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
22	20 21	anim12i	$⊢ (I \in ℕ_{0} \land N \in ℕ) \to (I \in ℝ \land N \in ℝ^{+})$
23	22	3adant3	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to (I \in ℝ \land N \in ℝ^{+})$
24		modcl	$⊢ (I \in ℝ \land N \in ℝ^{+}) \to I \mod N \in ℝ$
25	23 24	syl	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to I \mod N \in ℝ$
26	6 25	sylbi	$⊢ I \in (0 ..^N) \to I \mod N \in ℝ$
27	26	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to I \mod N \in ℝ$
28	27 5	readdcld	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (I \mod N) + S \in ℝ$
29		modcl	$⊢ ((I \mod N) + S \in ℝ \land N \in ℝ^{+}) \to ((I \mod N) + S) \mod N \in ℝ$
30	29	recnd	$⊢ ((I \mod N) + S \in ℝ \land N \in ℝ^{+}) \to ((I \mod N) + S) \mod N \in ℂ$
31	28 9 30	syl2anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I \mod N) + S) \mod N \in ℂ$
32		elfzo0	$⊢ J \in (0 ..^N) \leftrightarrow (J \in ℕ_{0} \land N \in ℕ \land J < N)$
33		nn0re	$⊢ J \in ℕ_{0} \to J \in ℝ$
34	33 21	anim12i	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (J \in ℝ \land N \in ℝ^{+})$
35	34	3adant3	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J \in ℝ \land N \in ℝ^{+})$
36		modcl	$⊢ (J \in ℝ \land N \in ℝ^{+}) \to J \mod N \in ℝ$
37	35 36	syl	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \mod N \in ℝ$
38	32 37	sylbi	$⊢ J \in (0 ..^N) \to J \mod N \in ℝ$
39	38	3ad2ant2	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to J \mod N \in ℝ$
40	39 5	readdcld	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (J \mod N) + S \in ℝ$
41		modcl	$⊢ ((J \mod N) + S \in ℝ \land N \in ℝ^{+}) \to ((J \mod N) + S) \mod N \in ℝ$
42	41	recnd	$⊢ ((J \mod N) + S \in ℝ \land N \in ℝ^{+}) \to ((J \mod N) + S) \mod N \in ℂ$
43	40 9 42	syl2anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((J \mod N) + S) \mod N \in ℂ$
44	31 43	subeq0ad	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N) = 0 \leftrightarrow ((I \mod N) + S) \mod N = ((J \mod N) + S) \mod N)$
45		oveq1	$⊢ (((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N) = 0 \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = 0 \mod N$
46		modsubmodmod	$⊢ ((I \mod N) + S \in ℝ \land (J \mod N) + S \in ℝ \land N \in ℝ^{+}) \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = ((I \mod N) + S - ((J \mod N) + S)) \mod N$
47	28 40 9 46	syl3anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = ((I \mod N) + S - ((J \mod N) + S)) \mod N$
48	26	recnd	$⊢ I \in (0 ..^N) \to I \mod N \in ℂ$
49	48	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to I \mod N \in ℂ$
50	38	recnd	$⊢ J \in (0 ..^N) \to J \mod N \in ℂ$
51	50	3ad2ant2	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to J \mod N \in ℂ$
52	4	zcnd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to S \in ℂ$
53	49 51 52	pnpcan2d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (I \mod N) + S - ((J \mod N) + S) = (I \mod N) - (J \mod N)$
54	53	oveq1d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I \mod N) + S - ((J \mod N) + S)) \mod N = ((I \mod N) - (J \mod N)) \mod N$
55	47 54	eqtrd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = ((I \mod N) - (J \mod N)) \mod N$
56	32	simp2bi	$⊢ J \in (0 ..^N) \to N \in ℕ$
57	56	nnrpd	$⊢ J \in (0 ..^N) \to N \in ℝ^{+}$
58		0mod	$⊢ N \in ℝ^{+} \to 0 \mod N = 0$
59	57 58	syl	$⊢ J \in (0 ..^N) \to 0 \mod N = 0$
60	59	3ad2ant2	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to 0 \mod N = 0$
61	55 60	eqeq12d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = 0 \mod N \leftrightarrow ((I \mod N) - (J \mod N)) \mod N = 0)$
62		zmodidfzoimp	$⊢ I \in (0 ..^N) \to I \mod N = I$
63	62	3ad2ant1	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to I \mod N = I$
64		zmodidfzoimp	$⊢ J \in (0 ..^N) \to J \mod N = J$
65	64	3ad2ant2	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to J \mod N = J$
66	63 65	oveq12d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (I \mod N) - (J \mod N) = I - J$
67	66	oveq1d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I \mod N) - (J \mod N)) \mod N = (I - J) \mod N$
68	67	eqeq1d	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (((I \mod N) - (J \mod N)) \mod N = 0 \leftrightarrow (I - J) \mod N = 0)$
69		zsubcl	$⊢ (I \in ℤ \land J \in ℤ) \to I - J \in ℤ$
70	1 13 69	syl2an	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to I - J \in ℤ$
71	70	zred	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to I - J \in ℝ$
72	8	adantr	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to N \in ℝ^{+}$
73		mod0	$⊢ (I - J \in ℝ \land N \in ℝ^{+}) \to ((I - J) \mod N = 0 \leftrightarrow \frac{I - J}{N} \in ℤ)$
74	71 72 73	syl2anc	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to ((I - J) \mod N = 0 \leftrightarrow \frac{I - J}{N} \in ℤ)$
75		zdiv	$⊢ (N \in ℕ \land I - J \in ℤ) \to (\exists k \in ℤ N k = I - J \leftrightarrow \frac{I - J}{N} \in ℤ)$
76	7 70 75	syl2an2r	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (\exists k \in ℤ N k = I - J \leftrightarrow \frac{I - J}{N} \in ℤ)$
77		oveq2	$⊢ k = 0 \to N k = N \cdot 0$
78		elfzoel2	$⊢ I \in (0 ..^N) \to N \in ℤ$
79	78	zcnd	$⊢ I \in (0 ..^N) \to N \in ℂ$
80	79	mul01d	$⊢ I \in (0 ..^N) \to N \cdot 0 = 0$
81	80	adantr	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to N \cdot 0 = 0$
82	81	adantr	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to N \cdot 0 = 0$
83	77 82	sylan9eq	$⊢ (k = 0 \land ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ)) \to N k = 0$
84	83	eqeq1d	$⊢ (k = 0 \land ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ)) \to (N k = I - J \leftrightarrow 0 = I - J)$
85		eqcom	$⊢ 0 = I - J \leftrightarrow I - J = 0$
86	1	zcnd	$⊢ I \in (0 ..^N) \to I \in ℂ$
87	13	zcnd	$⊢ J \in (0 ..^N) \to J \in ℂ$
88		subeq0	$⊢ (I \in ℂ \land J \in ℂ) \to (I - J = 0 \leftrightarrow I = J)$
89	86 87 88	syl2an	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (I - J = 0 \leftrightarrow I = J)$
90	89	biimpd	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (I - J = 0 \to I = J)$
91	85 90	syl5bi	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (0 = I - J \to I = J)$
92	91	adantr	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (0 = I - J \to I = J)$
93	92	adantl	$⊢ (k = 0 \land ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ)) \to (0 = I - J \to I = J)$
94	84 93	sylbid	$⊢ (k = 0 \land ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ)) \to (N k = I - J \to I = J)$
95	94	ex	$⊢ k = 0 \to (((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (N k = I - J \to I = J))$
96		subfzo0	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (- N < I - J \land I - J < N)$
97	96	adantr	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (- N < I - J \land I - J < N)$
98		elz	$⊢ k \in ℤ \leftrightarrow (k \in ℝ \land (k = 0 \lor k \in ℕ \lor - k \in ℕ))$
99		pm2.24	$⊢ k = 0 \to (\neg k = 0 \to (N k = I - J \to I = J))$
100	99	a1d	$⊢ k = 0 \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))$
101	100	2a1d	$⊢ k = 0 \to (k \in ℝ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))))$
102		breq1	$⊢ N k = I - J \to (N k < N \leftrightarrow I - J < N)$
103		nncn	$⊢ N \in ℕ \to N \in ℂ$
104	103	mulid1d	$⊢ N \in ℕ \to N \cdot 1 = N$
105	104	adantr	$⊢ (N \in ℕ \land k \in ℕ) \to N \cdot 1 = N$
106	105	eqcomd	$⊢ (N \in ℕ \land k \in ℕ) \to N = N \cdot 1$
107	106	breq2d	$⊢ (N \in ℕ \land k \in ℕ) \to (N k < N \leftrightarrow N k < N \cdot 1)$
108		nnre	$⊢ k \in ℕ \to k \in ℝ$
109	108	adantl	$⊢ (N \in ℕ \land k \in ℕ) \to k \in ℝ$
110		1red	$⊢ (N \in ℕ \land k \in ℕ) \to 1 \in ℝ$
111	21	adantr	$⊢ (N \in ℕ \land k \in ℕ) \to N \in ℝ^{+}$
112	109 110 111	ltmul2d	$⊢ (N \in ℕ \land k \in ℕ) \to (k < 1 \leftrightarrow N k < N \cdot 1)$
113		nnge1	$⊢ k \in ℕ \to 1 \leq k$
114		1red	$⊢ k \in ℕ \to 1 \in ℝ$
115	114 108	lenltd	$⊢ k \in ℕ \to (1 \leq k \leftrightarrow \neg k < 1)$
116		pm2.21	$⊢ \neg k < 1 \to (k < 1 \to I = J)$
117	115 116	syl6bi	$⊢ k \in ℕ \to (1 \leq k \to (k < 1 \to I = J))$
118	113 117	mpd	$⊢ k \in ℕ \to (k < 1 \to I = J)$
119	118	adantl	$⊢ (N \in ℕ \land k \in ℕ) \to (k < 1 \to I = J)$
120	112 119	sylbird	$⊢ (N \in ℕ \land k \in ℕ) \to (N k < N \cdot 1 \to I = J)$
121	107 120	sylbid	$⊢ (N \in ℕ \land k \in ℕ) \to (N k < N \to I = J)$
122	121	ex	$⊢ N \in ℕ \to (k \in ℕ \to (N k < N \to I = J))$
123	122	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (k \in ℕ \to (N k < N \to I = J))$
124	32 123	sylbi	$⊢ J \in (0 ..^N) \to (k \in ℕ \to (N k < N \to I = J))$
125	124	adantl	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (k \in ℕ \to (N k < N \to I = J))$
126	125	com13	$⊢ N k < N \to (k \in ℕ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to I = J))$
127	126	a1dd	$⊢ N k < N \to (k \in ℕ \to (\neg k = 0 \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to I = J)))$
128	102 127	syl6bir	$⊢ N k = I - J \to (I - J < N \to (k \in ℕ \to (\neg k = 0 \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to I = J))))$
129	128	com15	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (I - J < N \to (k \in ℕ \to (\neg k = 0 \to (N k = I - J \to I = J))))$
130	129	com12	$⊢ I - J < N \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to (k \in ℕ \to (\neg k = 0 \to (N k = I - J \to I = J))))$
131	130	adantl	$⊢ (- N < I - J \land I - J < N) \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to (k \in ℕ \to (\neg k = 0 \to (N k = I - J \to I = J))))$
132	131	com13	$⊢ k \in ℕ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
133	132	a1d	$⊢ k \in ℕ \to (k \in ℝ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))))$
134		breq2	$⊢ N k = I - J \to (- N < N k \leftrightarrow - N < I - J)$
135		nnre	$⊢ N \in ℕ \to N \in ℝ$
136		simpr	$⊢ (- k \in ℕ \land k \in ℝ) \to k \in ℝ$
137		remulcl	$⊢ (N \in ℝ \land k \in ℝ) \to N k \in ℝ$
138	135 136 137	syl2an	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N k \in ℝ$
139	135	adantr	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N \in ℝ$
140	138 139	possumd	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (0 < N k + N \leftrightarrow - N < N k)$
141	103	adantr	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N \in ℂ$
142	141	mulid1d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N \cdot 1 = N$
143	142	eqcomd	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N = N \cdot 1$
144	143	oveq2d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N k + N = N k + N \cdot 1$
145		recn	$⊢ k \in ℝ \to k \in ℂ$
146	145	adantl	$⊢ (- k \in ℕ \land k \in ℝ) \to k \in ℂ$
147	146	adantl	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to k \in ℂ$
148		1cnd	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to 1 \in ℂ$
149	141 147 148	adddid	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N (k + 1) = N k + N \cdot 1$
150	144 149	eqtr4d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N k + N = N (k + 1)$
151	150	breq2d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (0 < N k + N \leftrightarrow 0 < N (k + 1))$
152		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
153	152	adantl	$⊢ (- k \in ℕ \land k \in ℝ) \to k + 1 \in ℝ$
154	153	adantl	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to k + 1 \in ℝ$
155	139 154	remulcld	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N (k + 1) \in ℝ$
156		0red	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to 0 \in ℝ$
157		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
158	157	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N$
159		nnge1	$⊢ - k \in ℕ \to 1 \leq - k$
160		id	$⊢ k \in ℂ \to k \in ℂ$
161		1cnd	$⊢ k \in ℂ \to 1 \in ℂ$
162	160 161	addcomd	$⊢ k \in ℂ \to k + 1 = 1 + k$
163	161 160	subnegd	$⊢ k \in ℂ \to 1 - (- k) = 1 + k$
164	162 163	eqtr4d	$⊢ k \in ℂ \to k + 1 = 1 - (- k)$
165	145 164	syl	$⊢ k \in ℝ \to k + 1 = 1 - (- k)$
166	165	adantl	$⊢ (1 \leq - k \land k \in ℝ) \to k + 1 = 1 - (- k)$
167		1red	$⊢ k \in ℝ \to 1 \in ℝ$
168		renegcl	$⊢ k \in ℝ \to - k \in ℝ$
169	167 168	suble0d	$⊢ k \in ℝ \to (1 - (- k) \leq 0 \leftrightarrow 1 \leq - k)$
170	169	biimparc	$⊢ (1 \leq - k \land k \in ℝ) \to 1 - (- k) \leq 0$
171	166 170	eqbrtrd	$⊢ (1 \leq - k \land k \in ℝ) \to k + 1 \leq 0$
172	159 171	sylan	$⊢ (- k \in ℕ \land k \in ℝ) \to k + 1 \leq 0$
173	158 172	anim12i	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (0 \leq N \land k + 1 \leq 0)$
174	173	olcd	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to ((N \leq 0 \land 0 \leq k + 1) \lor (0 \leq N \land k + 1 \leq 0))$
175		mulle0b	$⊢ (N \in ℝ \land k + 1 \in ℝ) \to (N (k + 1) \leq 0 \leftrightarrow ((N \leq 0 \land 0 \leq k + 1) \lor (0 \leq N \land k + 1 \leq 0)))$
176	135 153 175	syl2an	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (N (k + 1) \leq 0 \leftrightarrow ((N \leq 0 \land 0 \leq k + 1) \lor (0 \leq N \land k + 1 \leq 0)))$
177	174 176	mpbird	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to N (k + 1) \leq 0$
178	155 156 177	lensymd	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to \neg 0 < N (k + 1)$
179	178	pm2.21d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (0 < N (k + 1) \to I = J)$
180	151 179	sylbid	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (0 < N k + N \to I = J)$
181	140 180	sylbird	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (- N < N k \to I = J)$
182	181	a1d	$⊢ (N \in ℕ \land (- k \in ℕ \land k \in ℝ)) \to (\neg k = 0 \to (- N < N k \to I = J))$
183	182	ex	$⊢ N \in ℕ \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (- N < N k \to I = J)))$
184	183	3ad2ant2	$⊢ (I \in ℕ_{0} \land N \in ℕ \land I < N) \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (- N < N k \to I = J)))$
185	6 184	sylbi	$⊢ I \in (0 ..^N) \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (- N < N k \to I = J)))$
186	185	adantr	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (- N < N k \to I = J)))$
187	186	com14	$⊢ - N < N k \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to I = J)))$
188	134 187	syl6bir	$⊢ N k = I - J \to (- N < I - J \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to I = J))))$
189	188	com15	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (- N < I - J \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
190	189	com12	$⊢ - N < I - J \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
191	190	adantr	$⊢ (- N < I - J \land I - J < N) \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- k \in ℕ \land k \in ℝ) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
192	191	com13	$⊢ (- k \in ℕ \land k \in ℝ) \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
193	192	ex	$⊢ - k \in ℕ \to (k \in ℝ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))))$
194	101 133 193	3jaoi	$⊢ (k = 0 \lor k \in ℕ \lor - k \in ℕ) \to (k \in ℝ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))))$
195	194	impcom	$⊢ (k \in ℝ \land (k = 0 \lor k \in ℕ \lor - k \in ℕ)) \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
196	98 195	sylbi	$⊢ k \in ℤ \to ((I \in (0 ..^N) \land J \in (0 ..^N)) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J))))$
197	196	impcom	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to ((- N < I - J \land I - J < N) \to (\neg k = 0 \to (N k = I - J \to I = J)))$
198	97 197	mpd	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (\neg k = 0 \to (N k = I - J \to I = J))$
199	198	com12	$⊢ \neg k = 0 \to (((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (N k = I - J \to I = J))$
200	95 199	pm2.61i	$⊢ ((I \in (0 ..^N) \land J \in (0 ..^N)) \land k \in ℤ) \to (N k = I - J \to I = J)$
201	200	rexlimdva	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (\exists k \in ℤ N k = I - J \to I = J)$
202	76 201	sylbird	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to (\frac{I - J}{N} \in ℤ \to I = J)$
203	74 202	sylbid	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N)) \to ((I - J) \mod N = 0 \to I = J)$
204	203	3adant3	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I - J) \mod N = 0 \to I = J)$
205	68 204	sylbid	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (((I \mod N) - (J \mod N)) \mod N = 0 \to I = J)$
206	61 205	sylbid	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N)) \mod N = 0 \mod N \to I = J)$
207	45 206	syl5	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((((I \mod N) + S) \mod N) - (((J \mod N) + S) \mod N) = 0 \to I = J)$
208	44 207	sylbird	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to (((I \mod N) + S) \mod N = ((J \mod N) + S) \mod N \to I = J)$
209	19 208	sylbid	$⊢ (I \in (0 ..^N) \land J \in (0 ..^N) \land S \in ℤ) \to ((I + S) \mod N = (J + S) \mod N \to I = J)$
210		oveq1	$⊢ I = J \to I + S = J + S$
211	210	oveq1d	$⊢ I = J \to (I + S) \mod N = (J + S) \mod N$
212	209 211	impbid1	$⊢ (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 addmodlteq

Proof