PA0059

even_not_odd

Stable checked-use theorem · independently closed

No even natural is odd.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

11 script commands · 3 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
even odd exclusive pointwise
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro he
  3. L3
    intro ho
02Separate the logical casesL4–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L4
    cases he
  2. L5
    cases ho
03Use earlier factsL6–11

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L6
    specialize even_odd_exclusive_pointwise n
  2. L7
    specialize even_odd_exclusive_pointwise x
  3. L8
    specialize even_odd_exclusive_pointwise x1
  4. L9
    apply even_odd_exclusive_pointwise
  5. L10
    exact he_witness
  6. L11
    exact ho_witness

Library-wide reading audit

Original exact command ledger · 11 lines
  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