BT0038

coprime_balanced_bezout

Stable · empty-context checked

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

Coprime inputs admit balanced natural Bezout coefficients with result one.

Direct prerequisites: gcd_balanced_bezout_exists. The authored body proceeds by case analysis (8), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0035 gcd_balanced_bezout_exists

Direct dependents

BT0039 gauss_coprime_cancel BT004F binary_crt

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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