PA006F

even_add_odd

Stable checked-use theorem · independently closed

An even natural plus an odd natural is odd.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

An even natural plus an odd natural is odd.

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

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

Referenced ingredients

PA000A mul_add PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA000A mul_add PA0009 add_assoc

Direct dependents

PA00CA even_sum_parity_cases PA00CE odd_sum_iff_opposite_parity

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
  8. 0008rewrite hm_witness
  9. 0009rewrite hn_witness
  10. 0010simp [mul_add, add_assoc]