Congruence modulo a positive modulus: the remainder definition, the witness form, preservation by operations and the limits of cancellation

Goal and scope

From the MKO's definition (n>0, a≡b (mod n) ⇔ a mod n=b mod n): (1) decide 100≡23 (mod 7); (2) prove that this is equivalent to the witness form 'there are naturals k, l with a+nk=b+nl', and give witnesses for 100 and 23; (3) explain why congruence is an equivalence relation; (4) prove that addition and multiplication preserve congruence, and from 15≡1 (mod 7) obtain 115≡24 and 1500≡23 (mod 7); (5) use 2·3≡2·0 (mod 6) to show that a common factor cannot be cancelled unconditionally; (6) explain why different moduli cannot be chained, and why the modulus 0 is excluded.

Treats natural a, b and a positive modulus n only (MKO assumptions a1 and a2); remainders are defined by the division algorithm. Proves that the two definitions agree, that congruence is an equivalence relation, and that addition and multiplication preserve it. The positive result that cancellation is valid when gcd(c,n)=1 is not proved here. Negative integers and the modulus 0 are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• division_algorithm
• distributive
• eq_refl_symm_trans
• numeric_evaluation

• G1 — a and b are natural numbers and the modulus n is a positive natural (MKO assumption a1); this entry excludes n=0 (MKO assumption a2).
• G2 — a mod n is the remainder of the division algorithm: the unique r with a=nq+r and 0≤r<n; for natural a the quotient q is natural too.
• G3 — Examples: 100, 23, 15, 1 modulo 7; 2·3 and 2·0 modulo 6; 100, 23, 5 with moduli 7 and 3.

• a\equiv b\pmod n — a is congruent to b modulo n
• a\bmod n — the remainder of a on division by n, 0≤a mod n<n
• k,\ l — the naturals in the witness form
• n — the positive modulus

Rules and sources

• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• mko_cong_def · cited — For natural numbers a, b and a positive natural n, a≡b (mod n) exactly when a mod n=b mod n. Equivalently, there are natural k, l with a+n·k=b+n·l. · mko-modular-congruence
• L_shift · lemma — For n>0 and naturals x, m: (x+n·m) mod n=x mod n.
• L_witness · lemma — For n>0 and naturals a, b: a mod n=b mod n ⇔ there are naturals k, l with a+nk=b+nl.
• L_add_mul · lemma — If a≡b (mod n) and c≡d (mod n), then a+c≡b+d (mod n) and ac≡bd (mod n).

Main derivation

a\equiv b\pmod n

a\bmod n=b\bmod n\quad(n>0)

100

100=7\cdot 14+2,\ 0\le 2<7,\ 100\bmod 7=2

23

23=7\cdot 3+2,\ 23\bmod 7=2

100\bmod 7=2=23\bmod 7

100\equiv 23\pmod 7

(x+nm)\bmod n

x\bmod n

a\bmod n=b\bmod n

\exists k,l\in\mathbb{N}:\ a+nk=b+nl

100=7\cdot 14+2,\ 23=7\cdot 3+2

100+7\cdot 3=23+7\cdot 14=121;\quad 100+7\cdot 0=23+7\cdot 11

\equiv\pmod n\ \text{for one fixed}\ n

\text{reflexive, symmetric, transitive}

15=7\cdot 2+1,\ 1=7\cdot 0+1

15\equiv 1\pmod 7

a\equiv b,\ c\equiv d\pmod n

a+c\equiv b+d,\ ac\equiv bd\pmod n

100\equiv 23,\ 15\equiv 1\pmod 7

115\equiv 24,\quad 1500\equiv 23\pmod 7

2\cdot 3\equiv 2\cdot 0\pmod 6

3\not\equiv 0\pmod 6

100\equiv 23\pmod 7,\ 23\equiv 5\pmod 3

100\not\equiv 5\pmod 7,\ 100\not\equiv 5\pmod 3

Substeps and lemmas

x=nq+r,\ 0\le r<n

x+nm=n(q+m)+r

x+nm=n(q+m)+r,\ 0\le r<n

(x+nm)\bmod n=r=x\bmod n

a=nq+r,\ b=nq'+r

a+nq'=b+nq

a+nk=b+nl

a\bmod n=(a+nk)\bmod n=(b+nl)\bmod n=b\bmod n

a=nq_1+r,\ b=nq_2+r,\ c=nq_3+s,\ d=nq_4+s

(a+c)\bmod n=(r+s)\bmod n=(b+d)\bmod n

ac=(nq_1+r)(nq_3+s)

ac=n(nq_1q_3+q_1s+rq_3)+rs,\ (ac)\bmod n=(rs)\bmod n=(bd)\bmod n

Reverse audits

• S13 · premise_audit · S08, numeric_evaluation — A concrete counterexample showing that the premise 'same modulus' in transitivity cannot be dropped.
• S12 · premise_audit · S01, numeric_evaluation — One counterexample refutes 'unconditional cancellation'; this guide does not prove that cancellation is valid when gcd(c,n)=1.
• S11 · premise_audit · S10, forall_elim, numeric_evaluation — An instance of the general result; the direct recomputation is a check and does not replace the proof of S10.
• S10.2 · premise_audit · S05, distributive — Only distributivity and L_shift are used; L_add_mul itself is not used.
• S10.1 · premise_audit · S05, distributive — Only L_shift and distributivity are used; L_add_mul itself is not used.
• S10 · premise_audit · L_add_mul — No converse is claimed: ac≡bd does not give a≡b or c≡d (S12).
• S09 · premise_audit · division_algorithm, mko_cong_def — Both remainders are computed directly.
• S08 · premise_audit · S01, eq_refl_symm_trans — Transitivity requires the same n in both congruences; remainders for different moduli are not the same quantity (S13).
• S07 · premise_audit · S06, exists_intro, numeric_evaluation — Existence needs only one pair; two are given to show non-uniqueness.
• S06.2 · premise_audit · S05, eq_congruence — It uses the already proved L_shift, not L_witness itself.
• S06.1 · premise_audit · distributive, add_comm, exists_intro — Only commutativity and associativity of addition and ∃-introduction are used; the lemma itself is not used.
• S06 · inverse_equivalence · L_witness — The two directions are proved in S06.1 and S06.2.
• S05.2 · premise_audit · division_algorithm — The key is uniqueness together with 0≤r<n; the lemma itself is not used.
• S05.1 · premise_audit · distributive, add_comm, add_assoc — Only distributivity and the laws of addition are used (N21 is a grid identity check); the lemma itself is not used.
• S05 · inverse_equivalence · L_shift — Both sides are the same number, so the equality holds both ways.
• S04 · inverse_equivalence · mko_cong_def — The definition is two-way: congruence holds exactly when the remainders are equal.
• S03 · premise_audit · division_algorithm, numeric_evaluation — As in S02.
• S02 · premise_audit · division_algorithm, numeric_evaluation — The remainder must lie in 0 to 6; this makes it unique.
• S01 · premise_audit · G1, G2, mko_cong_def — This step only unfolds the definition; n>0 is needed for the remainder to be defined.

Error controls and negative controls

Do not mix moduli

One misconception the MKO names: mixing moduli. 100≡23 (mod 7) and 23≡5 (mod 3) cannot be chained into 100≡5; in fact it fails for both moduli (S13).

No unconditional cancellation

Another misconception the MKO names: cancelling a common factor from both sides unconditionally. 2·3≡2·0 (mod 6) but 3≢0 (mod 6) (S12). Cancellation requires considering the gcd of c and n; this guide does not prove the positive condition.

The modulus 0 is excluded

The third misconception the MKO names: allowing a zero modulus. The division algorithm needs a positive divisor, so a mod 0 is undefined in this entry; programming languages treat x mod 0 in different ways (some raise an error), and this entry deliberately adopts none of them (MKO assumption a2).

Congruence is not numerical equality

100≡23 (mod 7) while 100≠23. Congruence compares remainders for a fixed modulus (MKO paragraph 0).

• From 2·3≡2·0 (mod 6), cancelling 2 gives 3≡0 (mod 6) → reject — 3 mod 6=3≠0; gcd(2,6)=2≠1.
• 100≡23 (mod 7) and 23≡5 (mod 3), so 100≡5 (mod 7) → reject — 100 mod 7=2 and 5 mod 7=5; transitivity holds only for the same modulus.
• Since some programming conventions give 7 mod 0=7, this entry can decide 7≡7 (mod 0) → reject — This entry requires n to be a positive natural; n=0 is deliberately excluded.
• 100≡23 (mod 7), so 100=23 → reject — Congruence only means equal remainders; 100≠23.
• The witness (k,l) for 100≡23 (mod 7) is unique → reject — Both (3,14) and (0,11) work.

Result and limitations

100≡23 (mod 7) because both leave remainder 2 on division by 7; the remainder definition and the witness form are equivalent, and witnesses for 100 and 23 are (k,l)=(3,14) or (0,11). For a fixed modulus congruence is an equivalence relation preserved by addition and multiplication: 115≡24 and 1500≡23 (mod 7). 2·3≡2·0 (mod 6) but 3≢0 (mod 6), so a common factor cannot be cancelled unconditionally; congruences with different moduli cannot be chained; the modulus 0 is excluded.

• The positive cancellation result (if gcd(c,n)=1 then ca≡cb ⇒ a≡b) is not proved here.
• The division algorithm (with uniqueness) is cited as a prerequisite; that the quotient of a natural a is natural is shown in the natural-divisibility guide.

Verification and source binding

21 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 2e962d623d84262cb743a552037824dee16a1980f16f38b26d7bf9aeaa025587
• original source SHA-256: 2e962d623d84262cb743a552037824dee16a1980f16f38b26d7bf9aeaa025587
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)