PA006G

odd_add_even

Stable checked-use theorem · independently closed

An odd natural plus an even natural is odd.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

An odd natural plus an even natural is odd.

Use the direct prerequisites mul_add, add_succ_left 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

Proof neighborhood

Direct dependencies

PA000A mul_add PA000E add_succ_left

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_succ_left]