PA001L

gcd_balanced_bezout_exists

Stable checked-use theorem · independently closed

Every pair has a relational gcd together with balanced natural Bezout witnesses.

Exact expanded PA statement

forall a b. 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))

Structural proof guide

Generated structural guide

Every pair has a relational gcd together with balanced natural Bezout witnesses.

Use the direct prerequisites le_refl, gcd_balanced_bezout_exists_up_to as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA001A le_refl PA001K gcd_balanced_bezout_exists_up_to

Proof neighborhood

Direct dependencies

PA001A le_refl PA001K gcd_balanced_bezout_exists_up_to

Direct dependents

PA001M coprime_balanced_bezout

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. 0003specialize gcd_balanced_bezout_exists_up_to b
  4. 0004specialize gcd_balanced_bezout_exists_up_to b
  5. 0005have hbb : exists t. t + b = b
  6. 0006apply le_refl
  7. 0007have hall : forall z. exists d. ((((exists x. z = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. z = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
  8. 0008apply gcd_balanced_bezout_exists_up_to
  9. 0009exact hbb
  10. 0010specialize hall a
  11. 0011exact hall