Metamath Proof Explorer

Theorem submodaddmod

Description: Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025)

Ref Expression
Assertion submodaddmod ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐶 ) mod 𝑁 ) ↔ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℂ )
3 2 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
4 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5 4 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℂ )
6 5 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
7 zcn ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℂ )
9 8 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐶 ∈ ℂ )
10 3 6 9 pnncand ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐵 + 𝐶 ) )
11 zaddcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 + 𝐶 ) ∈ ℤ )
12 11 zcnd ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
13 12 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
15 3 14 pncan2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) − 𝐴 ) = ( 𝐵 + 𝐶 ) )
16 10 15 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) − 𝐴 ) )
17 16 breq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝑁 ∥ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) − 𝐴 ) ) )
18 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝑁 ∈ ℕ )
19 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
20 19 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
21 20 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
22 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
23 22 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
24 23 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 − 𝐶 ) ∈ ℤ )
25 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( 𝐴 − 𝐶 ) ∈ ℤ ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐶 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ) )
26 18 21 24 25 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐶 ) mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐶 ) ) ) )
27 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℤ )
28 simp2 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℤ )
29 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℤ )
30 28 29 zaddcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 + 𝐶 ) ∈ ℤ )
31 27 30 zaddcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + ( 𝐵 + 𝐶 ) ) ∈ ℤ )
32 31 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 + ( 𝐵 + 𝐶 ) ) ∈ ℤ )
33 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
34 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 + ( 𝐵 + 𝐶 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) − 𝐴 ) ) )
35 18 32 33 34 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) − 𝐴 ) ) )
36 17 26 35 3bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = ( ( 𝐴 − 𝐶 ) mod 𝑁 ) ↔ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )