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. Exact original first-admission records.

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)

Checked theorems using this definition

TP0001 · totient_coprime_decidableTP0002 · totient_unit_bit_choice_existsTP0003 · totient_unit_bit_choice_functionalTP0006 · totient_unit_prefix_entryTP0007 · totient_unit_prefix_extendTP0008 · totient_unit_prefix_existsTP0009 · totient_unit_prefix_all_bitsTP000F · totient_unit_count_succ_decomposeTP0010 · totient_unit_count_succ_introTP0011 · totient_unit_choice_mod_oneTP0012 · totient_unit_count_mod_oneTP001D · totient_unit_choices_equal_of_equivalenceTP001E · totient_unit_count_interval_balanceTP001F · totient_coprime_periodicTP0022 · totient_unit_count_pointwise_equalTP0027 · totient_coprime_divisor_rightTP0028 · totient_coprime_product_iffTP0029 · totient_prime_coprime_iff_nondivisorTP002A · totient_coprime_repeated_factorTP002B · totient_coprime_cancel_unit_factorTP002C · totient_prime_multiple_is_not_unitTP002E · totient_prime_block_positive_offset_unitsTP0030 · totient_unit_choice_transportTP0033 · totient_new_prime_block_count_balanceTP0034 · totient_new_prime_multiple_blocks_balanceTP0035 · totient_unit_count_new_prime_balanceTP0036 · totient_unit_count_new_prime_factorTP0038 · totient_new_prime_factorTP003C · totient_coprime_divisor_leftTP003D · totient_coprime_multiplication_prime_stepTP003E · totient_coprime_multiplicative_from_prime_listTP003F · totient_coprime_multiplicativeTP0045 · totient_prime_support_powers_pairwise_coprimeTP0046 · totient_pairwise_coprime_product_fold