ExampleConstruction: Literature-sourcedVerification: 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.

A modulus $n>1$ is composite exactly when two nonzero classes in $\mathbb{Z}/n$ have product $[0]_n$

Example

For every integer $n>1$ , the following are equivalent:

$n$ is composite.
There are nonzero classes $u,v\in\mathbb Z/n$ with $uv=[0]_n$ .

Facts & Assumptions

Given: An integer $n>1$ .

[L1]

A positive integer greater than $1$ is composite exactly when it has a divisor $d$ with $1<d<n$ ; otherwise it is prime (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L2]

Products in $\mathbb Z/n$ are computed on representatives, and the quotient has standard representatives $0,\ldots,n-1$ (Addition and multiplication on $\mathbb{Z}/n$ by $[a]_n+[b]_n=[a+b]_n$ and $[a]_n[b]_n=[ab]_n$ , For $n\ge 1$ , every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$ , so $\lvert\mathbb{Z}/n\rvert=n$ ; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$ ).

[L3]

A class $[a]_n$ is a unit exactly when $\gcd(a,n)=1$ , and the gcd is a nonnegative common divisor that is positive when its arguments are not both zero (For $n\ge1$ , $[a]_n$ is a unit if and only if $\gcd(a,n)=1$ , Common divisor, and the greatest common divisor $\gcd(a,b)$ , with the convention $\gcd(0,0) := 0$ ).

Verification

technique · direct

1.1

If $n$ is composite, write $n=ab$ with $1<a<n$ and $1<b<n$ . Then $[a]_n$ and $[b]_n$ are nonzero standard classes, but $[a]_n[b]_n=[ab]_n=[n]_n=[0]_n$ .

L1L2

1.2

Conversely, suppose nonzero classes have product zero and choose their standard representatives $a,b$ , so $0<a,b<n$ and $n\mid ab$ . The class $[a]_n$ cannot be a unit, because multiplying an equation $[a]_n[b]_n=[0]_n$ by its inverse would give $[b]_n=[0]_n$ . Hence $d:=\gcd(a,n)>1$ by [L3]. Since $d\mid a$ and $0<a<n$ , one also has $d<n$ , so $d$ is a nontrivial divisor of $n$ and $n$ is composite by [L1].

L1L2L3

2.1

Steps 1.1 and 1.2 prove the equivalence.

step 1.1step 1.2∎

Depends on

Used by

False: [a]ₙ[b]ₙ=[0]ₙ always implies [a]ₙ=[0]ₙ or [b]ₙ=[0]ₙ False statement

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 78 results over 22 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)
University of Colorado, proof practice on zero divisors (standard reference, not scraped)

A modulus n>1n>1n>1 is composite exactly when two nonzero classes in Z/n\mathbb{Z}/nZ/n have product [0]n[0]_n[0]n​