PA0055

even_odd_exclusive_pointwise

Stable checked-use theorem · independently closed

An even and an odd decomposition of the same natural are incompatible.

Exact expanded PA statement

forall n a b. n = 2 * a -> n = 2 * b + 1 -> false

Structural proof guide

Generated structural guide

An even and an odd decomposition of the same natural are incompatible.

Use the direct prerequisites division_remainder_unique as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1), equality transport (1), certified simplification (1), closed numeral normalization (2).

Referenced ingredients

PA002E division_remainder_unique

Proof neighborhood

Direct dependencies

PA002E division_remainder_unique

Direct dependents

PA0056 odd_not_even PA0059 even_not_odd PA00BO double_predecessor_ne_one

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 a
  3. 0003intro b
  4. 0004intro he
  5. 0005intro ho
  6. 0006have hu : a = b /\ 0 = 1
  7. 0007specialize division_remainder_unique 2
  8. 0008specialize division_remainder_unique n
  9. 0009specialize division_remainder_unique a
  10. 0010specialize division_remainder_unique 0
  11. 0011specialize division_remainder_unique b
  12. 0012specialize division_remainder_unique 1
  13. 0013apply division_remainder_unique
  14. 0014rewrite he
  15. 0015simp
  16. 0016exists 1
  17. 0017norm_num
  18. 0018exact ho
  19. 0019exists 0
  20. 0020norm_num
  21. 0021cases hu
  22. 0022apply PA1
  23. 0023symm
  24. 0024exact hu_right