LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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}, \dots, n_{r - 1}$ be a finite list of positive integers such that $\gcd (n_{i}, n_{j}) = 1$ whenever $i \neq j$ . Put $P_{k} : = \prod_{i < k} n_{i}$ , with $P_{0} = 1$ .

For every $k \leq j < r$ , $\gcd (P_{k}, n_{j}) = 1$ .
If every $n_{i}$ divides an integer $M$ , then $P_{r} ∣ M$ .

The products are finite monoid products (The product $g_{0} g_{1} \dots 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}, \dots, 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 ∣ 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 ∣ M$ , $v ∣ M$ , and $\gcd (u, v) = 1$ , then $u v ∣ M$ (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ).

[L4]

Finite products have empty value $1$ and satisfy $P_{k + 1} = P_{k} n_{k}$ (The product $g_{0} g_{1} \dots 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 \leq j < r$ . If $\gcd (P_{k}, n_{j}) > 1$ , [L2] supplies a prime $q$ dividing this gcd. Then $q ∣ P_{k}$ , so [L1] gives an $i < k \leq j$ with $q ∣ n_{i}$ ; also $q ∣ n_{j}$ , contradicting $\gcd (n_{i}, n_{j}) = 1$ because $i \neq 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} ∣ M$ for some $k < r$ . The hypothesis gives $n_{k} ∣ M$ , and step 1.1 gives $\gcd (P_{k}, n_{k}) = 1$ ; hence [L3] gives $P_{k} n_{k} = P_{k + 1} ∣ M$ .

ihstep 1.1L3L4

3.1

Induction using steps 1.2 and 2.1 yields $P_{k} ∣ M$ for every $k \leq r$ , and in particular $P_{r} ∣ M$ ; together with step 1.1 this proves both clauses.

step 1.1step 1.2step 2.1L6discharge-induction∎

Depends on

Used by

Dependency tree · two levels

43 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, The Chinese Remainder Theorem (standard reference, not scraped)