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

Theorem addmodlteq 9733
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 9486 . . . . . . . 8 (𝐼 ∈ (0..^𝑁) → 𝐼 ∈ ℤ)
213ad2ant1 962 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℤ)
3 zq 9043 . . . . . . 7 (𝐼 ∈ ℤ → 𝐼 ∈ ℚ)
42, 3syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℚ)
5 simp3 943 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℤ)
6 zq 9043 . . . . . . 7 (𝑆 ∈ ℤ → 𝑆 ∈ ℚ)
75, 6syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℚ)
8 elfzo0 9521 . . . . . . . . . 10 (𝐼 ∈ (0..^𝑁) ↔ (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
98biimpi 118 . . . . . . . . 9 (𝐼 ∈ (0..^𝑁) → (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
1093ad2ant1 962 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐼 < 𝑁))
1110simp2d 954 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℕ)
12 nnq 9050 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
1311, 12syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℚ)
1411nngt0d 8400 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 0 < 𝑁)
15 modqaddmod 9698 . . . . . 6 (((𝐼 ∈ ℚ ∧ 𝑆 ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
164, 7, 13, 14, 15syl22anc 1173 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐼 + 𝑆) mod 𝑁))
1716eqcomd 2090 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 + 𝑆) mod 𝑁) = (((𝐼 mod 𝑁) + 𝑆) mod 𝑁))
18 elfzoelz 9486 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
19183ad2ant2 963 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℤ)
20 zq 9043 . . . . . . 7 (𝐽 ∈ ℤ → 𝐽 ∈ ℚ)
2119, 20syl 14 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℚ)
22 modqaddmod 9698 . . . . . 6 (((𝐽 ∈ ℚ ∧ 𝑆 ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
2321, 7, 13, 14, 22syl22anc 1173 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
2423eqcomd 2090 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁))
2517, 24eqeq12d 2099 . . 3 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
262, 11zmodcld 9680 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℕ0)
2726nn0zd 8799 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℤ)
2827, 5zaddcld 8805 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℤ)
2928, 11zmodcld 9680 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℕ0)
3029nn0cnd 8661 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
3119, 11zmodcld 9680 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℕ0)
3231nn0zd 8799 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℤ)
3332, 5zaddcld 8805 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℤ)
3433, 11zmodcld 9680 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℕ0)
3534nn0cnd 8661 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) ∈ ℂ)
3630, 35subeq0ad 7747 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 ↔ (((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)))
37 oveq1 5620 . . . . 5 (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁))
384, 13, 14modqcld 9663 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℚ)
39 qaddcl 9052 . . . . . . . . . 10 (((𝐼 mod 𝑁) ∈ ℚ ∧ 𝑆 ∈ ℚ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℚ)
4038, 7, 39syl2anc 403 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) + 𝑆) ∈ ℚ)
4121, 13, 14modqcld 9663 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℚ)
42 qaddcl 9052 . . . . . . . . . 10 (((𝐽 mod 𝑁) ∈ ℚ ∧ 𝑆 ∈ ℚ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ)
4341, 7, 42syl2anc 403 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ)
44 modqsubmodmod 9718 . . . . . . . . 9 (((((𝐼 mod 𝑁) + 𝑆) ∈ ℚ ∧ ((𝐽 mod 𝑁) + 𝑆) ∈ ℚ) ∧ (𝑁 ∈ ℚ ∧ 0 < 𝑁)) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
4540, 43, 13, 14, 44syl22anc 1173 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁))
4626nn0cnd 8661 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℂ)
4731nn0cnd 8661 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) ∈ ℂ)
485zcnd 8802 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑆 ∈ ℂ)
4946, 47, 48pnpcan2d 7775 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) = ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)))
5049oveq1d 5628 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) − ((𝐽 mod 𝑁) + 𝑆)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
5145, 50eqtrd 2117 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁))
52 q0mod 9690 . . . . . . . 8 ((𝑁 ∈ ℚ ∧ 0 < 𝑁) → (0 mod 𝑁) = 0)
5313, 14, 52syl2anc 403 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (0 mod 𝑁) = 0)
5451, 53eqeq12d 2099 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) ↔ (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0))
55 zmodidfzoimp 9689 . . . . . . . . . . 11 (𝐼 ∈ (0..^𝑁) → (𝐼 mod 𝑁) = 𝐼)
56553ad2ant1 962 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼 mod 𝑁) = 𝐼)
57 zmodidfzoimp 9689 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → (𝐽 mod 𝑁) = 𝐽)
58573ad2ant2 963 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 mod 𝑁) = 𝐽)
5956, 58oveq12d 5631 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) = (𝐼𝐽))
6059oveq1d 5628 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = ((𝐼𝐽) mod 𝑁))
6160eqeq1d 2093 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 ↔ ((𝐼𝐽) mod 𝑁) = 0))
62 qsubcl 9055 . . . . . . . . . 10 ((𝐼 ∈ ℚ ∧ 𝐽 ∈ ℚ) → (𝐼𝐽) ∈ ℚ)
634, 21, 62syl2anc 403 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼𝐽) ∈ ℚ)
64 modq0 9664 . . . . . . . . 9 (((𝐼𝐽) ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (((𝐼𝐽) mod 𝑁) = 0 ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
6563, 13, 14, 64syl3anc 1172 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) mod 𝑁) = 0 ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
662, 19zsubcld 8806 . . . . . . . . . 10 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐼𝐽) ∈ ℤ)
67 zdiv 8767 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝐼𝐽) ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
6811, 66, 67syl2anc 403 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) ↔ ((𝐼𝐽) / 𝑁) ∈ ℤ))
69 simpr 108 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝑘 = 0)
7069oveq2d 5629 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 𝑘) = (𝑁 · 0))
7111nncnd 8371 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℂ)
7271mul01d 7815 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝑁 · 0) = 0)
7372ad2antrr 472 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 0) = 0)
7470, 73eqtrd 2117 . . . . . . . . . . . . . . . 16 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (𝑁 · 𝑘) = 0)
7574eqeq1d 2093 . . . . . . . . . . . . . . 15 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝑁 · 𝑘) = (𝐼𝐽) ↔ 0 = (𝐼𝐽)))
76 eqcom 2087 . . . . . . . . . . . . . . . 16 (0 = (𝐼𝐽) ↔ (𝐼𝐽) = 0)
7710simp1d 953 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐼 ∈ ℕ0)
7877ad2antrr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐼 ∈ ℕ0)
7978nn0cnd 8661 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐼 ∈ ℂ)
80 elfzo0 9521 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
8180biimpi 118 . . . . . . . . . . . . . . . . . . . . . 22 (𝐽 ∈ (0..^𝑁) → (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
82813ad2ant2 963 . . . . . . . . . . . . . . . . . . . . 21 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
8382simp1d 953 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝐽 ∈ ℕ0)
8483ad2antrr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐽 ∈ ℕ0)
8584nn0cnd 8661 . . . . . . . . . . . . . . . . . 18 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → 𝐽 ∈ ℂ)
8679, 85subeq0ad 7747 . . . . . . . . . . . . . . . . 17 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝐼𝐽) = 0 ↔ 𝐼 = 𝐽))
8786biimpd 142 . . . . . . . . . . . . . . . 16 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝐼𝐽) = 0 → 𝐼 = 𝐽))
8876, 87syl5bi 150 . . . . . . . . . . . . . . 15 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → (0 = (𝐼𝐽) → 𝐼 = 𝐽))
8975, 88sylbid 148 . . . . . . . . . . . . . 14 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) → ((𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
9089imp 122 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 = 0) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → 𝐼 = 𝐽)
9190an32s 533 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 = 0) → 𝐼 = 𝐽)
92 subfzo0 9581 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
93923adant3 961 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
9493ad3antrrr 476 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
9594simprd 112 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝐼𝐽) < 𝑁)
96 simplr 497 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 𝑘) = (𝐼𝐽))
9771mulid1d 7449 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (𝑁 · 1) = 𝑁)
9897ad3antrrr 476 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 1) = 𝑁)
9995, 96, 983brtr4d 3850 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑁 · 𝑘) < (𝑁 · 1))
100 simpllr 501 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
101100zred 8801 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
102 1red 7447 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
10311nnrpd 9104 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ+)
104103ad3antrrr 476 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℝ+)
105101, 102, 104ltmul2d 9148 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → (𝑘 < 1 ↔ (𝑁 · 𝑘) < (𝑁 · 1)))
10699, 105mpbird 165 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 < 1)
107 simpr 108 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
108107nnge1d 8399 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
109102, 101, 108lensymd 7549 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → ¬ 𝑘 < 1)
110106, 109pm2.21dd 583 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ 𝑘 ∈ ℕ) → 𝐼 = 𝐽)
11193ad3antrrr 476 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (-𝑁 < (𝐼𝐽) ∧ (𝐼𝐽) < 𝑁))
112111simpld 110 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑁 < (𝐼𝐽))
113 simplr 497 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · 𝑘) = (𝐼𝐽))
114112, 113breqtrrd 3846 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑁 < (𝑁 · 𝑘))
11511nnzd 8800 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℤ)
116115adantr 270 . . . . . . . . . . . . . . . . . . 19 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℤ)
117 simpr 108 . . . . . . . . . . . . . . . . . . 19 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
118116, 117zmulcld 8807 . . . . . . . . . . . . . . . . . 18 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · 𝑘) ∈ ℤ)
119118zred 8801 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · 𝑘) ∈ ℝ)
120119ad2antrr 472 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · 𝑘) ∈ ℝ)
12111nnred 8370 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℝ)
122121ad3antrrr 476 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑁 ∈ ℝ)
123120, 122possumd 7987 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (0 < ((𝑁 · 𝑘) + 𝑁) ↔ -𝑁 < (𝑁 · 𝑘)))
124114, 123mpbird 165 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 < ((𝑁 · 𝑘) + 𝑁))
12597eqcomd 2090 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 = (𝑁 · 1))
126125oveq2d 5629 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
127126ad3antrrr 476 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑁 · 𝑘) + 𝑁) = ((𝑁 · 𝑘) + (𝑁 · 1)))
12871ad3antrrr 476 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑁 ∈ ℂ)
129117zcnd 8802 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
130129ad2antrr 472 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
131 1cnd 7448 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ∈ ℂ)
132128, 130, 131adddid 7456 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) = ((𝑁 · 𝑘) + (𝑁 · 1)))
133127, 132eqtr4d 2120 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑁 · 𝑘) + 𝑁) = (𝑁 · (𝑘 + 1)))
134124, 133breqtrd 3844 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 < (𝑁 · (𝑘 + 1)))
135117peano2zd 8804 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℤ)
136116, 135zmulcld 8807 . . . . . . . . . . . . . . . 16 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) ∈ ℤ)
137136zred 8801 . . . . . . . . . . . . . . 15 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
138137ad2antrr 472 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) ∈ ℝ)
139 0red 7433 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 ∈ ℝ)
14071adantr 270 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑁 ∈ ℂ)
141135zcnd 8802 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℂ)
142140, 141mulcomd 7453 . . . . . . . . . . . . . . . 16 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑁 · (𝑘 + 1)) = ((𝑘 + 1) · 𝑁))
143142ad2antrr 472 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) = ((𝑘 + 1) · 𝑁))
144135zred 8801 . . . . . . . . . . . . . . . . 17 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → (𝑘 + 1) ∈ ℝ)
145144ad2antrr 472 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
146 zcn 8688 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
147 1cnd 7448 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℤ → 1 ∈ ℂ)
148146, 147addcomd 7577 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (𝑘 + 1) = (1 + 𝑘))
149147, 146subnegd 7744 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (1 − -𝑘) = (1 + 𝑘))
150148, 149eqtr4d 2120 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℤ → (𝑘 + 1) = (1 − -𝑘))
151150ad3antlr 477 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) = (1 − -𝑘))
152 simpr 108 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑘 ∈ ℕ)
153152nnge1d 8399 . . . . . . . . . . . . . . . . . 18 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ≤ -𝑘)
154 1red 7447 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 1 ∈ ℝ)
155152nnred 8370 . . . . . . . . . . . . . . . . . . 19 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → -𝑘 ∈ ℝ)
156154, 155suble0d 7954 . . . . . . . . . . . . . . . . . 18 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((1 − -𝑘) ≤ 0 ↔ 1 ≤ -𝑘))
157153, 156mpbird 165 . . . . . . . . . . . . . . . . 17 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (1 − -𝑘) ≤ 0)
158151, 157eqbrtrd 3840 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑘 + 1) ≤ 0)
15911nnnn0d 8659 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 𝑁 ∈ ℕ0)
160159nn0ge0d 8662 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → 0 ≤ 𝑁)
161160ad3antrrr 476 . . . . . . . . . . . . . . . 16 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 0 ≤ 𝑁)
162 mulle0r 8340 . . . . . . . . . . . . . . . 16 ((((𝑘 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ ((𝑘 + 1) ≤ 0 ∧ 0 ≤ 𝑁)) → ((𝑘 + 1) · 𝑁) ≤ 0)
163145, 122, 158, 161, 162syl22anc 1173 . . . . . . . . . . . . . . 15 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ((𝑘 + 1) · 𝑁) ≤ 0)
164143, 163eqbrtrd 3840 . . . . . . . . . . . . . 14 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → (𝑁 · (𝑘 + 1)) ≤ 0)
165138, 139, 164lensymd 7549 . . . . . . . . . . . . 13 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → ¬ 0 < (𝑁 · (𝑘 + 1)))
166134, 165pm2.21dd 583 . . . . . . . . . . . 12 (((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) ∧ -𝑘 ∈ ℕ) → 𝐼 = 𝐽)
167 elz 8685 . . . . . . . . . . . . . 14 (𝑘 ∈ ℤ ↔ (𝑘 ∈ ℝ ∧ (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ)))
168167simprbi 269 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ))
169168ad2antlr 473 . . . . . . . . . . . 12 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → (𝑘 = 0 ∨ 𝑘 ∈ ℕ ∨ -𝑘 ∈ ℕ))
17091, 110, 166, 169mpjao3dan 1241 . . . . . . . . . . 11 ((((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) ∧ (𝑁 · 𝑘) = (𝐼𝐽)) → 𝐼 = 𝐽)
171170ex 113 . . . . . . . . . 10 (((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
172171rexlimdva 2485 . . . . . . . . 9 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑁 · 𝑘) = (𝐼𝐽) → 𝐼 = 𝐽))
17368, 172sylbird 168 . . . . . . . 8 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) / 𝑁) ∈ ℤ → 𝐼 = 𝐽))
17465, 173sylbid 148 . . . . . . 7 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼𝐽) mod 𝑁) = 0 → 𝐼 = 𝐽))
17561, 174sylbid 148 . . . . . 6 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) − (𝐽 mod 𝑁)) mod 𝑁) = 0 → 𝐼 = 𝐽))
17654, 175sylbid 148 . . . . 5 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) mod 𝑁) = (0 mod 𝑁) → 𝐼 = 𝐽))
17737, 176syl5 32 . . . 4 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) − (((𝐽 mod 𝑁) + 𝑆) mod 𝑁)) = 0 → 𝐼 = 𝐽))
17836, 177sylbird 168 . . 3 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → ((((𝐼 mod 𝑁) + 𝑆) mod 𝑁) = (((𝐽 mod 𝑁) + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
17925, 178sylbid 148 . 2 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) → 𝐼 = 𝐽))
180 oveq1 5620 . . 3 (𝐼 = 𝐽 → (𝐼 + 𝑆) = (𝐽 + 𝑆))
181180oveq1d 5628 . 2 (𝐼 = 𝐽 → ((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁))
182179, 181impbid1 140 1 ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3o 921  w3a 922   = wceq 1287  wcel 1436  wrex 2356   class class class wbr 3820  (class class class)co 5613  cc 7292  cr 7293  0cc0 7294  1c1 7295   + caddc 7297   · cmul 7299   < clt 7466  cle 7467  cmin 7597  -cneg 7598   / cdiv 8078  cn 8357  0cn0 8606  cz 8683  cq 9036  +crp 9066  ..^cfzo 9481   mod cmo 9657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-cnex 7380  ax-resscn 7381  ax-1cn 7382  ax-1re 7383  ax-icn 7384  ax-addcl 7385  ax-addrcl 7386  ax-mulcl 7387  ax-mulrcl 7388  ax-addcom 7389  ax-mulcom 7390  ax-addass 7391  ax-mulass 7392  ax-distr 7393  ax-i2m1 7394  ax-0lt1 7395  ax-1rid 7396  ax-0id 7397  ax-rnegex 7398  ax-precex 7399  ax-cnre 7400  ax-pre-ltirr 7401  ax-pre-ltwlin 7402  ax-pre-lttrn 7403  ax-pre-apti 7404  ax-pre-ltadd 7405  ax-pre-mulgt0 7406  ax-pre-mulext 7407  ax-arch 7408
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-iun 3715  df-br 3821  df-opab 3875  df-mpt 3876  df-id 4094  df-po 4097  df-iso 4098  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-res 4423  df-ima 4424  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-fv 4989  df-riota 5569  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-1st 5868  df-2nd 5869  df-pnf 7468  df-mnf 7469  df-xr 7470  df-ltxr 7471  df-le 7472  df-sub 7599  df-neg 7600  df-reap 7993  df-ap 8000  df-div 8079  df-inn 8358  df-n0 8607  df-z 8684  df-uz 8952  df-q 9037  df-rp 9067  df-fz 9357  df-fzo 9482  df-fl 9605  df-mod 9658
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator