PD0003

Dvd(d,n)

The natural number d divides n.

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

∃ k. n = d · k

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

Hygienic expanded first-order definition 
exists k. n = d * k

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

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

PowerDivides(p,e,n)PrimeDivisorSupport(n,pb,pc,l)

Checked theorems using this definition

PV0002 · prime_valuation_zero_of_nondivisorPV0003 · prime_valuation_nondivisor_of_zeroPV0006 · pow_positive_exponent_base_dividesPV0008 · prime_divisor_of_prime_powerPV000B · prime_exponent_entries_prime_dividesPV000C · prime_exponent_entries_restore_prime_powerPV0011 · prime_valuation_strict_cofactor_existsPV0012 · prime_valuation_support_append_full_powerPV0013 · prime_valuation_support_bounded_exists