LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Congruent integers may be added, subtracted and multiplied: representative changes preserve both arithmetic operations

Statement

Let $n, a, a^{'}, b, b^{'} \in Z$ . If $a \equiv a^{'} (m o d n)$ and $b \equiv b^{'} (m o d n)$ , then

$a + b \equiv a^{'} + b^{'} (m o d n), a - b \equiv a^{'} - b^{'} (m o d n), a b \equiv a^{'} b^{'} (m o d n) .$

In particular $- a \equiv - a^{'} (m o d n)$ , and for every $k \in N$ the natural powers of Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ satisfy $a^{k} \equiv (a^{'})^{k} (m o d n)$ .

Facts & Assumptions

Given: Integers $n, a, a^{'}, b, b^{'}$ with $a \equiv a^{'} (m o d n)$ and $b \equiv b^{'} (m o d n)$ .

[F1]

$u \equiv v (m o d n)$ means $n ∣ (u - v)$ (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ ).

[L1]

If $d ∣ u$ and $d ∣ v$ , then $d ∣ u x + v y$ for all integers $x, y$ ; also $d ∣ u$ implies $d ∣ u w$ and $d ∣ - u$ (Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ ).

[L2]

$Z$ is a commutative ring, so subtraction, distributivity and the identities used below are valid (The integers form a commutative ring).

[F2]

Natural powers in the multiplicative monoid of $Z$ satisfy $x^{0} = 1$ and $x^{k + 1} = x^{k} x$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

[L3]

A property true at $0$ and inherited by successors holds for every natural number (The principle of mathematical induction).

Proof

technique · direct

1.1

By [F1], $n ∣ (a - a^{'})$ and $n ∣ (b - b^{'})$ .

givenF1

2.1

Since $(a + b) - (a^{'} + b^{'}) = (a - a^{'}) + (b - b^{'})$ , linearity gives $a + b \equiv a^{'} + b^{'} (m o d n)$ .

step 1.1F1L1L2

2.2

Since $(a - b) - (a^{'} - b^{'}) = (a - a^{'}) - (b - b^{'})$ , linearity gives $a - b \equiv a^{'} - b^{'} (m o d n)$ ; also $n ∣ (a - a^{'})$ gives $n ∣ - (a - a^{'}) = (- a) - (- a^{'})$ , so $- a \equiv - a^{'} (m o d n)$ .

step 1.1F1L1L2

2.3

The identity $a b - a^{'} b^{'} = a (b - b^{'}) + b^{'} (a - a^{'})$ and linearity give $n ∣ (a b - a^{'} b^{'})$ , hence $a b \equiv a^{'} b^{'} (m o d n)$ .

step 1.1F1L1L2

3.1

The power claim holds at $k = 0$ because $a^{0} = 1 = (a^{'})^{0}$ . If it holds at $k$ , then step 2.3 applied to $a^{k} \equiv (a^{'})^{k}$ and $a \equiv a^{'}$ gives $a^{k + 1} = a^{k} a \equiv (a^{'})^{k} a^{'} = (a^{'})^{k + 1}$ . Thus it holds for every $k \in N$ by induction.

step 2.3F2L3∎

Depends on

Used by

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Modular Arithmetic (standard reference, not scraped)