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 𝑁 ) ↔ 𝐼 = 𝐽 ) )