PA005C

odd_successor_to_even

Stable checked-use theorem · independently closed

If a successor is odd, its predecessor is even.

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. S n = 2 * a + 1) -> exists b. n = 2 * b

Structural proof guide

Generated structural guide

If a successor is odd, its predecessor is even.

Use the direct prerequisites parity_cases, successor_even_of_odd, odd_not_even as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (1).

Referenced ingredients

PA0057 parity_cases PA005B successor_even_of_odd PA0056 odd_not_even

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA005B successor_even_of_odd PA0056 odd_not_even

Direct dependents

PA005E pow_predecessor_parity_mod

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

17 script commands · 9 reading checkpoints · 1 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 (3)
parity casessuccessor even of oddodd not even
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hso
02Use earlier factsL3–3

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

  1. L3
    specialize parity_cases n
03Separate the logical casesL4–5

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

  1. L4
    cases parity_cases
  2. L5
    cases parity_cases_witness
04Construct an explicit witnessL6–6

Supply the displayed value, then prove that it has the required property.

  1. L6
    exists x
05Use earlier factsL7–7

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

  1. L7
    exact parity_cases_witness_left
06Separate the logical casesL8–8

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

  1. L8
    exfalso
07Establish hseL9–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply successor even of odd.

  1. L9
    have hse : exists b. S n = 2 * b
  2. L10
    specialize successor_even_of_odd n
  3. L11
    apply successor_even_of_odd
08Construct an explicit witnessL12–12

Supply the displayed value, then prove that it has the required property.

  1. L12
    exists x
09Use earlier factsL13–17

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

  1. L13
    exact parity_cases_witness_right
  2. L14
    specialize odd_not_even (S n)
  3. L15
    apply odd_not_even
  4. L16
    exact hso
  5. L17
    exact hse

Library-wide reading audit

Original exact command ledger · 17 lines
  1. 0001intro n
  2. 0002intro hso
  3. 0003specialize parity_cases n
  4. 0004cases parity_cases
  5. 0005cases parity_cases_witness
  6. 0006exists x
  7. 0007exact parity_cases_witness_left
  8. 0008exfalso
  9. 0009have hse : exists b. S n = 2 * b
  10. 0010specialize successor_even_of_odd n
  11. 0011apply successor_even_of_odd
  12. 0012exists x
  13. 0013exact parity_cases_witness_right
  14. 0014specialize odd_not_even (S n)
  15. 0015apply odd_not_even
  16. 0016exact hso
  17. 0017exact hse