PA00FK

mod_two_one_to_odd

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

Congruence to one modulo two supplies an odd witness.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Congruence to one modulo two supplies an odd witness.

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

The proof proceeds by case analysis (1), intermediate claims (1), closed numeral normalization (1).

Referenced ingredients

PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Proof neighborhood

Direct dependencies

PA002V mod_eq_to_remainder_decomposition PA000H mul_comm

Direct dependents

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 hone
  3. 0003have hdecomp : exists q. n = q * 2 + 1
  4. 0004specialize mod_eq_to_remainder_decomposition 2
  5. 0005specialize mod_eq_to_remainder_decomposition n
  6. 0006specialize mod_eq_to_remainder_decomposition 1
  7. 0007apply mod_eq_to_remainder_decomposition
  8. 0008intro htwo
  9. 0009apply PA1
  10. 0010exact htwo
  11. 0011exists 0
  12. 0012norm_num
  13. 0013exact hone
  14. 0014cases hdecomp
  15. 0015exists x
  16. 0016trans x * 2 + 1
  17. 0017exact hdecomp_witness
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl