PA00AK

bounded_mod_inverse_unique

Stable checked-use theorem · independently closed

Two bounded inverses of the same residue are equal.

Exact expanded PA statement

forall p x y z. (exists wip_strict_gap_unique_y_bound. wip_strict_gap_unique_y_bound + S y = p) -> (exists wip_strict_gap_unique_z_bound. wip_strict_gap_unique_z_bound + S z = p) -> (exists wip_mod_left_unique_xy wip_mod_right_unique_xy. x * y + p * wip_mod_left_unique_xy = 1 + p * wip_mod_right_unique_xy) -> (exists wip_mod_left_unique_xz wip_mod_right_unique_xz. x * z + p * wip_mod_left_unique_xz = 1 + p * wip_mod_right_unique_xz) -> y = z

Structural proof guide

Generated structural guide

Two bounded inverses of the same residue are equal.

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

The proof proceeds by intermediate claims (7), equality transport (3).

Referenced ingredients

PA003L mod_eq_symm PA0020 mod_eq_mul_left PA001Y mod_eq_mul_right PA000B mul_assoc PA000H mul_comm PA0002 mul_one PA000M one_mul PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA003L mod_eq_symm PA0020 mod_eq_mul_left PA001Y mod_eq_mul_right PA000B mul_assoc PA000H mul_comm PA0002 mul_one PA000M one_mul PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct dependents

PA00AL bounded_inverse_index_unique

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 p
  2. 0002intro x
  3. 0003intro y
  4. 0004intro z
  5. 0005intro hy
  6. 0006intro hz
  7. 0007intro hxy
  8. 0008intro hxz
  9. 0009have hreverse : exists wip_mod_left_unique_reverse_xz wip_mod_right_unique_reverse_xz. 1 + p * wip_mod_left_unique_reverse_xz = x * z + p * wip_mod_right_unique_reverse_xz
  10. 0010specialize mod_eq_symm p
  11. 0011specialize mod_eq_symm (x * z)
  12. 0012specialize mod_eq_symm 1
  13. 0013apply mod_eq_symm
  14. 0014exact hxz
  15. 0015have hleftscaled : exists wip_mod_left_unique_left_scaled wip_mod_right_unique_left_scaled. y * 1 + p * wip_mod_left_unique_left_scaled = y * (x * z) + p * wip_mod_right_unique_left_scaled
  16. 0016specialize mod_eq_mul_left p
  17. 0017specialize mod_eq_mul_left 1
  18. 0018specialize mod_eq_mul_left (x * z)
  19. 0019specialize mod_eq_mul_left y
  20. 0020apply mod_eq_mul_left
  21. 0021exact hreverse
  22. 0022have hrightscaled : exists wip_mod_left_unique_right_scaled wip_mod_right_unique_right_scaled. (x * y) * z + p * wip_mod_left_unique_right_scaled = 1 * z + p * wip_mod_right_unique_right_scaled
  23. 0023specialize mod_eq_mul_right p
  24. 0024specialize mod_eq_mul_right (x * y)
  25. 0025specialize mod_eq_mul_right 1
  26. 0026specialize mod_eq_mul_right z
  27. 0027apply mod_eq_mul_right
  28. 0028exact hxy
  29. 0029have hleft : y * 1 = y
  30. 0030specialize mul_one y
  31. 0031exact mul_one
  32. 0032have hmiddle : y * (x * z) = (x * y) * z
  33. 0033trans (y * x) * z
  34. 0034symm
  35. 0035specialize mul_assoc y
  36. 0036specialize mul_assoc x
  37. 0037specialize mul_assoc z
  38. 0038apply mul_assoc
  39. 0039congr
  40. 0040apply mul_comm
  41. 0041refl
  42. 0042have hright : 1 * z = z
  43. 0043specialize one_mul z
  44. 0044exact one_mul
  45. 0045rewrite hleft at hleftscaled
  46. 0046rewrite hmiddle at hleftscaled
  47. 0047rewrite hright at hrightscaled
  48. 0048have hyz : exists wip_mod_left_unique_result wip_mod_right_unique_result. y + p * wip_mod_left_unique_result = z + p * wip_mod_right_unique_result
  49. 0049specialize mod_eq_trans p
  50. 0050specialize mod_eq_trans y
  51. 0051specialize mod_eq_trans ((x * y) * z)
  52. 0052specialize mod_eq_trans z
  53. 0053apply mod_eq_trans
  54. 0054exact hleftscaled
  55. 0055exact hrightscaled
  56. 0056specialize mod_eq_bounded_unique p
  57. 0057specialize mod_eq_bounded_unique y
  58. 0058specialize mod_eq_bounded_unique z
  59. 0059apply mod_eq_bounded_unique
  60. 0060exact hy
  61. 0061exact hz
  62. 0062exact hyz