PA003R

mod_eq_cancel_coprime

Stable checked-use theorem · independently closed

A coprime factor cancels from balanced congruence at nonzero modulus.

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.

  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