Metamath Proof Explorer

Theorem 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 ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )

Proof

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