PA001F

is_gcd_zero_right

Stable checked-use theorem · independently closed

Every natural is the relational gcd of itself and zero.

Exact expanded PA statement

forall a. (((exists x. a = a * x) /\ (exists y. 0 = a * y)) /\ forall c. (exists u. a = c * u) -> (exists v. 0 = c * v) -> exists w. a = c * w)

Structural proof guide

Generated structural guide

Every natural is the relational gcd of itself and zero.

Use the direct prerequisites multiple_refl, multiple_zero as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0019 multiple_refl PA001E multiple_zero

Proof neighborhood

Direct dependencies

PA0019 multiple_refl PA001E multiple_zero

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to

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. 0002split
  3. 0003split
  4. 0004specialize multiple_refl a
  5. 0005exact multiple_refl
  6. 0006specialize multiple_zero a
  7. 0007exact multiple_zero
  8. 0008intro c
  9. 0009intro ha
  10. 0010intro hz
  11. 0011exact ha