PD0005 — Coprime(a,b)

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Hygienic expanded first-order definition

forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Dvd(d,n)

Definitions depending on this notation

CRTPairwiseCoprimePrefix(b,c,l)

Checked theorems using this definition

CR0009 · crt_pairwise_coprime_prefix_last CR0012 · crt_pairwise_coprime_prefix_product_coprime_last

Separate complete second-wave branches: Full G011 proof · Alpha v27.