BT002V

gcd_exists_relational

Stable checked-use theorem · independently kernel verified

Every pair of naturals has a relational greatest common divisor.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

11 script commands · 4 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
le reflgcd exists up to
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
02Use earlier factsL3–4

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L3
    specialize gcd_exists_up_to b
  2. L4
    specialize gcd_exists_up_to b
03Establish hbbL5–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le refl.

  1. L5
    have hbb : exists t. t + b = b
  2. L6
    apply le_refl
04Establish hallL7–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gcd exists up to.

  1. L7
    have 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)
  2. L8
    apply gcd_exists_up_to
  3. L9
    exact hbb
  4. L10
    specialize hall a
  5. L11
    exact hall

Library-wide reading audit

Original exact command ledger · 11 lines
  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