Theorem addmodlteq 13997

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 16373. (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 13716	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℤ)
2	1	zred 12747	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℝ)
3	2	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℝ)
4		simp3 1138	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℤ)
5	4	zred 12747	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℝ)
6		elfzo0 13757	. . . . . . . . 9 ⊢ (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
7	6	simp2bi 1146	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
8	7	nnrpd 13097	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
9	8	3ad2ant1 1133	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ+)
10		modaddmod 13961	. . . . . 6 ⊢ ((𝐼 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
11	3, 5, 9, 10	syl3anc 1371	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
12	11	eqcomd 2746	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 + 𝑆) mod 𝑁) = (((𝐼 mod 𝑁) + 𝑆) mod 𝑁))
13		elfzoelz 13716	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
14	13	zred 12747	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
15	14	3ad2ant2 1134	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℝ)
16		modaddmod 13961	. . . . . 6 ⊢ ((𝐽 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
17	15, 5, 9, 16	syl3anc 1371	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
18	17	eqcomd 2746	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁))
19	12, 18	eqeq12d 2756	. . 3 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
20		nn0re 12562	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ)
21		nnrp 13068	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
22	20, 21	anim12i 612	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
23	22	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
24		modcl 13924	. . . . . . . . . 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 11319	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℝ)
29		modcl 13924	. . . . . . 7 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
30	29	recnd 11318	. . . . . 6 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
31	28, 9, 30	syl2anc 583	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
32		elfzo0 13757	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
33		nn0re 12562	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ ℕ0 → 𝐽 ∈ ℝ)
34	33, 21	anim12i 612	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
35	34	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
36		modcl 13924	. . . . . . . . . 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 11319	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ)
41		modcl 13924	. . . . . . 7 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
42	41	recnd 11318	. . . . . 6 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
43	40, 9, 42	syl2anc 583	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
44	31, 43	subeq0ad 11657	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
45		oveq1 7455	. . . . 5 ⊢ (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁))
46		modsubmodmod 13981	. . . . . . . . 9 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
47	28, 40, 9, 46	syl3anc 1371	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
48	26	recnd 11318	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) ∈ ℂ)
49	48	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℂ)
50	38	recnd 11318	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) ∈ ℂ)
51	50	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℂ)
52	4	zcnd 12748	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℂ)
53	49, 51, 52	pnpcan2d 11685	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) = ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)))
54	53	oveq1d 7463	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
55	47, 54	eqtrd 2780	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
56	32	simp2bi 1146	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
57	56	nnrpd 13097	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
58		0mod 13953	. . . . . . . . 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 2756	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) ↔ (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0))
62		zmodidfzoimp 13952	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) = 𝐼)
63	62	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) = 𝐼)
64		zmodidfzoimp 13952	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) = 𝐽)
65	64	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) = 𝐽)
66	63, 65	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) = (𝐼 − 𝐽))
67	66	oveq1d 7463	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = ((𝐼 − 𝐽) mod 𝑁))
68	67	eqeq1d 2742	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) mod 𝑁) = 0))
69		zsubcl 12685	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 − 𝐽) ∈ ℤ)
70	1, 13, 69	syl2an 595	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℤ)
71	70	zred 12747	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℝ)
72	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ+)
73		mod0 13927	. . . . . . . . . 10 ⊢ (((𝐼 − 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
74	71, 72, 73	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
75		zdiv 12713	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐼 − 𝐽) ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
76	7, 70, 75	syl2an2r 684	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
77		oveq2 7456	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (𝑁 · 𝑘) = (𝑁 · 0))
78		elfzoel2 13715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
79	78	zcnd 12748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
80	79	mul01d 11489	. . . . . . . . . . . . . . . . . 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 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → (𝑁 · 𝑘) = 0)
84	83	eqeq1d 2742	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ 0 = (𝐼 − 𝐽)))
85		eqcom 2747	. . . . . . . . . . . . . . . . 17 ⊢ (0 = (𝐼 − 𝐽) ↔ (𝐼 − 𝐽) = 0)
86	1	zcnd 12748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℂ)
87	13	zcnd 12748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ)
88		subeq0 11562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐼 − 𝐽) = 0 ↔ 𝐼 = 𝐽))
89	86, 87, 88	syl2an 595	. . . . . . . . . . . . . . . . . 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 13839	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
97	96	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
98		elz 12641	. . . . . . . . . . . . . . . 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 5169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝐼 − 𝐽) < 𝑁))
103		nncn 12301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
104	103	mulridd 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
105	104	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑁 · 1) = 𝑁)
106	105	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 = (𝑁 · 1))
107	106	breq2d 5178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
108		nnre 12300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
109	108	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
110		1red 11291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
111	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℝ+)
112	109, 110, 111	ltmul2d 13141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
113		nnge1 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
114		1red 11291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
115	114, 108	lenltd 11436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → (-𝑁 < (𝑁 · 𝑘) ↔ -𝑁 < (𝐼 − 𝐽)))
135		nnre 12300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
137		remulcl 11269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑁 · 𝑘) ∈ ℝ)
138	135, 136, 137	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 𝑘) ∈ ℝ)
139	135	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℝ)
140	138, 139	possumd 11915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ -𝑁 < (𝑁 · 𝑘)))
141	103	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℂ)
142	141	mulridd 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 1) = 𝑁)
143	142	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 = (𝑁 · 1))
144	143	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
145		recn 11274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℂ)
146	145	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℂ)
147	146	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑘 ∈ ℂ)
148		1cnd 11285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 1 ∈ ℂ)
149	141, 147, 148	adddid 11314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) = ((𝑁 · 𝑘) + (𝑁 · 1)))
150	144, 149	eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = (𝑁 · (𝑘 + 1)))
151	150	breq2d 5178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ 0 < (𝑁 · (𝑘 + 1))))
152		peano2re 11463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
153	152	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ∈ ℝ)
154	153	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑘 + 1) ∈ ℝ)
155	139, 154	remulcld 11320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
156		0red 11293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 0 ∈ ℝ)
157		nnnn0 12560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
158	157	nn0ge0d 12616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
159		nnge1 12321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (-𝑘 ∈ ℕ → 1 ≤ -𝑘)
160		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 𝑘 ∈ ℂ)
161		1cnd 11285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 1 ∈ ℂ)
162	160, 161	addcomd 11492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 + 𝑘))
163	161, 160	subnegd 11654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (1 − -𝑘) = (1 + 𝑘))
164	162, 163	eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 − -𝑘))
165	145, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) = (1 − -𝑘))
166	165	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) = (1 − -𝑘))
167		1red 11291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → 1 ∈ ℝ)
168		renegcl 11599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → -𝑘 ∈ ℝ)
169	167, 168	suble0d 11881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → ((1 − -𝑘) ≤ 0 ↔ 1 ≤ -𝑘))
170	169	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (1 − -𝑘) ≤ 0)
171	166, 170	eqbrtrd 5188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
172	159, 171	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
173	158, 172	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))
174	173	olcd 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0)))
175		mulle0b 12166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
176	135, 153, 175	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
177	174, 176	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ≤ 0)
178	155, 156, 177	lensymd 11441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1428	. . . . . . . . . . . . . . . . 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 3161	. . . . . . . . . 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 7455	. . 3 ⊢ (𝐼 = 𝐽 → (𝐼 + 𝑆) = (𝐽 + 𝑆))
211	210	oveq1d 7463	. 2 ⊢ (𝐼 = 𝐽 → ((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
212	209, 211	impbid1 225	1 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∨ w3o 1086   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∃wrex 3076   class class class wbr 5166  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189   < clt 11324   ≤ cle 11325   − cmin 11520  -cneg 11521   / cdiv 11947  ℕcn 12293  ℕ₀cn0 12553  ℤcz 12639  ℝ⁺crp 13057  ..^cfzo 13711   mod cmo 13920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921

This theorem is referenced by:  cshf1  14858