ND0281

DivisorComplement(n,d,q)

At a positive divisor d, a genuine product witness n=d*q specifies the complementary quotient. Zero and nondivisors are fixed. For n>0, totality, reversibility and bounds are proved separately, not assumed in this graph.

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 = 0 ∧ n = d · q ∨ (d = 0 ∨ ¬Dvd(d,n)) ∧ q = d

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

Hygienic expanded first-order definition 
(((~(((d))=0)) /\ (((n))=((d))*((q))))) \/ (((((d))=0 \/ ~(exists pvs_factor_lowercontinuationnondivisor. ((n)) = ((d)) * pvs_factor_lowercontinuationnondivisor)) /\ (((q))=((d)))))

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

DivisorComplementPrefix(n,b,c,l)

Checked theorems using this definition

DI0002 · divisor_complement_existsDI0003 · divisor_complement_functionalDI0004 · divisor_complement_positive_equationDI0005 · divisor_complement_symmetricDI0006 · divisor_complement_boundedDI0007 · divisor_complement_prefix_existsDI0008 · divisor_complement_prefix_lookupDI0009 · divisor_complement_prefix_permutationDI000B · divisor_complement_prefix_involutionDI000C · divisor_complement_prefix_positive_quotient