ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addmodlteq GIF version

Theorem addmodlteq 10201
Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. (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.
StepHypRef Expression
1 elfzoelz 9954 . . . . . . . 8 (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℤ)
213ad2ant1 1003 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℤ)
3 zq 9444 . . . . . . 7 (𝐼 ∈ ℤ → 𝐼 ∈ ℚ)
42, 3syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℚ)
5 simp3 984 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℤ)
6 zq 9444 . . . . . . 7 (𝑆 ∈ ℤ → 𝑆 ∈ ℚ)
75, 6syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℚ)
8 elfzo0 9989 . . . . . . . . . 10 (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
98biimpi 119 . . . . . . . . 9 (𝐼 ∈ (0..^𝑁) → (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
1093ad2ant1 1003 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
1110simp2d 995 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℕ)
12 nnq 9451 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
1311, 12syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℚ)
1411nngt0d 8787 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 0 < 𝑁)
15 modqaddmod 10166 . . . . . 6 (((𝐼 ∈ ℚ ∧ 𝑆 ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
164, 7, 13, 14, 15syl22anc 1218 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
1716eqcomd 2146 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 + 𝑆) mod 𝑁) = (((𝐼 mod 𝑁) + 𝑆) mod 𝑁))
18 elfzoelz 9954 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
19183ad2ant2 1004 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℤ)
20 zq 9444 . . . . . . 7 (𝐽 ∈ ℤ → 𝐽 ∈ ℚ)
2119, 20syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℚ)
22 modqaddmod 10166 . . . . . 6 (((𝐽 ∈ ℚ ∧ 𝑆 ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
2321, 7, 13, 14, 22syl22anc 1218 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
2423eqcomd 2146 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁))
2517, 24eqeq12d 2155 . . 3 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
262, 11zmodcld 10148 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℕ0)
2726nn0zd 9194 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℤ)
2827, 5zaddcld 9200 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℤ)
2928, 11zmodcld 10148 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℕ0)
3029nn0cnd 9055 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
3119, 11zmodcld 10148 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℕ0)
3231nn0zd 9194 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℤ)
3332, 5zaddcld 9200 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℤ)
3433, 11zmodcld 10148 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℕ0)
3534nn0cnd 9055 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
3630, 35subeq0ad 8106 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
37 oveq1 5788 . . . . 5 (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁))
384, 13, 14modqcld 10131 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℚ)
39 qaddcl 9453 . . . . . . . . . 10 (((𝐼 mod 𝑁) ∈ ℚ ∧ 𝑆 ∈ ℚ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℚ)
4038, 7, 39syl2anc 409 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℚ)
4121, 13, 14modqcld 10131 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℚ)
42 qaddcl 9453 . . . . . . . . . 10 (((𝐽 mod 𝑁) ∈ ℚ ∧ 𝑆 ∈ ℚ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ)
4341, 7, 42syl2anc 409 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ)
44 modqsubmodmod 10186 . . . . . . . . 9 (((((𝐼 mod 𝑁) + 𝑆) ∈ ℚ ∧ ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
4540, 43, 13, 14, 44syl22anc 1218 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
4626nn0cnd 9055 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℂ)
4731nn0cnd 9055 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℂ)
485zcnd 9197 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℂ)
4946, 47, 48pnpcan2d 8134 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) = ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)))
5049oveq1d 5796 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
5145, 50eqtrd 2173 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
52 q0mod 10158 . . . . . . . 8 ((𝑁 ∈ ℚ ∧ 0 < 𝑁) → (0 mod 𝑁) = 0)
5313, 14, 52syl2anc 409 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (0 mod 𝑁) = 0)
5451, 53eqeq12d 2155 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) ↔ (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0))
55 zmodidfzoimp 10157 . . . . . . . . . . 11 (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) = 𝐼)
56553ad2ant1 1003 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) = 𝐼)
57 zmodidfzoimp 10157 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) = 𝐽)
58573ad2ant2 1004 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) = 𝐽)
5956, 58oveq12d 5799 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) = (𝐼𝐽))
6059oveq1d 5796 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = ((𝐼𝐽) mod 𝑁))
6160eqeq1d 2149 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 ↔ ((𝐼𝐽) mod 𝑁) = 0))
62 qsubcl 9456 . . . . . . . . . 10 ((𝐼 ∈ ℚ ∧ 𝐽 ∈ ℚ) → (𝐼𝐽) ∈ ℚ)
634, 21, 62syl2anc 409 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼𝐽) ∈ ℚ)
64 modq0 10132 . . . . . . . . 9 (((𝐼𝐽) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐼𝐽) mod 𝑁) = 0 ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
6563, 13, 14, 64syl3anc 1217 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) mod 𝑁) = 0 ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
662, 19zsubcld 9201 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼𝐽) ∈ ℤ)
67 zdiv 9162 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝐼𝐽) ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
6811, 66, 67syl2anc 409 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
69 simpr 109 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝑘 = 0)
7069oveq2d 5797 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 𝑘) = (𝑁 · 0))
7111nncnd 8757 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℂ)
7271mul01d 8178 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝑁 · 0) = 0)
7372ad2antrr 480 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 0) = 0)
7470, 73eqtrd 2173 . . . . . . . . . . . . . . . 16 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 𝑘) = 0)
7574eqeq1d 2149 . . . . . . . . . . . . . . 15 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝑁 · 𝑘) = (𝐼𝐽) ↔ 0 = (𝐼𝐽)))
76 eqcom 2142 . . . . . . . . . . . . . . . 16 (0 = (𝐼𝐽) ↔ (𝐼𝐽) = 0)
7710simp1d 994 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℕ0)
7877ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐼 ∈ ℕ0)
7978nn0cnd 9055 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐼 ∈ ℂ)
80 elfzo0 9989 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
8180biimpi 119 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 ∈ (0..^𝑁) → (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
82813ad2ant2 1004 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
8382simp1d 994 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℕ0)
8483ad2antrr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐽 ∈ ℕ0)
8584nn0cnd 9055 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐽 ∈ ℂ)
8679, 85subeq0ad 8106 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝐼𝐽) = 0 ↔ 𝐼 = 𝐽))
8786biimpd 143 . . . . . . . . . . . . . . . 16 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝐼𝐽) = 0 → 𝐼 = 𝐽))
8876, 87syl5bi 151 . . . . . . . . . . . . . . 15 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (0 = (𝐼𝐽) → 𝐼 = 𝐽))
8975, 88sylbid 149 . . . . . . . . . . . . . 14 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
9089imp 123 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → 𝐼 = 𝐽)
9190an32s 558 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 = 0) → 𝐼 = 𝐽)
92 subfzo0 10049 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
93923adant3 1002 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
9493ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
9594simprd 113 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝐼𝐽) < 𝑁)
96 simplr 520 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 𝑘) = (𝐼𝐽))
9771mulid1d 7806 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝑁 · 1) = 𝑁)
9897ad3antrrr 484 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 1) = 𝑁)
9995, 96, 983brtr4d 3967 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 𝑘) < (𝑁 · 1))
100 simpllr 524 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
101100zred 9196 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
102 1red 7804 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
10311nnrpd 9510 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ+)
104103ad3antrrr 484 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℝ+)
105101, 102, 104ltmul2d 9555 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
10699, 105mpbird 166 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 < 1)
107 simpr 109 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
108107nnge1d 8786 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
109102, 101, 108lensymd 7907 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → ¬ 𝑘 < 1)
110106, 109pm2.21dd 610 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝐼 = 𝐽)
11193ad3antrrr 484 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
112111simpld 111 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑁 < (𝐼𝐽))
113 simplr 520 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · 𝑘) = (𝐼𝐽))
114112, 113breqtrrd 3963 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑁 < (𝑁 · 𝑘))
11511nnzd 9195 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℤ)
116115adantr 274 . . . . . . . . . . . . . . . . . . 19 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℤ)
117 simpr 109 . . . . . . . . . . . . . . . . . . 19 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
118116, 117zmulcld 9202 . . . . . . . . . . . . . . . . . 18 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · 𝑘) ∈ ℤ)
119118zred 9196 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · 𝑘) ∈ ℝ)
120119ad2antrr 480 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · 𝑘) ∈ ℝ)
12111nnred 8756 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ)
122121ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑁 ∈ ℝ)
123120, 122possumd 8354 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ -𝑁 < (𝑁 · 𝑘)))
124114, 123mpbird 166 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 < ((𝑁 · 𝑘) + 𝑁))
12597eqcomd 2146 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 = (𝑁 · 1))
126125oveq2d 5797 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
127126ad3antrrr 484 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
12871ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑁 ∈ ℂ)
129117zcnd 9197 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
130129ad2antrr 480 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
131 1cnd 7805 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ∈ ℂ)
132128, 130, 131adddid 7813 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) = ((𝑁 · 𝑘) + (𝑁 · 1)))
133127, 132eqtr4d 2176 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑁 · 𝑘) + 𝑁) = (𝑁 · (𝑘 + 1)))
134124, 133breqtrd 3961 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 < (𝑁 · (𝑘 + 1)))
135117peano2zd 9199 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℤ)
136116, 135zmulcld 9202 . . . . . . . . . . . . . . . 16 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) ∈ ℤ)
137136zred 9196 . . . . . . . . . . . . . . 15 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
138137ad2antrr 480 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
139 0red 7790 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 ∈ ℝ)
14071adantr 274 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℂ)
141135zcnd 9197 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℂ)
142140, 141mulcomd 7810 . . . . . . . . . . . . . . . 16 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) = ((𝑘 + 1) · 𝑁))
143142ad2antrr 480 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) = ((𝑘 + 1) · 𝑁))
144135zred 9196 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℝ)
145144ad2antrr 480 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
146 zcn 9082 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
147 1cnd 7805 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ → 1 ∈ ℂ)
148146, 147addcomd 7936 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (𝑘 + 1) = (1 + 𝑘))
149147, 146subnegd 8103 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (1 − -𝑘) = (1 + 𝑘))
150148, 149eqtr4d 2176 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (𝑘 + 1) = (1 − -𝑘))
151150ad3antlr 485 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) = (1 − -𝑘))
152 simpr 109 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑘 ∈ ℕ)
153152nnge1d 8786 . . . . . . . . . . . . . . . . . 18 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ≤ -𝑘)
154 1red 7804 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ∈ ℝ)
155152nnred 8756 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑘 ∈ ℝ)
156154, 155suble0d 8321 . . . . . . . . . . . . . . . . . 18 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((1 − -𝑘) ≤ 0 ↔ 1 ≤ -𝑘))
157153, 156mpbird 166 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (1 − -𝑘) ≤ 0)
158151, 157eqbrtrd 3957 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) ≤ 0)
15911nnnn0d 9053 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℕ0)
160159nn0ge0d 9056 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 0 ≤ 𝑁)
161160ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 ≤ 𝑁)
162 mulle0r 8725 . . . . . . . . . . . . . . . 16 ((((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ ((𝑘 + 1) ≤ 0 ∧ 0 ≤ 𝑁)) → ((𝑘 + 1) · 𝑁) ≤ 0)
163145, 122, 158, 161, 162syl22anc 1218 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑘 + 1) · 𝑁) ≤ 0)
164143, 163eqbrtrd 3957 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) ≤ 0)
165138, 139, 164lensymd 7907 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ¬ 0 < (𝑁 · (𝑘 + 1)))
166134, 165pm2.21dd 610 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝐼 = 𝐽)
167 elz 9079 . . . . . . . . . . . . . 14 (𝑘 ∈ ℤ ↔ (𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)))
168167simprbi 273 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ))
169168ad2antlr 481 . . . . . . . . . . . 12 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ))
17091, 110, 166, 169mpjao3dan 1286 . . . . . . . . . . 11 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → 𝐼 = 𝐽)
171170ex 114 . . . . . . . . . 10 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
172171rexlimdva 2552 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
17368, 172sylbird 169 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) / 𝑁) ∈ ℤ → 𝐼 = 𝐽))
17465, 173sylbid 149 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
17561, 174sylbid 149 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 → 𝐼 = 𝐽))
17654, 175sylbid 149 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) → 𝐼 = 𝐽))
17737, 176syl5 32 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → 𝐼 = 𝐽))
17836, 177sylbird 169 . . 3 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
17925, 178sylbid 149 . 2 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
180 oveq1 5788 . . 3 (𝐼 = 𝐽 → (𝐼 + 𝑆) = (𝐽 + 𝑆))
181180oveq1d 5796 . 2 (𝐼 = 𝐽 → ((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
182179, 181impbid1 141 1 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3o 962  w3a 963   = wceq 1332  wcel 1481  wrex 2418   class class class wbr 3936  (class class class)co 5781  cc 7641  cr 7642  0cc0 7643  1c1 7644   + caddc 7646   · cmul 7648   < clt 7823  cle 7824  cmin 7956  -cneg 7957   / cdiv 8455  cn 8743  0cn0 9000  cz 9077  cq 9437  +crp 9469  ..^cfzo 9949   mod cmo 10125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulrcl 7742  ax-addcom 7743  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-1rid 7750  ax-0id 7751  ax-rnegex 7752  ax-precex 7753  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-apti 7758  ax-pre-ltadd 7759  ax-pre-mulgt0 7760  ax-pre-mulext 7761  ax-arch 7762
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-id 4222  df-po 4225  df-iso 4226  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-fv 5138  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-reap 8360  df-ap 8367  df-div 8456  df-inn 8744  df-n0 9001  df-z 9078  df-uz 9350  df-q 9438  df-rp 9470  df-fz 9821  df-fzo 9950  df-fl 10073  df-mod 10126
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator