PA009C

prime_scaled_inverse_unique

Alpha v16 checked-use theorem · independently closed; not Stable

The bounded scaled inverse of a prime unit is unique.

Exact expanded PA statement

forall p a x y z. ((~(p = 1) /\ forall esi_prime_left_unique_prime esi_prime_right_unique_prime. p = esi_prime_left_unique_prime * esi_prime_right_unique_prime -> esi_prime_left_unique_prime = 1 \/ esi_prime_right_unique_prime = 1)) -> ((((~(x = 0) /\ (exists esi_strict_gap_unique_left_left_bound. esi_strict_gap_unique_left_left_bound + S x = p))) /\ (((~(y = 0) /\ (exists esi_strict_gap_unique_left_right_bound. esi_strict_gap_unique_left_right_bound + S y = p))) /\ (exists esi_mod_left_unique_left_mod esi_mod_right_unique_left_mod. (x * y) + p * esi_mod_left_unique_left_mod = (a) + p * esi_mod_right_unique_left_mod)))) -> ((((~(x = 0) /\ (exists esi_strict_gap_unique_right_left_bound. esi_strict_gap_unique_right_left_bound + S x = p))) /\ (((~(z = 0) /\ (exists esi_strict_gap_unique_right_right_bound. esi_strict_gap_unique_right_right_bound + S z = p))) /\ (exists esi_mod_left_unique_right_mod esi_mod_right_unique_right_mod. (x * z) + p * esi_mod_left_unique_right_mod = (a) + p * esi_mod_right_unique_right_mod)))) -> y = z

Structural proof guide

Generated structural guide

The bounded scaled inverse of a prime unit is unique.

Use the direct prerequisites divisor_le_nonzero, lt_not_le, mod_eq_symm, mod_eq_trans, prime_mod_cancel, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (5).

Referenced ingredients

PA0039 divisor_le_nonzero PA003A lt_not_le PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA0039 divisor_le_nonzero PA003A lt_not_le PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Direct dependents

PA009D scaled_inverse_prefix_extensional

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hp
  7. 0007intro hxy
  8. 0008intro hxz
  9. 0009cases hxy
  10. 0010cases hxy_left
  11. 0011cases hxy_right
  12. 0012cases hxy_right_left
  13. 0013cases hxz
  14. 0014cases hxz_left
  15. 0015cases hxz_right
  16. 0016cases hxz_right_left
  17. 0017have hnotdiv : ~(exists k. x = p * k)
  18. 0018intro hdiv
  19. 0019have hpx : exists t. t + p = x
  20. 0020specialize divisor_le_nonzero p
  21. 0021specialize divisor_le_nonzero x
  22. 0022apply divisor_le_nonzero
  23. 0023exact hxy_left_left
  24. 0024exact hdiv
  25. 0025specialize lt_not_le x
  26. 0026specialize lt_not_le p
  27. 0027apply lt_not_le
  28. 0028exact hxy_left_right
  29. 0029exact hpx
  30. 0030have hreverse : exists esi_mod_left_unique_reverse esi_mod_right_unique_reverse. (a) + p * esi_mod_left_unique_reverse = (x * z) + p * esi_mod_right_unique_reverse
  31. 0031specialize mod_eq_symm p
  32. 0032specialize mod_eq_symm (x * z)
  33. 0033specialize mod_eq_symm a
  34. 0034apply mod_eq_symm
  35. 0035exact hxz_right_right
  36. 0036have hproducts : exists esi_mod_left_unique_products esi_mod_right_unique_products. (x * y) + p * esi_mod_left_unique_products = (x * z) + p * esi_mod_right_unique_products
  37. 0037specialize mod_eq_trans p
  38. 0038specialize mod_eq_trans (x * y)
  39. 0039specialize mod_eq_trans a
  40. 0040specialize mod_eq_trans (x * z)
  41. 0041apply mod_eq_trans
  42. 0042exact hxy_right_right
  43. 0043exact hreverse
  44. 0044have hyz : exists esi_mod_left_unique_residues esi_mod_right_unique_residues. (y) + p * esi_mod_left_unique_residues = (z) + p * esi_mod_right_unique_residues
  45. 0045specialize prime_mod_cancel p
  46. 0046specialize prime_mod_cancel x
  47. 0047specialize prime_mod_cancel y
  48. 0048specialize prime_mod_cancel z
  49. 0049apply prime_mod_cancel
  50. 0050exact hp
  51. 0051exact hnotdiv
  52. 0052exact hproducts
  53. 0053specialize mod_eq_bounded_unique p
  54. 0054specialize mod_eq_bounded_unique y
  55. 0055specialize mod_eq_bounded_unique z
  56. 0056apply mod_eq_bounded_unique
  57. 0057exact hxy_right_left_right
  58. 0058exact hxz_right_left_right
  59. 0059exact hyz