CG0009

linear_congruence_zero_modulus_nonzero_coefficient_unique

At modulus zero a nonzero coefficient has at most one natural solution; no bounded residue or finite-class formula is asserted.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Each statement retains its explicit modulus, coprimality and divisibility assumptions. These twelve arithmetic laws do not assert all order, primitive-root, Carmichael, exponential or simultaneous-polynomial congruence goals are finished.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ x. ∀ y. ¬a = 0 → ModEq(0,a · x,b) → ModEq(0,a · y,b) → x = y

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModEq(m,a,b) · 6

Actual proof prerequisites

mod_eq_zero_iff_eq · checked external prerequisitemul_left_cancel_nonzero · checked external prerequisite
Original expanded first-order statement 
forall a b x y. (~(a=0)) -> (exists hgcrt_mod_left_lcc_zero_unique_x hgcrt_mod_right_lcc_zero_unique_x. (a * x) + 0 * hgcrt_mod_left_lcc_zero_unique_x = b + 0 * hgcrt_mod_right_lcc_zero_unique_x) -> (exists hgcrt_mod_left_lcc_zero_unique_y hgcrt_mod_right_lcc_zero_unique_y. (a * y) + 0 * hgcrt_mod_left_lcc_zero_unique_y = b + 0 * hgcrt_mod_right_lcc_zero_unique_y) -> (x=y)

Complete tactic proof in conservative notation

All 32 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

32 script commands · 9 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro ha
  6. L6
    intro hx
  7. L7
    intro hy
02Establish he_xL8–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq zero iff eq.

  1. L8
    have he_x : (ModEq(0,a · x,b) → a · x = b) ∧ (a · x = b → ModEq(0,a · x,b))Definitions: ModEq(0,a · x,b)Original native command in the exact edition
  2. L9
    specialize mod_eq_zero_iff_eq (a*x)
  3. L10
    specialize mod_eq_zero_iff_eq (b)
  4. L11
    apply mod_eq_zero_iff_eq
03Separate the logical casesL12–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases he_x
04Establish hxeqL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply he x left.

  1. L13
    have hxeq : a*x=b
  2. L14
    apply he_x_left
  3. L15
    exact hx
05Establish he_yL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq zero iff eq.

  1. L16
    have he_y : (ModEq(0,a · y,b) → a · y = b) ∧ (a · y = b → ModEq(0,a · y,b))Definitions: ModEq(0,a · y,b)Original native command in the exact edition
  2. L17
    specialize mod_eq_zero_iff_eq (a*y)
  3. L18
    specialize mod_eq_zero_iff_eq (b)
  4. L19
    apply mod_eq_zero_iff_eq
06Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases he_y
07Establish hyeqL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply he y left.

  1. L21
    have hyeq : a*y=b
  2. L22
    apply he_y_left
  3. L23
    exact hy
  4. L24
    specialize mul_left_cancel_nonzero (a)
  5. L25
    specialize mul_left_cancel_nonzero (x)
  6. L26
    specialize mul_left_cancel_nonzero (y)
  7. L27
    apply mul_left_cancel_nonzero
  8. L28
    exact ha
  9. L29
    trans b
  10. L30
    exact hxeq
08Calculate and transport equalitiesL31–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    symm
09Use earlier factsL32–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    exact hyeq

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro x
  4. 0004intro y
  5. 0005intro ha
  6. 0006intro hx
  7. 0007intro hy
  8. 0008have he_x : (ModEq(0,a · x,b) → a · x = b) ∧ (a · x = b → ModEq(0,a · x,b))
  9. 0009specialize mod_eq_zero_iff_eq (a*x)
  10. 0010specialize mod_eq_zero_iff_eq (b)
  11. 0011apply mod_eq_zero_iff_eq
  12. 0012cases he_x
  13. 0013have hxeq : a*x=b
  14. 0014apply he_x_left
  15. 0015exact hx
  16. 0016have he_y : (ModEq(0,a · y,b) → a · y = b) ∧ (a · y = b → ModEq(0,a · y,b))
  17. 0017specialize mod_eq_zero_iff_eq (a*y)
  18. 0018specialize mod_eq_zero_iff_eq (b)
  19. 0019apply mod_eq_zero_iff_eq
  20. 0020cases he_y
  21. 0021have hyeq : a*y=b
  22. 0022apply he_y_left
  23. 0023exact hy
  24. 0024specialize mul_left_cancel_nonzero (a)
  25. 0025specialize mul_left_cancel_nonzero (x)
  26. 0026specialize mul_left_cancel_nonzero (y)
  27. 0027apply mul_left_cancel_nonzero
  28. 0028exact ha
  29. 0029trans b
  30. 0030exact hxeq
  31. 0031symm
  32. 0032exact hyeq