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

UnitBitPrefix(n,b,c,l)UnitProductFactor(m,i,v)UnitScaledPrefix(a,m,b,c,d,e,l)

Checked theorems using this definition

EU0001 · euler_coprime_mod_transportEU0002 · euler_multiplier_coprime_iffEU0004 · euler_modular_unit_coprimeEU0005 · euler_coprime_modular_unitEU000B · euler_multiplier_prefix_bounded_injectiveEU000C · euler_multiplier_prefix_permutationEU000D · euler_multiplier_permutation_existsEU000E · euler_unit_product_factor_existsEU000F · euler_unit_product_factor_unit_valueEU0010 · euler_unit_product_factor_nonunit_valueEU0011 · euler_unit_product_factor_coprimeEU0017 · euler_unit_product_coprimeEU0018 · euler_unit_factor_scaled_congruenceEU0019 · euler_nonunit_factor_unchanged_congruenceEU001B · euler_unit_product_reindex_scaleEU001D · euler_coprime_weighted_product_cancelEU001E · euler_unit_count_product_balanceEU001F · euler_coprime_totient_power_valueEU0020 · euler_coprime_totient_power