BT002V

gcd_exists_relational

Stable · empty-context checked

Every pair of naturals has a relational greatest common divisor.

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)

Structural proof guide

Every pair of naturals has a relational greatest common divisor.

Direct prerequisites: le_refl, gcd_exists_up_to. The authored body proceeds by intermediate claims (2).

Proof neighborhood

Direct dependencies

BT000E le_refl BT002U gcd_exists_up_to

Direct dependents

BT003N euclid_prime_dvd_product BT008Q prime_coprime_or_divides

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. 0003specialize gcd_exists_up_to b
  4. 0004specialize gcd_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)
  8. 0008apply gcd_exists_up_to
  9. 0009exact hbb
  10. 0010specialize hall a
  11. 0011exact hall