PA003R · theorem

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.

Statement with defined notation

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

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0005 Coprime PD0008 ModEq

3 occurrences

In local proof propositions

PD0008 ModEq PD0031 BalancedInverse

8 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

PA003S prime_mod_cancel PA0084 gauss_signed_products_cancel_mod PA008L fermat_predecessor_exponent_mod_one

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

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

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 : ∃ z. BalancedInverse(m,a,z)Definitions: BalancedInverse(m,a,z)Original native command in the exact edition
  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 : ModEq(m,x · (a · x1),x · 1)Definitions: ModEq(m,x · (a · x1),x · 1)Original native command in the exact edition
  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 : ModEq(m,a · x · x1,x)Definitions: ModEq(m,a · x · x1,x)Original native command in the exact edition
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 : ModEq(m,x,a · x · x1)Definitions: ModEq(m,x,a · x · x1)Original native command in the exact edition
  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 : ModEq(m,a · x · x1,a · y · x1)Definitions: ModEq(m,a · x · x1,a · y · x1)Original native command in the exact edition
  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 : ModEq(m,y · (a · x1),y · 1)Definitions: ModEq(m,y · (a · x1),y · 1)Original native command in the exact edition
  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 : ModEq(m,a · y · x1,y)Definitions: ModEq(m,a · y · x1,y)Original native command in the exact edition
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 : ModEq(m,x,a · y · x1)Definitions: ModEq(m,x,a · y · x1)Original native command in the exact edition
  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 defined 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 : ∃ z. BalancedInverse(m,a,z)
    Exact native replay linehave 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 : ModEq(m,x · (a · x1),x · 1)
    Exact native replay linehave 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 : ModEq(m,a · x · x1,x)
    Exact native replay linehave 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 : ModEq(m,x,a · x · x1)
    Exact native replay linehave 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 : ModEq(m,a · x · x1,a · y · x1)
    Exact native replay linehave 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 : ModEq(m,y · (a · x1),y · 1)
    Exact native replay linehave 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 : ModEq(m,a · y · x1,y)
    Exact native replay linehave 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 : ModEq(m,x,a · y · x1)
    Exact native replay linehave 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