PA006D

odd_mul_odd

Stable checked-use theorem · independently closed

The product of two odd naturals is odd.

Exact expanded PA statement

forall m n. (exists a. m = 2 * a + 1) -> (exists b. n = 2 * b + 1) -> exists c. m * n = 2 * c + 1

Structural proof guide

Generated structural guide

The product of two odd naturals is odd.

Use the direct prerequisites mul_add, add_mul, add_assoc, add_succ_left, mul_double_right as previously established PA formulas.

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

Referenced ingredients

PA000A mul_add PA0016 add_mul PA0009 add_assoc PA000E add_succ_left PA006C mul_double_right

Proof neighborhood

Direct dependencies

PA000A mul_add PA0016 add_mul PA0009 add_assoc PA000E add_succ_left PA006C mul_double_right

Direct dependents

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00FU qres_opposite_status_from_mod_four_three

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 m
  2. 0002intro n
  3. 0003intro hm
  4. 0004intro hn
  5. 0005cases hm
  6. 0006cases hn
  7. 0007exists (2 * x + 1) * x1 + x
  8. 0008rewrite hm_witness
  9. 0009rewrite hn_witness
  10. 0010simp [mul_add, add_mul, add_assoc, add_succ_left]
  11. 0011congr
  12. 0012congr
  13. 0013apply mul_double_right
  14. 0014refl