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

Coprime(a,b)PowerDivides(p,e,n)PrimeDivisorSupport(n,pb,pc,l)

Checked theorems using this definition

TP0026 · totient_divisor_reflexiveTP0027 · totient_coprime_divisor_rightTP0029 · totient_prime_coprime_iff_nondivisorTP002A · totient_coprime_repeated_factorTP002D · totient_nonzero_prime_block_offset_not_divisibleTP002F · totient_unit_count_repeated_prime_factorTP0037 · totient_repeated_prime_factorTP003C · totient_coprime_divisor_leftTP003D · totient_coprime_multiplication_prime_step