PA003P

coprime_balanced_mod_inverse

Stable checked-use theorem · independently closed

Balanced Bezout coefficients give a subtraction-free modular inverse.

Exact expanded PA statement

forall a m. (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v

Structural proof guide

Generated structural guide

Balanced Bezout coefficients give a subtraction-free modular inverse.

Use the direct prerequisites coprime_balanced_bezout, add_assoc as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (1).

Referenced ingredients

PA001M coprime_balanced_bezout PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA001M coprime_balanced_bezout PA0009 add_assoc

Direct dependents

PA003Q coprime_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 hcop
  4. 0004have hbez : exists xp yp xn yn. a * xp + m * yp = 1 + (a * xn + m * yn)
  5. 0005specialize coprime_balanced_bezout a
  6. 0006specialize coprime_balanced_bezout m
  7. 0007apply coprime_balanced_bezout
  8. 0008exact hcop
  9. 0009cases hbez
  10. 0010cases hbez_witness
  11. 0011cases hbez_witness_witness
  12. 0012cases hbez_witness_witness_witness
  13. 0013exists x
  14. 0014exists x2
  15. 0015exists x1
  16. 0016exists x3
  17. 0017trans 1 + (a * x2 + m * x3)
  18. 0018exact hbez_witness_witness_witness_witness
  19. 0019symm
  20. 0020apply add_assoc