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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝐵 · 𝐶 ) ↔ ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℤ )
2 1 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℂ )
3 2 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
4 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
5 4 zcnd ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
6 5 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
7 6 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
8 3 7 pncan2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) − 𝐴 ) = ( 𝐵 · 𝐶 ) )
9 8 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐵 · 𝐶 ) = ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) − 𝐴 ) )
10 9 breq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝐵 · 𝐶 ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) − 𝐴 ) ) )
11 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝑁 ∈ ℕ )
12 4 3adant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
13 1 12 zaddcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 + ( 𝐵 · 𝐶 ) ) ∈ ℤ )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 + ( 𝐵 · 𝐶 ) ) ∈ ℤ )
15 1 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
16 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 + ( 𝐵 · 𝐶 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) − 𝐴 ) ) )
17 11 14 15 16 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) − 𝐴 ) ) )
18 10 17 bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ) → ( 𝑁 ∥ ( 𝐵 · 𝐶 ) ↔ ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) mod 𝑁 ) = ( 𝐴 mod 𝑁 ) ) )