PD0003

Dvd(d,n)

The natural number d divides n.

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

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)DivisorFactorPair(m,n,d,a,b)JordanTupleAllDivisible(d,b,c,k)JordanPrimitiveTuple(n,b,c,k)

Checked theorems using this definition

JT0006 · jordan_primitive_tuple_divisor_modulusJT0007 · jordan_tuple_divisor_downwardJT000D · jordan_divisibility_congruence_transportJT0011 · jordan_tuple_all_divisible_extendJT0012 · jordan_tuple_all_divisible_decidableJT0013 · jordan_tuple_divisor_test_decidableJT0014 · jordan_tuple_primitive_bounded_decidableJT0015 · jordan_primitive_tuple_decidableJT0031 · jordan_tuple_congruence_divisorJT005D · jordan_primitive_tuple_avoids_prime_common_divisorJT005E · jordan_prime_power_tuple_primitive_of_not_all_divisible