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

Metamath Proof Explorer

Theorem addmulmodb

Description: An integer plus a product is itself modulo a positive integer iff the product is divisible by the positive integer. (Contributed by AV, 8-Sep-2025)

Ref Expression
Assertion addmulmodb ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → N ∥ B ⁢ C ↔ A + B ⁢ C mod N = A mod N

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ
2 1 zcnd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℂ
3 2 adantl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℂ
4 zmulcl ⊢ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C ∈ ℤ
5 4 zcnd ⊢ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C ∈ ℂ
6 5 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C ∈ ℂ
7 6 adantl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C ∈ ℂ
8 3 7 pncan2d ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A + B ⁢ C - A = B ⁢ C
9 8 eqcomd ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C = A + B ⁢ C - A
10 9 breq2d ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → N ∥ B ⁢ C ↔ N ∥ A + B ⁢ C - A
11 simpl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → N ∈ ℕ
12 4 3adant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ⁢ C ∈ ℤ
13 1 12 zaddcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A + B ⁢ C ∈ ℤ
14 13 adantl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A + B ⁢ C ∈ ℤ
15 1 adantl ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ
16 moddvds ⊢ N ∈ ℕ ∧ A + B ⁢ C ∈ ℤ ∧ A ∈ ℤ → A + B ⁢ C mod N = A mod N ↔ N ∥ A + B ⁢ C - A
17 11 14 15 16 syl3anc ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A + B ⁢ C mod N = A mod N ↔ N ∥ A + B ⁢ C - A
18 10 17 bitr4d ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → N ∥ B ⁢ C ↔ A + B ⁢ C mod N = A mod N