PA00BO

double_predecessor_ne_one

Alpha v16 checked-use theorem · independently closed; not Stable

A doubled predecessor cannot equal one.

Exact expanded PA statement

forall n h. n = h + h -> ~(n = 1)

Structural proof guide

Generated structural guide

A doubled predecessor cannot equal one.

Use the direct prerequisites even_odd_exclusive_pointwise, mul_comm, zero_add as previously established PA formulas.

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

Referenced ingredients

PA0055 even_odd_exclusive_pointwise PA000H mul_comm PA0001 zero_add

Proof neighborhood

Direct dependencies

PA0055 even_odd_exclusive_pointwise PA000H mul_comm PA0001 zero_add

Direct dependents

PA00BP odd_prime_one_not_mod_predecessor

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro n
  2. 0002intro h
  3. 0003intro heven
  4. 0004intro hone
  5. 0005have heven_two : n = 2 * h
  6. 0006trans h + h
  7. 0007exact heven
  8. 0008trans h * 2
  9. 0009simp [zero_add]
  10. 0010specialize mul_comm h
  11. 0011specialize mul_comm 2
  12. 0012apply mul_comm
  13. 0013have hone_odd : n = 2 * 0 + 1
  14. 0014rewrite hone
  15. 0015norm_num
  16. 0016specialize even_odd_exclusive_pointwise n
  17. 0017specialize even_odd_exclusive_pointwise h
  18. 0018specialize even_odd_exclusive_pointwise 0
  19. 0019apply even_odd_exclusive_pointwise
  20. 0020exact heven_two
  21. 0021exact hone_odd