PA005C

odd_successor_to_even

Stable checked-use theorem · independently closed

If a successor is odd, its predecessor is even.

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.

  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