PA003Q

coprime_mod_inverse

Stable checked-use theorem · independently closed

A nonzero modulus turns balanced Bezout data into a natural modular inverse.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A nonzero modulus turns balanced Bezout data into a natural modular inverse.

Use the direct prerequisites nonzero_is_succ, coprime_balanced_mod_inverse, mod_eq_refl, mod_eq_add, mod_eq_predecessor_cancel, mod_eq_trans, mul_add, mul_assoc, mul_comm as previously established PA formulas.

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

Referenced ingredients

PA001V nonzero_is_succ PA003P coprime_balanced_mod_inverse PA0023 mod_eq_refl PA0022 mod_eq_add PA0025 mod_eq_predecessor_cancel PA0024 mod_eq_trans PA000A mul_add PA000B mul_assoc PA000H mul_comm

Proof neighborhood

Direct dependencies

PA001V nonzero_is_succ PA003P coprime_balanced_mod_inverse PA0023 mod_eq_refl PA0022 mod_eq_add PA0025 mod_eq_predecessor_cancel PA0024 mod_eq_trans PA000A mul_add PA000B mul_assoc PA000H mul_comm

Direct dependents

PA003R mod_eq_cancel_coprime PA0062 prime_mod_inverse

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 a
  2. 0002intro m
  3. 0003intro hm
  4. 0004intro hcop
  5. 0005have hms : exists k. m = S k
  6. 0006specialize nonzero_is_succ m
  7. 0007apply nonzero_is_succ
  8. 0008exact hm
  9. 0009have hbal : exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v
  10. 0010specialize coprime_balanced_mod_inverse a
  11. 0011specialize coprime_balanced_mod_inverse m
  12. 0012apply coprime_balanced_mod_inverse
  13. 0013exact hcop
  14. 0014cases hms
  15. 0015cases hbal
  16. 0016cases hbal_witness
  17. 0017cases hbal_witness_witness
  18. 0018cases hbal_witness_witness_witness
  19. 0019have hself : exists u v. (x * (a * x2)) + m * u = (x * (a * x2)) + m * v
  20. 0020specialize mod_eq_refl m
  21. 0021specialize mod_eq_refl (x * (a * x2))
  22. 0022apply mod_eq_refl
  23. 0023have hadd : exists u v. ((a * x1) + x * (a * x2)) + m * u = ((1 + a * x2) + x * (a * x2)) + m * v
  24. 0024specialize mod_eq_add m
  25. 0025specialize mod_eq_add (a * x1)
  26. 0026specialize mod_eq_add (1 + a * x2)
  27. 0027specialize mod_eq_add (x * (a * x2))
  28. 0028specialize mod_eq_add (x * (a * x2))
  29. 0029apply mod_eq_add
  30. 0030exists x3
  31. 0031exists x4
  32. 0032exact hbal_witness_witness_witness_witness
  33. 0033exact hself
  34. 0034have hcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + m * u = 1 + m * v
  35. 0035specialize mod_eq_predecessor_cancel x
  36. 0036specialize mod_eq_predecessor_cancel 1
  37. 0037specialize mod_eq_predecessor_cancel (a * x2)
  38. 0038have hkcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + S x * u = 1 + S x * v
  39. 0039apply mod_eq_predecessor_cancel
  40. 0040rewrite <- hms_witness at hkcancel
  41. 0041rewrite <- hms_witness at hkcancel
  42. 0042exact hkcancel
  43. 0043have hfinal : exists u v. ((a * x1) + x * (a * x2)) + m * u = 1 + m * v
  44. 0044specialize mod_eq_trans m
  45. 0045specialize mod_eq_trans ((a * x1) + x * (a * x2))
  46. 0046specialize mod_eq_trans ((1 + a * x2) + x * (a * x2))
  47. 0047specialize mod_eq_trans 1
  48. 0048apply mod_eq_trans
  49. 0049exact hadd
  50. 0050exact hcancel
  51. 0051have hnorm : a * (x1 + x * x2) = (a * x1) + x * (a * x2)
  52. 0052trans a * x1 + a * (x * x2)
  53. 0053apply mul_add
  54. 0054congr
  55. 0055refl
  56. 0056trans (a * x) * x2
  57. 0057symm
  58. 0058apply mul_assoc
  59. 0059trans (x * a) * x2
  60. 0060congr
  61. 0061apply mul_comm
  62. 0062refl
  63. 0063apply mul_assoc
  64. 0064exists x1 + x * x2
  65. 0065rewrite hnorm
  66. 0066exact hfinal