PA006I

odd_add_odd

Stable checked-use theorem · independently closed

The sum of two odd naturals is even.

Exact expanded PA statement

forall m n. (exists a. m = 2 * a + 1) -> (exists b. n = 2 * b + 1) -> exists c. m + n = 2 * c

Structural proof guide

Generated structural guide

The sum of two odd naturals is even.

Use the direct prerequisites mul_add, add_succ_left, add_assoc, add_comm as previously established PA formulas.

The proof proceeds by case analysis (2), equality transport (2), certified simplification (1).

Referenced ingredients

PA000A mul_add PA000E add_succ_left PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA000A mul_add PA000E add_succ_left PA0009 add_assoc PA000F add_comm

Direct dependents

PA00CB even_sum_iff_same_parity PA00CD odd_sum_parity_cases

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 m
  2. 0002intro n
  3. 0003intro hm
  4. 0004intro hn
  5. 0005cases hm
  6. 0006cases hn
  7. 0007exists x + x1 + 1
  8. 0008rewrite hm_witness
  9. 0009rewrite hn_witness
  10. 0010simp [mul_add, add_assoc, add_comm]