PA005C · theorem

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.

Statement with defined notation

∀ n. Odd(S n) → Even(n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0009 Even PD0010 Odd

2 occurrences

In local proof propositions

PD0009 Even

1 occurrences

Exact expanded native-PA statement
forall n. (exists a. S n = 2 * a + 1) -> exists b. n = 2 * b

Proof neighborhood

Direct theorem prerequisites

PA0057 parity_cases PA005B successor_even_of_odd PA0056 odd_not_even

Direct theorem dependents

PA005E pow_predecessor_parity_mod

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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 defined 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 : Even(S n)
    Exact native replay linehave 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