PD0008

ModEq(m,a,b)

Balanced-natural congruence modulo m.

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

∃ u. ∃ v. a + m · u = b + m · v

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

Hygienic expanded first-order definition 
exists u v. a + m * u = b + m * v

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

Unit(a,m)CanonicalModularResidue(m,a,r)UnitScaledPrefix(a,m,b,c,d,e,l)

Checked theorems using this definition

EU0001 · euler_coprime_mod_transportEU0002 · euler_multiplier_coprime_iffEU0008 · euler_multiplier_prefix_extendEU0018 · euler_unit_factor_scaled_congruenceEU0019 · euler_nonunit_factor_unchanged_congruenceEU001D · euler_coprime_weighted_product_cancelEU001E · euler_unit_count_product_balanceEU001F · euler_coprime_totient_power_valueEU0020 · euler_coprime_totient_powerEU0021 · euler_modular_unit_totient_powerEU0022 · euler_theorem_for_units