LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\mathbb Z$ . If $a\equiv a'\pmod n$ and $b\equiv b'\pmod n$ , then

$a+b\equiv a'+b'\pmod n,\qquad a-b\equiv a'-b'\pmod n,\qquad ab\equiv a'b'\pmod n.$

In particular $-a\equiv-a'\pmod n$ , and for every $k\in\mathbb 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\pmod n$ .

Facts & Assumptions

Given: Integers $n,a,a',b,b'$ with $a\equiv a'\pmod n$ and $b\equiv b'\pmod n$ .

[F1]

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

[L1]

If $d\mid u$ and $d\mid v$ , then $d\mid ux+vy$ for all integers $x,y$ ; also $d\mid u$ implies $d\mid uw$ and $d\mid-u$ (Divisibility is reflexive and transitive on $\mathbb{Z}$ , and is linear: if $d \mid a$ and $d \mid b$ then $d \mid ax + by$ for all integers $x, y$ ; also $d \mid a$ implies $d \mid ac$ , $-d \mid a$ and $d \mid -a$ ).

[L2]

$\mathbb 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 $\mathbb Z$ satisfy $x^0=1$ and $x^{k+1}=x^kx$ (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\mid(a-a')$ and $n\mid(b-b')$ .

givenF1

2.1

Since $(a+b)-(a'+b')=(a-a')+(b-b')$ , linearity gives $a+b\equiv a'+b'\pmod n$ .

step 1.1F1L1L2

2.2

Since $(a-b)-(a'-b')=(a-a')-(b-b')$ , linearity gives $a-b\equiv a'-b'\pmod n$ ; also $n\mid(a-a')$ gives $n\mid-(a-a')=(-a)-(-a')$ , so $-a\equiv-a'\pmod n$ .

step 1.1F1L1L2

2.3

The identity $ab-a'b'=a(b-b')+b'(a-a')$ and linearity give $n\mid(ab-a'b')$ , hence $ab\equiv a'b'\pmod 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^ka\equiv(a')^ka'=(a')^{k+1}$ . Thus it holds for every $k\in\mathbb N$ by induction.

step 2.3F2L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 46 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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