Theorem addmodlteq 13915

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 16272. (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 13636	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℤ)
2	1	zred 12670	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℝ)
3	2	3ad2ant1 1131	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℝ)
4		simp3 1136	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℤ)
5	4	zred 12670	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℝ)
6		elfzo0 13677	. . . . . . . . 9 ⊢ (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
7	6	simp2bi 1144	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
8	7	nnrpd 13018	. . . . . . 7 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
9	8	3ad2ant1 1131	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ+)
10		modaddmod 13879	. . . . . 6 ⊢ ((𝐼 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
11	3, 5, 9, 10	syl3anc 1369	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
12	11	eqcomd 2736	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 + 𝑆) mod 𝑁) = (((𝐼 mod 𝑁) + 𝑆) mod 𝑁))
13		elfzoelz 13636	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
14	13	zred 12670	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
15	14	3ad2ant2 1132	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℝ)
16		modaddmod 13879	. . . . . 6 ⊢ ((𝐽 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
17	15, 5, 9, 16	syl3anc 1369	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
18	17	eqcomd 2736	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁))
19	12, 18	eqeq12d 2746	. . 3 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
20		nn0re 12485	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ)
21		nnrp 12989	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
22	20, 21	anim12i 611	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
23	22	3adant3 1130	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
24		modcl 13842	. . . . . . . . . 10 ⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (𝐼 mod 𝑁) ∈ ℝ)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → (𝐼 mod 𝑁) ∈ ℝ)
26	6, 25	sylbi 216	. . . . . . . 8 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) ∈ ℝ)
27	26	3ad2ant1 1131	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℝ)
28	27, 5	readdcld 11247	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℝ)
29		modcl 13842	. . . . . . 7 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
30	29	recnd 11246	. . . . . 6 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
31	28, 9, 30	syl2anc 582	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
32		elfzo0 13677	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
33		nn0re 12485	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ ℕ0 → 𝐽 ∈ ℝ)
34	33, 21	anim12i 611	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
35	34	3adant3 1130	. . . . . . . . . 10 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+))
36		modcl 13842	. . . . . . . . . 10 ⊢ ((𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (𝐽 mod 𝑁) ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 mod 𝑁) ∈ ℝ)
38	32, 37	sylbi 216	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) ∈ ℝ)
39	38	3ad2ant2 1132	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℝ)
40	39, 5	readdcld 11247	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ)
41		modcl 13842	. . . . . . 7 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℝ)
42	41	recnd 11246	. . . . . 6 ⊢ ((((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
43	40, 9, 42	syl2anc 582	. . . . 5 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
44	31, 43	subeq0ad 11585	. . . 4 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
45		oveq1 7418	. . . . 5 ⊢ (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁))
46		modsubmodmod 13899	. . . . . . . . 9 ⊢ ((((𝐼 mod 𝑁) + 𝑆) ∈ ℝ ∧ ((𝐽 mod 𝑁) + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
47	28, 40, 9, 46	syl3anc 1369	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
48	26	recnd 11246	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) ∈ ℂ)
49	48	3ad2ant1 1131	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℂ)
50	38	recnd 11246	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) ∈ ℂ)
51	50	3ad2ant2 1132	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℂ)
52	4	zcnd 12671	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℂ)
53	49, 51, 52	pnpcan2d 11613	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) = ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)))
54	53	oveq1d 7426	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
55	47, 54	eqtrd 2770	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
56	32	simp2bi 1144	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℕ)
57	56	nnrpd 13018	. . . . . . . . 9 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℝ+)
58		0mod 13871	. . . . . . . . 9 ⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0)
59	57, 58	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (0 mod 𝑁) = 0)
60	59	3ad2ant2 1132	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (0 mod 𝑁) = 0)
61	55, 60	eqeq12d 2746	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) ↔ (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0))
62		zmodidfzoimp 13870	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) = 𝐼)
63	62	3ad2ant1 1131	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) = 𝐼)
64		zmodidfzoimp 13870	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) = 𝐽)
65	64	3ad2ant2 1132	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) = 𝐽)
66	63, 65	oveq12d 7429	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) = (𝐼 − 𝐽))
67	66	oveq1d 7426	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = ((𝐼 − 𝐽) mod 𝑁))
68	67	eqeq1d 2732	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) mod 𝑁) = 0))
69		zsubcl 12608	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 − 𝐽) ∈ ℤ)
70	1, 13, 69	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℤ)
71	70	zred 12670	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐼 − 𝐽) ∈ ℝ)
72	8	adantr 479	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ+)
73		mod0 13845	. . . . . . . . . 10 ⊢ (((𝐼 − 𝐽) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
74	71, 72, 73	syl2anc 582	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) mod 𝑁) = 0 ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
75		zdiv 12636	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐼 − 𝐽) ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
76	7, 70, 75	syl2an2r 681	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ ((𝐼 − 𝐽) / 𝑁) ∈ ℤ))
77		oveq2 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (𝑁 · 𝑘) = (𝑁 · 0))
78		elfzoel2 13635	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
79	78	zcnd 12671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
80	79	mul01d 11417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐼 ∈ (0..^𝑁) → (𝑁 · 0) = 0)
81	80	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑁 · 0) = 0)
82	81	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (𝑁 · 0) = 0)
83	77, 82	sylan9eq 2790	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → (𝑁 · 𝑘) = 0)
84	83	eqeq1d 2732	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) ↔ 0 = (𝐼 − 𝐽)))
85		eqcom 2737	. . . . . . . . . . . . . . . . 17 ⊢ (0 = (𝐼 − 𝐽) ↔ (𝐼 − 𝐽) = 0)
86	1	zcnd 12671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℂ)
87	13	zcnd 12671	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℂ)
88		subeq0 11490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ) → ((𝐼 − 𝐽) = 0 ↔ 𝐼 = 𝐽))
89	86, 87, 88	syl2an 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) = 0 ↔ 𝐼 = 𝐽))
90	89	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) = 0 → 𝐼 = 𝐽))
91	85, 90	biimtrid 241	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
92	91	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
93	92	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → (0 = (𝐼 − 𝐽) → 𝐼 = 𝐽))
94	84, 93	sylbid 239	. . . . . . . . . . . . 13 ⊢ ((𝑘 = 0 ∧ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ)) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))
95	94	ex 411	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))
96		subfzo0 13758	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
97	96	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) ∧ 𝑘 ∈ ℤ) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
98		elz 12564	. . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝐼 − 𝐽) < 𝑁))
103		nncn 12224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
104	103	mulridd 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 · 1) = 𝑁)
105	104	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑁 · 1) = 𝑁)
106	105	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 = (𝑁 · 1))
107	106	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < 𝑁 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
108		nnre 12223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
109	108	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
110		1red 11219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
111	21	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℝ+)
112	109, 110, 111	ltmul2d 13062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
113		nnge1 12244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → 1 ≤ 𝑘)
114		1red 11219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
115	114, 108	lenltd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ∈ ℕ → (1 ≤ 𝑘 ↔ ¬ 𝑘 < 1))
116		pm2.21 123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ 𝑘 < 1 → (𝑘 < 1 → 𝐼 = 𝐽))
117	115, 116	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ ℕ → (1 ≤ 𝑘 → (𝑘 < 1 → 𝐼 = 𝐽)))
118	113, 117	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ ℕ → (𝑘 < 1 → 𝐼 = 𝐽))
119	118	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 → 𝐼 = 𝐽))
120	112, 119	sylbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < (𝑁 · 1) → 𝐼 = 𝐽))
121	107, 120	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽))
122	121	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
123	122	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐽 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
124	32, 123	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 ∈ (0..^𝑁) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
125	124	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → ((𝑁 · 𝑘) < 𝑁 → 𝐼 = 𝐽)))
126	125	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 · 𝑘) < 𝑁 → (𝑘 ∈ ℕ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))
127	126	a1dd 50	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽))))
128	102, 127	syl6bir 253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → ((𝐼 − 𝐽) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))))
129	128	com15 101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 − 𝐽) < 𝑁 → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
130	129	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐼 − 𝐽) < 𝑁 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
131	130	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑘 ∈ ℕ → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
132	131	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
133	132	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
134		breq2 5151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → (-𝑁 < (𝑁 · 𝑘) ↔ -𝑁 < (𝐼 − 𝐽)))
135		nnre 12223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
136		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ)
137		remulcl 11197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑁 · 𝑘) ∈ ℝ)
138	135, 136, 137	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 𝑘) ∈ ℝ)
139	135	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℝ)
140	138, 139	possumd 11843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ -𝑁 < (𝑁 · 𝑘)))
141	103	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 ∈ ℂ)
142	141	mulridd 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · 1) = 𝑁)
143	142	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑁 = (𝑁 · 1))
144	143	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
145		recn 11202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → 𝑘 ∈ ℂ)
146	145	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℂ)
147	146	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 𝑘 ∈ ℂ)
148		1cnd 11213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 1 ∈ ℂ)
149	141, 147, 148	adddid 11242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) = ((𝑁 · 𝑘) + (𝑁 · 1)))
150	144, 149	eqtr4d 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · 𝑘) + 𝑁) = (𝑁 · (𝑘 + 1)))
151	150	breq2d 5159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ 0 < (𝑁 · (𝑘 + 1))))
152		peano2re 11391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
153	152	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ∈ ℝ)
154	153	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑘 + 1) ∈ ℝ)
155	139, 154	remulcld 11248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
156		0red 11221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → 0 ∈ ℝ)
157		nnnn0 12483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
158	157	nn0ge0d 12539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
159		nnge1 12244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (-𝑘 ∈ ℕ → 1 ≤ -𝑘)
160		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 𝑘 ∈ ℂ)
161		1cnd 11213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 ∈ ℂ → 1 ∈ ℂ)
162	160, 161	addcomd 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 + 𝑘))
163	161, 160	subnegd 11582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑘 ∈ ℂ → (1 − -𝑘) = (1 + 𝑘))
164	162, 163	eqtr4d 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℂ → (𝑘 + 1) = (1 − -𝑘))
165	145, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) = (1 − -𝑘))
166	165	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) = (1 − -𝑘))
167		1red 11219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → 1 ∈ ℝ)
168		renegcl 11527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑘 ∈ ℝ → -𝑘 ∈ ℝ)
169	167, 168	suble0d 11809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑘 ∈ ℝ → ((1 − -𝑘) ≤ 0 ↔ 1 ≤ -𝑘))
170	169	biimparc 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (1 − -𝑘) ≤ 0)
171	166, 170	eqbrtrd 5169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((1 ≤ -𝑘 ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
172	159, 171	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (𝑘 + 1) ≤ 0)
173	158, 172	anim12i 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))
174	173	olcd 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0)))
175		mulle0b 12089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
176	135, 153, 175	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ((𝑁 · (𝑘 + 1)) ≤ 0 ↔ ((𝑁 ≤ 0 ∧ 0 ≤ (𝑘 + 1)) ∨ (0 ≤ 𝑁 ∧ (𝑘 + 1) ≤ 0))))
177	174, 176	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (𝑁 · (𝑘 + 1)) ≤ 0)
178	155, 156, 177	lensymd 11369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → ¬ 0 < (𝑁 · (𝑘 + 1)))
179	178	pm2.21d 121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < (𝑁 · (𝑘 + 1)) → 𝐼 = 𝐽))
180	151, 179	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (0 < ((𝑁 · 𝑘) + 𝑁) → 𝐼 = 𝐽))
181	140, 180	sylbird 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))
182	181	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ ℕ ∧ (-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ)) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽)))
183	182	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℕ → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
184	183	3ad2ant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
185	6, 184	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∈ (0..^𝑁) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
186	185	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → (-𝑁 < (𝑁 · 𝑘) → 𝐼 = 𝐽))))
187	186	com14 96	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (-𝑁 < (𝑁 · 𝑘) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽))))
188	134, 187	syl6bir 253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 · 𝑘) = (𝐼 − 𝐽) → (-𝑁 < (𝐼 − 𝐽) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → 𝐼 = 𝐽)))))
189	188	com15 101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
190	189	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝑁 < (𝐼 − 𝐽) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
191	190	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
192	191	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝑘 ∈ ℕ ∧ 𝑘 ∈ ℝ) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
193	192	ex 411	. . . . . . . . . . . . . . . . . 18 ⊢ (-𝑘 ∈ ℕ → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
194	101, 133, 193	3jaoi 1425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ) → (𝑘 ∈ ℝ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))))))
195	194	impcom 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)) → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
196	98, 195	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℤ → ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁) → (¬ 𝑘 = 0 → ((𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽)))))
197	196	impcom 406	. . . . . . . . . . . . . 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 3153	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼 − 𝐽) → 𝐼 = 𝐽))
202	76, 201	sylbird 259	. . . . . . . . 9 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) / 𝑁) ∈ ℤ → 𝐼 = 𝐽))
203	74, 202	sylbid 239	. . . . . . . 8 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (((𝐼 − 𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
204	203	3adant3 1130	. . . . . . 7 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 − 𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
205	68, 204	sylbid 239	. . . . . 6 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 → 𝐼 = 𝐽))
206	61, 205	sylbid 239	. . . . 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 259	. . 3 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
209	19, 208	sylbid 239	. 2 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
210		oveq1 7418	. . 3 ⊢ (𝐼 = 𝐽 → (𝐼 + 𝑆) = (𝐽 + 𝑆))
211	210	oveq1d 7426	. 2 ⊢ (𝐼 = 𝐽 → ((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
212	209, 211	impbid1 224	1 ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ∃wrex 3068   class class class wbr 5147  (class class class)co 7411  ℂcc 11110  ℝcr 11111  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117   < clt 11252   ≤ cle 11253   − cmin 11448  -cneg 11449   / cdiv 11875  ℕcn 12216  ℕ₀cn0 12476  ℤcz 12562  ℝ⁺crp 12978  ..^cfzo 13631   mod cmo 13838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839

This theorem is referenced by:  cshf1  14764