Theorem addmodlteq 13869

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 16252. (Contributed by AV, 20-Mar-2021.)

Assertion

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

Proof of Theorem addmodlteq

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzoelz 13575	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℤ)
2	1	zred 12596	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℝ)
3	2	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℝ)
4		simp3 1138	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℤ)
5	4	zred 12596	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℝ)
6		elfzo0 13616	. . . . . . . . 9 ⊢ (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
7	6	simp2bi 1146	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
8	7	nnrpd 12947	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
9	8	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ+)
10		modaddmod 13832	. . . . . 6 ⊢ ((𝐼 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
11	3, 5, 9, 10	syl3anc 1373	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
12	11	eqcomd 2742	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 + 𝑆) mod 𝑁) = (((𝐼 mod 𝑁) + 𝑆) mod 𝑁))
13		elfzoelz 13575	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
14	13	zred 12596	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
15	14	3ad2ant2 1134	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℝ)
16		modaddmod 13832	. . . . . 6 ⊢ ((𝐽 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
17	15, 5, 9, 16	syl3anc 1373	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
18	17	eqcomd 2742	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁))
19	12, 18	eqeq12d 2752	. . 3 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
20		nn0re 12410	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ)
21		nnrp 12917	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
22	20, 21	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
23	22	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
24		modcl 13793	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (𝐼 mod 𝑁) ∈ ℝ)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (𝐼 mod 𝑁) ∈ ℝ)
26	6, 25	sylbi 217	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) ∈ ℝ)
27	26	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℝ)
28	27, 5	readdcld 11161	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℝ)
29		modcl 13793	. . . . . . 7 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
30	29	recnd 11160	. . . . . 6 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
31	28, 9, 30	syl2anc 584	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
32		elfzo0 13616	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
33		nn0re 12410	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ ℕ0 → 𝐽 ∈ ℝ)
34	33, 21	anim12i 613	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
35	34	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
36		modcl 13793	. . . . . . . . . 10 ⊢ ((𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (𝐽 mod 𝑁) ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 mod 𝑁) ∈ ℝ)
38	32, 37	sylbi 217	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) ∈ ℝ)
39	38	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℝ)
40	39, 5	readdcld 11161	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ)
41		modcl 13793	. . . . . . 7 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
42	41	recnd 11160	. . . . . 6 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
43	40, 9, 42	syl2anc 584	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
44	31, 43	subeq0ad 11502	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
45		oveq1 7365	. . . . 5 ⊢ (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁))
46		modsubmodmod 13853	. . . . . . . . 9 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
47	28, 40, 9, 46	syl3anc 1373	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
48	26	recnd 11160	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) ∈ ℂ)
49	48	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℂ)
50	38	recnd 11160	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) ∈ ℂ)
51	50	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℂ)
52	4	zcnd 12597	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℂ)
53	49, 51, 52	pnpcan2d 11530	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) = ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)))
54	53	oveq1d 7373	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
55	47, 54	eqtrd 2771	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
56	32	simp2bi 1146	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
57	56	nnrpd 12947	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
58		0mod 13822	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0)
59	57, 58	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (0 mod 𝑁) = 0)
60	59	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (0 mod 𝑁) = 0)
61	55, 60	eqeq12d 2752	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) ↔ (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0))
62		zmodidfzoimp 13821	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) = 𝐼)
63	62	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) = 𝐼)
64		zmodidfzoimp 13821	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) = 𝐽)
65	64	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) = 𝐽)
66	63, 65	oveq12d 7376	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) = (𝐼 − 𝐽))
67	66	oveq1d 7373	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = ((𝐼 − 𝐽) mod 𝑁))
68	67	eqeq1d 2738	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) mod 𝑁) = 0))
69		zsubcl 12533	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 − 𝐽) ∈ ℤ)
70	1, 13, 69	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℤ)
71	70	zred 12596	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℝ)
72	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ+)
73		mod0 13796	. . . . . . . . . 10 ⊢ (((𝐼 − 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
74	71, 72, 73	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
75		zdiv 12562	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐼 − 𝐽) ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
76	7, 70, 75	syl2an2r 685	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
77		oveq2 7366	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (𝑁 · 𝑘) = (𝑁 · 0))
78		elfzoel2 13574	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
79	78	zcnd 12597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
80	79	mul01d 11332	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ (0..^𝑁) → (𝑁 · 0) = 0)
81	80	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑁 · 0) = 0)
82	81	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (𝑁 · 0) = 0)
83	77, 82	sylan9eq 2791	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → (𝑁 · 𝑘) = 0)
84	83	eqeq1d 2738	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ 0 = (𝐼 − 𝐽)))
85		eqcom 2743	. . . . . . . . . . . . . . . . 17 ⊢ (0 = (𝐼 − 𝐽) ↔ (𝐼 − 𝐽) = 0)
86	1	zcnd 12597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℂ)
87	13	zcnd 12597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ)
88		subeq0 11407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐼 − 𝐽) = 0 ↔ 𝐼 = 𝐽))
89	86, 87, 88	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) = 0 ↔ 𝐼 = 𝐽))
90	89	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) = 0 → 𝐼 = 𝐽))
91	85, 90	biimtrid 242	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
92	91	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
93	92	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
94	84, 93	sylbid 240	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))
95	94	ex 412	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))
96		subfzo0 13708	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
97	96	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
98		elz 12490	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℤ ↔ (𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)))
99		pm2.24 124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 0 → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))
100	99	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))
101	100	2a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
102		breq1 5101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝐼 − 𝐽) < 𝑁))
103		nncn 12153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
104	103	mulridd 11149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
105	104	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑁 · 1) = 𝑁)
106	105	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 = (𝑁 · 1))
107	106	breq2d 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
108		nnre 12152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
109	108	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
110		1red 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
111	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℝ+)
112	109, 110, 111	ltmul2d 12991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
113		nnge1 12173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
114		1red 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
115	114, 108	lenltd 11279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ ℕ → (1 ≤ 𝑘 ↔ ¬ 𝑘 < 1))
116		pm2.21 123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑘 < 1 → (𝑘 < 1 → 𝐼 = 𝐽))
117	115, 116	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → (1 ≤ 𝑘 → (𝑘 < 1 → 𝐼 = 𝐽)))
118	113, 117	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ ℕ → (𝑘 < 1 → 𝐼 = 𝐽))
119	118	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 → 𝐼 = 𝐽))
120	112, 119	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < (𝑁 · 1) → 𝐼 = 𝐽))
121	107, 120	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽))
122	121	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
123	122	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
124	32, 123	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 ∈ (0..^𝑁) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
125	124	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
126	125	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 · 𝑘) < 𝑁 → (𝑘 ∈ ℕ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))
127	126	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽))))
128	102, 127	biimtrrdi 254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → ((𝐼 − 𝐽) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))))
129	128	com15 101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
130	129	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 − 𝐽) < 𝑁 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
131	130	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
132	131	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
133	132	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
134		breq2 5102	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → (-𝑁 < (𝑁 · 𝑘) ↔ -𝑁 < (𝐼 − 𝐽)))
135		nnre 12152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
137		remulcl 11111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑁 · 𝑘) ∈ ℝ)
138	135, 136, 137	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 𝑘) ∈ ℝ)
139	135	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℝ)
140	138, 139	possumd 11762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ -𝑁 < (𝑁 · 𝑘)))
141	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℂ)
142	141	mulridd 11149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 1) = 𝑁)
143	142	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 = (𝑁 · 1))
144	143	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
145		recn 11116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℂ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℂ)
147	146	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑘 ∈ ℂ)
148		1cnd 11127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 1 ∈ ℂ)
149	141, 147, 148	adddid 11156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) = ((𝑁 · 𝑘) + (𝑁 · 1)))
150	144, 149	eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = (𝑁 · (𝑘 + 1)))
151	150	breq2d 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ 0 < (𝑁 · (𝑘 + 1))))
152		peano2re 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
153	152	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ∈ ℝ)
154	153	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑘 + 1) ∈ ℝ)
155	139, 154	remulcld 11162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
156		0red 11135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 0 ∈ ℝ)
157		nnnn0 12408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
158	157	nn0ge0d 12465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
159		nnge1 12173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (-𝑘 ∈ ℕ → 1 ≤ -𝑘)
160		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 𝑘 ∈ ℂ)
161		1cnd 11127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 1 ∈ ℂ)
162	160, 161	addcomd 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 + 𝑘))
163	161, 160	subnegd 11499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (1 − -𝑘) = (1 + 𝑘))
164	162, 163	eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 − -𝑘))
165	145, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) = (1 − -𝑘))
166	165	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) = (1 − -𝑘))
167		1red 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → 1 ∈ ℝ)
168		renegcl 11444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → -𝑘 ∈ ℝ)
169	167, 168	suble0d 11728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → ((1 − -𝑘) ≤ 0 ↔ 1 ≤ -𝑘))
170	169	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (1 − -𝑘) ≤ 0)
171	166, 170	eqbrtrd 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
172	159, 171	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
173	158, 172	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))
174	173	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0)))
175		mulle0b 12013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
176	135, 153, 175	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
177	174, 176	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ≤ 0)
178	155, 156, 177	lensymd 11284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ¬ 0 < (𝑁 · (𝑘 + 1)))
179	178	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < (𝑁 · (𝑘 + 1)) → 𝐼 = 𝐽))
180	151, 179	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) → 𝐼 = 𝐽))
181	140, 180	sylbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))
182	181	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽)))
183	182	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
184	183	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
185	6, 184	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∈ (0..^𝑁) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
186	185	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
187	186	com14 96	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-𝑁 < (𝑁 · 𝑘) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽))))
188	134, 187	biimtrrdi 254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → (-𝑁 < (𝐼 − 𝐽) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))))
189	188	com15 101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
190	189	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝑁 < (𝐼 − 𝐽) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
191	190	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
192	191	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
193	192	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝑘 ∈ ℕ → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
194	101, 133, 193	3jaoi 1430	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ) → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
195	194	impcom 407	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
196	98, 195	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
197	196	impcom 407	. . . . . . . . . . . . . 14 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))
198	97, 197	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))
199	198	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 𝑘 = 0 → (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))
200	95, 199	pm2.61i 182	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))
201	200	rexlimdva 3137	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))
202	76, 201	sylbird 260	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) / 𝑁) ∈ ℤ → 𝐼 = 𝐽))
203	74, 202	sylbid 240	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
204	203	3adant3 1132	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 − 𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
205	68, 204	sylbid 240	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 → 𝐼 = 𝐽))
206	61, 205	sylbid 240	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) → 𝐼 = 𝐽))
207	45, 206	syl5 34	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → 𝐼 = 𝐽))
208	44, 207	sylbird 260	. . 3 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
209	19, 208	sylbid 240	. 2 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
210		oveq1 7365	. . 3 ⊢ (𝐼 = 𝐽 → (𝐼 + 𝑆) = (𝐽 + 𝑆))
211	210	oveq1d 7373	. 2 ⊢ (𝐼 = 𝐽 → ((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
212	209, 211	impbid1 225	1 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∃wrex 3060   class class class wbr 5098  (class class class)co 7358  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031   < clt 11166   ≤ cle 11167   − cmin 11364  -cneg 11365   / cdiv 11794  ℕcn 12145  ℕ₀cn0 12401  ℤcz 12488  ℝ⁺crp 12905  ..^cfzo 13570   mod cmo 13789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9345  df-inf 9346  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-n0 12402  df-z 12489  df-uz 12752  df-rp 12906  df-fz 13424  df-fzo 13571  df-fl 13712  df-mod 13790

This theorem is referenced by:  cshf1  14733