PA003R

mod_eq_cancel_coprime

Stable checked-use theorem · independently closed

A coprime factor cancels from balanced congruence at nonzero modulus.

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

Exact expanded PA statement

forall m a x y. ~(m = 0) -> (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> (exists u v. (a * x) + m * u = (a * y) + m * v) -> exists r s. x + m * r = y + m * s

Structural proof guide

Generated structural guide

A coprime factor cancels from balanced congruence at nonzero modulus.

Use the direct prerequisites coprime_mod_inverse, mod_eq_mul_right, mod_eq_mul_left, mod_eq_symm, mod_eq_trans, mul_assoc, mul_comm, mul_one as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (12).

Referenced ingredients

PA003Q coprime_mod_inverse PA001Y mod_eq_mul_right PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans PA000B mul_assoc PA000H mul_comm PA0002 mul_one

Proof neighborhood

Direct dependencies

PA003Q coprime_mod_inverse PA001Y mod_eq_mul_right PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans PA000B mul_assoc PA000H mul_comm PA0002 mul_one

Direct dependents

PA003S prime_mod_cancel PA0084 gauss_signed_products_cancel_mod PA008L fermat_predecessor_exponent_mod_one

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

114 script commands · 37 reading checkpoints · 12 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.

Named ingredients (8)
coprime mod inversemod eq mul rightmod eq mul leftmod eq symmmod eq transmul assocmul commmul one
01Fix variables and assumptionsL1–7

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hm
  6. L6
    intro hcop
  7. L7
    intro hxy
02Establish hinvL8–13

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

  1. L8
    have hinv : exists z u v. a * z + m * u = 1 + m * v
  2. L9
    specialize coprime_mod_inverse a
  3. L10
    specialize coprime_mod_inverse m
  4. L11
    apply coprime_mod_inverse
  5. L12
    exact hm
  6. L13
    exact hcop
03Separate the logical casesL14–16

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

  1. L14
    cases hinv
  2. L15
    cases hinv_witness
  3. L16
    cases hinv_witness_witness
04Establish hzxL17–22

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

  1. L17
    have hzx : exists u v. (x * (a * x1)) + m * u = (x * 1) + m * v
  2. L18
    specialize mod_eq_mul_left m
  3. L19
    specialize mod_eq_mul_left (a * x1)
  4. L20
    specialize mod_eq_mul_left 1
  5. L21
    specialize mod_eq_mul_left x
  6. L22
    apply mod_eq_mul_left
05Construct an explicit witnessL23–24

Supply the displayed value, then prove that it has the required property.

  1. L23
    exists x2
  2. L24
    exists x3
06Use earlier factsL25–25

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

  1. L25
    exact hinv_witness_witness_witness
07Establish hnormxL26–34

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

  1. L26
    have hnormx : x * (a * x1) = (a * x) * x1
  2. L27
    trans (x * a) * x1
  3. L28
    symm
  4. L29
    apply mul_assoc
  5. L30
    trans (a * x) * x1
  6. L31
    congr
  7. L32
    apply mul_comm
  8. L33
    refl
  9. L34
    refl
08Establish honexL35–36

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

  1. L35
    have honex : x * 1 = x
  2. L36
    apply mul_one
09Establish hxprodL37–37

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hxprod : exists u v. ((a * x) * x1) + m * u = x + m * v
10Separate the logical casesL38–39

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

  1. L38
    cases hzx
  2. L39
    cases hzx_witness
11Construct an explicit witnessL40–41

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists x4
  2. L41
    exists x5
12Calculate and transport equalitiesL42–44

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

  1. L42
    trans (x * (a * x1)) + m * x4
  2. L43
    congr
  3. L44
    symm
13Use earlier factsL45–45

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

  1. L45
    exact hnormx
14Calculate and transport equalitiesL46–47

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

  1. L46
    refl
  2. L47
    trans (x * 1) + m * x5
15Use earlier factsL48–48

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

  1. L48
    exact hzx_witness_witness
16Calculate and transport equalitiesL49–49

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

  1. L49
    congr
17Use earlier factsL50–50

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

  1. L50
    exact honex
18Calculate and transport equalitiesL51–51

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

  1. L51
    refl
19Establish hxhprodL52–57

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

  1. L52
    have hxhprod : exists u v. x + m * u = ((a * x) * x1) + m * v
  2. L53
    specialize mod_eq_symm m
  3. L54
    specialize mod_eq_symm ((a * x) * x1)
  4. L55
    specialize mod_eq_symm x
  5. L56
    apply mod_eq_symm
  6. L57
    exact hxprod
20Establish hscaledL58–64

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

  1. L58
    have hscaled : exists u v. ((a * x) * x1) + m * u = ((a * y) * x1) + m * v
  2. L59
    specialize mod_eq_mul_right m
  3. L60
    specialize mod_eq_mul_right (a * x)
  4. L61
    specialize mod_eq_mul_right (a * y)
  5. L62
    specialize mod_eq_mul_right x1
  6. L63
    apply mod_eq_mul_right
  7. L64
    exact hxy
21Establish hzyL65–70

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

  1. L65
    have hzy : exists u v. (y * (a * x1)) + m * u = (y * 1) + m * v
  2. L66
    specialize mod_eq_mul_left m
  3. L67
    specialize mod_eq_mul_left (a * x1)
  4. L68
    specialize mod_eq_mul_left 1
  5. L69
    specialize mod_eq_mul_left y
  6. L70
    apply mod_eq_mul_left
22Construct an explicit witnessL71–72

Supply the displayed value, then prove that it has the required property.

  1. L71
    exists x2
  2. L72
    exists x3
23Use earlier factsL73–73

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

  1. L73
    exact hinv_witness_witness_witness
24Establish hnormyL74–82

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

  1. L74
    have hnormy : y * (a * x1) = (a * y) * x1
  2. L75
    trans (y * a) * x1
  3. L76
    symm
  4. L77
    apply mul_assoc
  5. L78
    trans (a * y) * x1
  6. L79
    congr
  7. L80
    apply mul_comm
  8. L81
    refl
  9. L82
    refl
25Establish honeyL83–84

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

  1. L83
    have honey : y * 1 = y
  2. L84
    apply mul_one
26Establish hyprodL85–85

Establish this local claim before using it. It is not an additional assumption.

  1. L85
    have hyprod : exists u v. ((a * y) * x1) + m * u = y + m * v
27Separate the logical casesL86–87

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

  1. L86
    cases hzy
  2. L87
    cases hzy_witness
28Construct an explicit witnessL88–89

Supply the displayed value, then prove that it has the required property.

  1. L88
    exists x4
  2. L89
    exists x5
29Calculate and transport equalitiesL90–92

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

  1. L90
    trans (y * (a * x1)) + m * x4
  2. L91
    congr
  3. L92
    symm
30Use earlier factsL93–93

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

  1. L93
    exact hnormy
31Calculate and transport equalitiesL94–95

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

  1. L94
    refl
  2. L95
    trans (y * 1) + m * x5
32Use earlier factsL96–96

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

  1. L96
    exact hzy_witness_witness
33Calculate and transport equalitiesL97–97

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

  1. L97
    congr
34Use earlier factsL98–98

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

  1. L98
    exact honey
35Calculate and transport equalitiesL99–99

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

  1. L99
    refl
36Establish hmidL100–109

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

  1. L100
    have hmid : exists u v. x + m * u = ((a * y) * x1) + m * v
  2. L101
    specialize mod_eq_trans m
  3. L102
    specialize mod_eq_trans x
  4. L103
    specialize mod_eq_trans ((a * x) * x1)
  5. L104
    specialize mod_eq_trans ((a * y) * x1)
  6. L105
    apply mod_eq_trans
  7. L106
    exact hxhprod
  8. L107
    exact hscaled
  9. L108
    specialize mod_eq_trans m
  10. L109
    specialize mod_eq_trans x
37Use earlier factsL110–114

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

  1. L110
    specialize mod_eq_trans ((a * y) * x1)
  2. L111
    specialize mod_eq_trans y
  3. L112
    apply mod_eq_trans
  4. L113
    exact hmid
  5. L114
    exact hyprod

Library-wide reading audit

Original exact command ledger · 114 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hm
  6. 0006intro hcop
  7. 0007intro hxy
  8. 0008have hinv : exists z u v. a * z + m * u = 1 + m * v
  9. 0009specialize coprime_mod_inverse a
  10. 0010specialize coprime_mod_inverse m
  11. 0011apply coprime_mod_inverse
  12. 0012exact hm
  13. 0013exact hcop
  14. 0014cases hinv
  15. 0015cases hinv_witness
  16. 0016cases hinv_witness_witness
  17. 0017have hzx : exists u v. (x * (a * x1)) + m * u = (x * 1) + m * v
  18. 0018specialize mod_eq_mul_left m
  19. 0019specialize mod_eq_mul_left (a * x1)
  20. 0020specialize mod_eq_mul_left 1
  21. 0021specialize mod_eq_mul_left x
  22. 0022apply mod_eq_mul_left
  23. 0023exists x2
  24. 0024exists x3
  25. 0025exact hinv_witness_witness_witness
  26. 0026have hnormx : x * (a * x1) = (a * x) * x1
  27. 0027trans (x * a) * x1
  28. 0028symm
  29. 0029apply mul_assoc
  30. 0030trans (a * x) * x1
  31. 0031congr
  32. 0032apply mul_comm
  33. 0033refl
  34. 0034refl
  35. 0035have honex : x * 1 = x
  36. 0036apply mul_one
  37. 0037have hxprod : exists u v. ((a * x) * x1) + m * u = x + m * v
  38. 0038cases hzx
  39. 0039cases hzx_witness
  40. 0040exists x4
  41. 0041exists x5
  42. 0042trans (x * (a * x1)) + m * x4
  43. 0043congr
  44. 0044symm
  45. 0045exact hnormx
  46. 0046refl
  47. 0047trans (x * 1) + m * x5
  48. 0048exact hzx_witness_witness
  49. 0049congr
  50. 0050exact honex
  51. 0051refl
  52. 0052have hxhprod : exists u v. x + m * u = ((a * x) * x1) + m * v
  53. 0053specialize mod_eq_symm m
  54. 0054specialize mod_eq_symm ((a * x) * x1)
  55. 0055specialize mod_eq_symm x
  56. 0056apply mod_eq_symm
  57. 0057exact hxprod
  58. 0058have hscaled : exists u v. ((a * x) * x1) + m * u = ((a * y) * x1) + m * v
  59. 0059specialize mod_eq_mul_right m
  60. 0060specialize mod_eq_mul_right (a * x)
  61. 0061specialize mod_eq_mul_right (a * y)
  62. 0062specialize mod_eq_mul_right x1
  63. 0063apply mod_eq_mul_right
  64. 0064exact hxy
  65. 0065have hzy : exists u v. (y * (a * x1)) + m * u = (y * 1) + m * v
  66. 0066specialize mod_eq_mul_left m
  67. 0067specialize mod_eq_mul_left (a * x1)
  68. 0068specialize mod_eq_mul_left 1
  69. 0069specialize mod_eq_mul_left y
  70. 0070apply mod_eq_mul_left
  71. 0071exists x2
  72. 0072exists x3
  73. 0073exact hinv_witness_witness_witness
  74. 0074have hnormy : y * (a * x1) = (a * y) * x1
  75. 0075trans (y * a) * x1
  76. 0076symm
  77. 0077apply mul_assoc
  78. 0078trans (a * y) * x1
  79. 0079congr
  80. 0080apply mul_comm
  81. 0081refl
  82. 0082refl
  83. 0083have honey : y * 1 = y
  84. 0084apply mul_one
  85. 0085have hyprod : exists u v. ((a * y) * x1) + m * u = y + m * v
  86. 0086cases hzy
  87. 0087cases hzy_witness
  88. 0088exists x4
  89. 0089exists x5
  90. 0090trans (y * (a * x1)) + m * x4
  91. 0091congr
  92. 0092symm
  93. 0093exact hnormy
  94. 0094refl
  95. 0095trans (y * 1) + m * x5
  96. 0096exact hzy_witness_witness
  97. 0097congr
  98. 0098exact honey
  99. 0099refl
  100. 0100have hmid : exists u v. x + m * u = ((a * y) * x1) + m * v
  101. 0101specialize mod_eq_trans m
  102. 0102specialize mod_eq_trans x
  103. 0103specialize mod_eq_trans ((a * x) * x1)
  104. 0104specialize mod_eq_trans ((a * y) * x1)
  105. 0105apply mod_eq_trans
  106. 0106exact hxhprod
  107. 0107exact hscaled
  108. 0108specialize mod_eq_trans m
  109. 0109specialize mod_eq_trans x
  110. 0110specialize mod_eq_trans ((a * y) * x1)
  111. 0111specialize mod_eq_trans y
  112. 0112apply mod_eq_trans
  113. 0113exact hmid
  114. 0114exact hyprod