PA005A

even_successor_to_odd

Stable checked-use theorem · independently closed

If a successor is even, its predecessor is odd.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

If a successor is even, its predecessor is odd.

Use the direct prerequisites parity_cases, successor_odd_of_even, even_not_odd as previously established PA formulas.

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

Referenced ingredients

PA0057 parity_cases PA0058 successor_odd_of_even PA0059 even_not_odd

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA0058 successor_odd_of_even PA0059 even_not_odd

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.

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