PA0056

odd_not_even

Stable checked-use theorem · independently closed

No odd natural is even.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

No odd natural is even.

Use the direct prerequisites even_odd_exclusive_pointwise as previously established PA formulas.

The proof proceeds by case analysis (2).

Referenced ingredients

PA0055 even_odd_exclusive_pointwise

Proof neighborhood

Direct dependencies

PA0055 even_odd_exclusive_pointwise

Direct dependents

PA005C odd_successor_to_even PA005E pow_predecessor_parity_mod PA00C8 odd_multiplier_odd_product_iff 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 n
  2. 0002intro ho
  3. 0003intro he
  4. 0004cases ho
  5. 0005cases he
  6. 0006specialize even_odd_exclusive_pointwise n
  7. 0007specialize even_odd_exclusive_pointwise x1
  8. 0008specialize even_odd_exclusive_pointwise x
  9. 0009apply even_odd_exclusive_pointwise
  10. 0010exact he_witness
  11. 0011exact ho_witness