LemmaStatement: AI-adaptedProof: AI-generatedSession-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.

For a finite pairwise-coprime list of positive integers, the product divides every common multiple, and each initial product is coprime to every remaining modulus

Statement

Let $n_0,\ldots,n_{r-1}$ be a finite list of positive integers such that $\gcd(n_i,n_j)=1$ whenever $i\ne j$ . Put $P_k:=\prod_{i<k}n_i$ , with $P_0=1$ .

For every $k\le j<r$ , $\gcd(P_k,n_j)=1$ .
If every $n_i$ divides an integer $M$ , then $P_r\mid M$ .

The products are finite monoid products (The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

Facts & Assumptions

Given: A natural $r$ , a pairwise-coprime list of positive integers $n_0,\ldots,n_{r-1}$ , its initial products $P_k$ , and an integer $M$ divisible by every list member.

[L1]

A prime dividing a finite product of integers divides one of its factors (If a prime $p$ divides a finite product $\prod_{i<n} a_i$ of integers then $p \mid a_i$ for some $i < n$ ; at $n = 0$ the product is $1$ and the hypothesis cannot hold).

[L2]

Every integer greater than $1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime).

[L3]

If $u\mid M$ , $v\mid M$ , and $\gcd(u,v)=1$ , then $uv\mid M$ (If $\gcd(a,b) = 1$ and $a \mid bc$ then $a \mid c$ ; and if $a \mid c$ , $b \mid c$ and $\gcd(a,b) = 1$ then $ab \mid c$ ).

[L4]

Finite products have empty value $1$ and satisfy $P_{k+1}=P_kn_k$ (The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either).

[L5]

Coprime integers have gcd $1$ , whose only positive divisors are $1$ (Coprime integers: $\gcd(a,b) = 1$ , Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

[L6]

Induction proves a statement at every natural number from its base case and successor implication (The principle of mathematical induction).

Proof

technique · induction

1.1

Fix $k\le j<r$ . If $\gcd(P_k,n_j)>1$ , [L2] supplies a prime $q$ dividing this gcd. Then $q\mid P_k$ , so [L1] gives an $i<k\le j$ with $q\mid n_i$ ; also $q\mid n_j$ , contradicting $\gcd(n_i,n_j)=1$ because $i\ne j$ and the positive prime $q>1$ would divide that gcd. Hence $\gcd(P_k,n_j)=1$ .

L1L2L5

1.2

At $k=0$ , $P_0=1$ divides $M$ .

baseL4

2.1

Assume $P_k\mid M$ for some $k<r$ . The hypothesis gives $n_k\mid M$ , and step 1.1 gives $\gcd(P_k,n_k)=1$ ; hence [L3] gives $P_kn_k=P_{k+1}\mid M$ .

ihstep 1.1L3L4

3.1

Induction using steps 1.2 and 2.1 yields $P_k\mid M$ for every $k\le r$ , and in particular $P_r\mid M$ ; together with step 1.1 this proves both clauses.

step 1.1step 1.2step 2.1L6discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 27 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, The Chinese Remainder Theorem (standard reference, not scraped)