PD0005

Coprime(a,b)

Every common divisor of a and b is one.

Conservative notation; not a theorem, primitive, or axiom.

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

Definition in prerequisite notation

∀ d. Dvd(d,a) → Dvd(d,b) → d = 1

Only definitions earlier in this acyclic notation graph are used here.

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

MultiplicativePrefix(N,F)DirichletCoprimeProductData(N,F,G,m,n,A,B,T,Q,r,s)

Checked theorems using this definition

MX0004 · signed_multiplicative_coprime_productMX0005 · signed_multiplicative_introMX0009 · signed_multiplicative_product_values_existMX000C · coprime_divisor_gcd_productMX000D · coprime_divisor_factor_pair_coordinatesMX000E · coprime_divisor_factor_pair_uniqueMX000F · coprime_divisor_factor_pair_existsMX0010 · coprime_divisor_factor_pair_boundsMX0011 · coprime_divisor_factor_pair_exists_uniqueMX0012 · coprime_divisor_factor_pair_cofactorsMX004F · dirichlet_multiplicative_pair_factorizationMX0050 · dirichlet_multiplicative_pair_entryMX0054 · dirichlet_coprime_grid_support_coveringMX0056 · dirichlet_coprime_product_data_constructMX0057 · dirichlet_convolution_multiplicative_values