PA000J

add_eq_zero_left

Stable checked-use theorem · independently closed

A sum equal to zero has zero as its left addend.

Exact expanded PA statement

forall a b. a + b = 0 -> a = 0

Structural proof guide

Generated structural guide

A sum equal to zero has zero as its left addend.

Use the direct prerequisites add_comm, add_eq_zero_right as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000F add_comm PA0004 add_eq_zero_right

Proof neighborhood

Direct dependencies

PA000F add_comm PA0004 add_eq_zero_right

Direct dependents

PA000K bounded_common_multiple_exists PA007C gauss_signed_half_magnitude_injective

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. 0003intro h
  4. 0004specialize add_eq_zero_right b
  5. 0005specialize add_eq_zero_right a
  6. 0006apply add_eq_zero_right
  7. 0007trans a + b
  8. 0008apply add_comm
  9. 0009exact h