This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addmodlteqALT

Description: Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq based on the "divides" relation. (Contributed by AV, 14-Mar-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion addmodlteqALT ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) )
2 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
3 simplrr ⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → 𝑁 ∈ ℕ )
4 nn0z ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
5 4 ad2antrl ⊢ ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) → 𝐼 ∈ ℤ )
6 zaddcl ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝐼 + 𝑆 ) ∈ ℤ )
7 5 6 sylan ⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝐼 + 𝑆 ) ∈ ℤ )
8 zaddcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( 𝐽 + 𝑆 ) ∈ ℤ )
9 8 adantlr ⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝐽 + 𝑆 ) ∈ ℤ )
10 3 7 9 3jca ⊢ ( ( ( 𝐽 ∈ ℤ ∧ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) )
11 10 exp31 ⊢ ( 𝐽 ∈ ℤ → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
12 2 11 syl ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
13 12 com12 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
14 13 3adant3 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐼 < 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
15 1 14 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝑆 ∈ ℤ → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) ) ) )
16 15 3imp ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) )
17 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐼 + 𝑆 ) ∈ ℤ ∧ ( 𝐽 + 𝑆 ) ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ) )
18 16 17 syl ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ) )
19 elfzoel2 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
20 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
21 20 subid1d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 0 ) = 𝑁 )
22 21 eqcomd ⊢ ( 𝑁 ∈ ℤ → 𝑁 = ( 𝑁 − 0 ) )
23 19 22 syl ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝑁 = ( 𝑁 − 0 ) )
24 23 3ad2ant1 ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → 𝑁 = ( 𝑁 − 0 ) )
25 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝐼 ∈ ℤ )
26 25 zcnd ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑁 ) → 𝐼 ∈ ℂ )
27 2 zcnd ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℂ )
28 zcn ⊢ ( 𝑆 ∈ ℤ → 𝑆 ∈ ℂ )
29 pnpcan2 ⊢ ( ( 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) = ( 𝐼 − 𝐽 ) )
30 26 27 28 29 syl3an ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) = ( 𝐼 − 𝐽 ) )
31 24 30 breq12d ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( 𝑁 ∥ ( ( 𝐼 + 𝑆 ) − ( 𝐽 + 𝑆 ) ) ↔ ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ) )
32 fzocongeq ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ↔ 𝐼 = 𝐽 ) )
33 32 3adant3 ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( 𝑁 − 0 ) ∥ ( 𝐼 − 𝐽 ) ↔ 𝐼 = 𝐽 ) )
34 18 31 33 3bitrd ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑁 ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝐼 + 𝑆 ) mod 𝑁 ) = ( ( 𝐽 + 𝑆 ) mod 𝑁 ) ↔ 𝐼 = 𝐽 ) )