PA0059

even_not_odd

Stable checked-use theorem · independently closed

No even natural is odd.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

No even natural is odd.

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

PA005A even_successor_to_odd PA00C7 odd_multiplier_even_product_iff PA00CA even_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 he
  3. 0003intro ho
  4. 0004cases he
  5. 0005cases ho
  6. 0006specialize even_odd_exclusive_pointwise n
  7. 0007specialize even_odd_exclusive_pointwise x
  8. 0008specialize even_odd_exclusive_pointwise x1
  9. 0009apply even_odd_exclusive_pointwise
  10. 0010exact he_witness
  11. 0011exact ho_witness