PA001M

coprime_balanced_bezout

Stable checked-use theorem · independently closed

Coprime inputs admit balanced natural Bezout coefficients with result one.

Exact expanded PA statement

forall a b. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)

Structural proof guide

Generated structural guide

Coprime inputs admit balanced natural Bezout coefficients with result one.

Use the direct prerequisites gcd_balanced_bezout_exists as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (2), equality transport (1).

Referenced ingredients

PA001L gcd_balanced_bezout_exists

Proof neighborhood

Direct dependencies

PA001L gcd_balanced_bezout_exists

Direct dependents

PA001P gauss_coprime_cancel PA0026 binary_crt PA003P coprime_balanced_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 b
  3. 0003intro hcop
  4. 0004have hgb : exists d. ((((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))
  5. 0005apply gcd_balanced_bezout_exists
  6. 0006cases hgb
  7. 0007cases hgb_witness
  8. 0008cases hgb_witness_left
  9. 0009cases hgb_witness_left_left
  10. 0010have hd : x = 1
  11. 0011specialize hcop x
  12. 0012apply hcop
  13. 0013exact hgb_witness_left_left_left
  14. 0014exact hgb_witness_left_left_right
  15. 0015cases hgb_witness_right
  16. 0016cases hgb_witness_right_witness
  17. 0017cases hgb_witness_right_witness_witness
  18. 0018cases hgb_witness_right_witness_witness_witness
  19. 0019exists x1
  20. 0020exists x2
  21. 0021exists x3
  22. 0022exists x4
  23. 0023rewrite hd at hgb_witness_right_witness_witness_witness_witness
  24. 0024exact hgb_witness_right_witness_witness_witness_witness