PA00CI

odd_to_mod_two_one

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

Every odd natural is congruent to one modulo two.

Exact expanded PA statement

forall n. (exists pmt_odd_n. n = 2 * pmt_odd_n + 1) -> (exists pmt_u_n_one pmt_v_n_one. n + 2 * pmt_u_n_one = 1 + 2 * pmt_v_n_one)

Structural proof guide

Generated structural guide

Every odd natural is congruent to one modulo two.

Use the direct prerequisites add_comm as previously established PA formulas.

The proof proceeds by case analysis (1), equality transport (1), certified simplification (2).

Referenced ingredients

PA000F add_comm

Proof neighborhood

Direct dependencies

PA000F add_comm

Direct dependents

PA00CJ matching_parity_mod_two PA00FL mod_two_preserves_parity

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 hodd
  3. 0003cases hodd
  4. 0004exists 0
  5. 0005exists x
  6. 0006rewrite hodd_witness
  7. 0007simp
  8. 0008symm
  9. 0009trans 2 * x + 1
  10. 0010apply add_comm
  11. 0011simp