PA0036

gcd_exists_relational

Stable checked-use theorem · independently closed

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

Generated structural guide

Every pair of naturals has a relational greatest common divisor.

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

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA001A le_refl PA0035 gcd_exists_up_to

Proof neighborhood

Direct dependencies

PA001A le_refl PA0035 gcd_exists_up_to

Direct dependents

PA0038 euclid_prime_dvd_product PA003M prime_coprime_or_divides

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.

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