CG0001

mod_eq_cancel_gcd_cofactor

The actual quotient modulus m/g exactly classifies cancellation of a common coefficient at nonzero m.

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. ∀ m. ∀ g. ∀ A. ∀ M. ∀ x. ∀ y. ¬m = 0 → IsGCD(g,a,m) → a = g · A → m = g · M → (ModEq(m,a · x,a · y) → ModEq(M,x,y)) ∧ (ModEq(M,x,y) → ModEq(m,a · x,a · y))

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

Definition DAG

Coprime(a,b) · 1IsGCD(g,a,b) · 1ModEq(m,a,b) · 4

Actual proof prerequisites

mul_zero_left · checked external prerequisiteis_gcd_quotients_coprime_nonzero · checked external prerequisitemul_assoc · checked external prerequisitemod_eq_cancel_coprime · checked external prerequisitemod_eq_unscale_nonzero · checked external prerequisitemod_eq_scale · checked external prerequisitemod_eq_mul_left · checked external prerequisite
Original expanded first-order statement 
forall a m g A M x y. (~(m=0)) -> ((((exists hag_left_factor_lcc_cancel. a = g * hag_left_factor_lcc_cancel) /\ (exists hag_right_factor_lcc_cancel. m = g * hag_right_factor_lcc_cancel)) /\ forall hag_divisor_lcc_cancel. (exists hag_common_left_lcc_cancel. a = hag_divisor_lcc_cancel * hag_common_left_lcc_cancel) -> (exists hag_common_right_lcc_cancel. m = hag_divisor_lcc_cancel * hag_common_right_lcc_cancel) -> exists hag_greatest_factor_lcc_cancel. g = hag_divisor_lcc_cancel * hag_greatest_factor_lcc_cancel)) -> (a=g*A) -> (m=g*M) -> ((((exists hgcrt_mod_left_lcc_cancel_left hgcrt_mod_right_lcc_cancel_left. (a * x) + m * hgcrt_mod_left_lcc_cancel_left = (a * y) + m * hgcrt_mod_right_lcc_cancel_left) -> (exists hgcrt_mod_left_lcc_cancel_right hgcrt_mod_right_lcc_cancel_right. x + M * hgcrt_mod_left_lcc_cancel_right = y + M * hgcrt_mod_right_lcc_cancel_right)) /\ (((exists hgcrt_mod_left_lcc_cancel_right hgcrt_mod_right_lcc_cancel_right. x + M * hgcrt_mod_left_lcc_cancel_right = y + M * hgcrt_mod_right_lcc_cancel_right) -> (exists hgcrt_mod_left_lcc_cancel_left hgcrt_mod_right_lcc_cancel_left. (a * x) + m * hgcrt_mod_left_lcc_cancel_left = (a * y) + m * hgcrt_mod_right_lcc_cancel_left)))))

Complete tactic proof in conservative notation

All 78 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

78 script commands · 18 reading checkpoints · 5 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–10

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro g
  4. L4
    intro A
  5. L5
    intro M
  6. L6
    intro x
  7. L7
    intro y
  8. L8
    intro hm0
  9. L9
    intro hg
  10. L10
    intro ha
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hm
03Establish hg0L12–18

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

  1. L12
    have hg0 : ~(g=0)
  2. L13
    intro hz
  3. L14
    apply hm0
  4. L15
    trans g*M
  5. L16
    exact hm
  6. L17
    rewrite hz
  7. L18
    apply mul_zero_left
04Establish hM0L19–25

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

  1. L19
    have hM0 : ~(M=0)
  2. L20
    intro hz
  3. L21
    apply hm0
  4. L22
    trans g*M
  5. L23
    exact hm
  6. L24
    rewrite hz
  7. L25
    simp
05Establish hcL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd quotients coprime nonzero.

  1. L26
  2. L27
    specialize is_gcd_quotients_coprime_nonzero (g)
  3. L28
    specialize is_gcd_quotients_coprime_nonzero (a)
  4. L29
    specialize is_gcd_quotients_coprime_nonzero (m)
  5. L30
    specialize is_gcd_quotients_coprime_nonzero (A)
  6. L31
    specialize is_gcd_quotients_coprime_nonzero (M)
  7. L32
    apply is_gcd_quotients_coprime_nonzero
  8. L33
    exact hg
  9. L34
    exact hg0
  10. L35
    exact ha
06Use earlier factsL36–36

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

  1. L36
    exact hm
07Establish hxL37–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L37
    have hx : a*x=g*(A*x)
  2. L38
    rewrite ha
  3. L39
    apply mul_assoc
08Establish hyL40–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L40
    have hy : a*y=g*(A*y)
  2. L41
    rewrite ha
  3. L42
    apply mul_assoc
09Separate the logical casesL43–43

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

  1. L43
    split
10Fix variables and assumptionsL44–44

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

  1. L44
    intro h
11Use earlier factsL45–54

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

  1. L45
    specialize mod_eq_cancel_coprime (M)
  2. L46
    specialize mod_eq_cancel_coprime (A)
  3. L47
    specialize mod_eq_cancel_coprime (x)
  4. L48
    specialize mod_eq_cancel_coprime (y)
  5. L49
    apply mod_eq_cancel_coprime
  6. L50
    exact hM0
  7. L51
    exact hc
  8. L52
    specialize mod_eq_unscale_nonzero (g)
  9. L53
    specialize mod_eq_unscale_nonzero (M)
  10. L54
    specialize mod_eq_unscale_nonzero (A*x)
12Use earlier factsL55–57

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

  1. L55
    specialize mod_eq_unscale_nonzero (A*y)
  2. L56
    apply mod_eq_unscale_nonzero
  3. L57
    exact hg0
13Calculate and transport equalitiesL58–61

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

  1. L58
    rewrite <- hm
  2. L59
    rewrite <- hm
  3. L60
    rewrite <- hx
  4. L61
    rewrite <- hy
14Use earlier factsL62–62

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

  1. L62
    exact h
15Fix variables and assumptionsL63–63

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

  1. L63
    intro h
16Calculate and transport equalitiesL64–67

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

  1. L64
    rewrite hm
  2. L65
    rewrite hm
  3. L66
    rewrite hx
  4. L67
    rewrite hy
17Use earlier factsL68–77

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

  1. L68
    specialize mod_eq_scale (g)
  2. L69
    specialize mod_eq_scale (M)
  3. L70
    specialize mod_eq_scale (A*x)
  4. L71
    specialize mod_eq_scale (A*y)
  5. L72
    apply mod_eq_scale
  6. L73
    specialize mod_eq_mul_left (M)
  7. L74
    specialize mod_eq_mul_left (x)
  8. L75
    specialize mod_eq_mul_left (y)
  9. L76
    specialize mod_eq_mul_left (A)
  10. L77
    apply mod_eq_mul_left
18Use earlier factsL78–78

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

  1. L78
    exact h

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro g
  4. 0004intro A
  5. 0005intro M
  6. 0006intro x
  7. 0007intro y
  8. 0008intro hm0
  9. 0009intro hg
  10. 0010intro ha
  11. 0011intro hm
  12. 0012have hg0 : ~(g=0)
  13. 0013intro hz
  14. 0014apply hm0
  15. 0015trans g*M
  16. 0016exact hm
  17. 0017rewrite hz
  18. 0018apply mul_zero_left
  19. 0019have hM0 : ~(M=0)
  20. 0020intro hz
  21. 0021apply hm0
  22. 0022trans g*M
  23. 0023exact hm
  24. 0024rewrite hz
  25. 0025simp
  26. 0026have hc : Coprime(A,M)
  27. 0027specialize is_gcd_quotients_coprime_nonzero (g)
  28. 0028specialize is_gcd_quotients_coprime_nonzero (a)
  29. 0029specialize is_gcd_quotients_coprime_nonzero (m)
  30. 0030specialize is_gcd_quotients_coprime_nonzero (A)
  31. 0031specialize is_gcd_quotients_coprime_nonzero (M)
  32. 0032apply is_gcd_quotients_coprime_nonzero
  33. 0033exact hg
  34. 0034exact hg0
  35. 0035exact ha
  36. 0036exact hm
  37. 0037have hx : a*x=g*(A*x)
  38. 0038rewrite ha
  39. 0039apply mul_assoc
  40. 0040have hy : a*y=g*(A*y)
  41. 0041rewrite ha
  42. 0042apply mul_assoc
  43. 0043split
  44. 0044intro h
  45. 0045specialize mod_eq_cancel_coprime (M)
  46. 0046specialize mod_eq_cancel_coprime (A)
  47. 0047specialize mod_eq_cancel_coprime (x)
  48. 0048specialize mod_eq_cancel_coprime (y)
  49. 0049apply mod_eq_cancel_coprime
  50. 0050exact hM0
  51. 0051exact hc
  52. 0052specialize mod_eq_unscale_nonzero (g)
  53. 0053specialize mod_eq_unscale_nonzero (M)
  54. 0054specialize mod_eq_unscale_nonzero (A*x)
  55. 0055specialize mod_eq_unscale_nonzero (A*y)
  56. 0056apply mod_eq_unscale_nonzero
  57. 0057exact hg0
  58. 0058rewrite <- hm
  59. 0059rewrite <- hm
  60. 0060rewrite <- hx
  61. 0061rewrite <- hy
  62. 0062exact h
  63. 0063intro h
  64. 0064rewrite hm
  65. 0065rewrite hm
  66. 0066rewrite hx
  67. 0067rewrite hy
  68. 0068specialize mod_eq_scale (g)
  69. 0069specialize mod_eq_scale (M)
  70. 0070specialize mod_eq_scale (A*x)
  71. 0071specialize mod_eq_scale (A*y)
  72. 0072apply mod_eq_scale
  73. 0073specialize mod_eq_mul_left (M)
  74. 0074specialize mod_eq_mul_left (x)
  75. 0075specialize mod_eq_mul_left (y)
  76. 0076specialize mod_eq_mul_left (A)
  77. 0077apply mod_eq_mul_left
  78. 0078exact h