PA006E

even_mul_right

Stable checked-use theorem · independently closed

A product with an even right factor is even.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A product with an even right factor is even.

Use the direct prerequisites mul_double_right as previously established PA formulas.

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

Referenced ingredients

PA006C mul_double_right

Proof neighborhood

Direct dependencies

PA006C mul_double_right

Direct dependents

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00FO qres_same_status_from_mod_four_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 m
  2. 0002intro n
  3. 0003intro hn
  4. 0004cases hn
  5. 0005exists m * x
  6. 0006rewrite hn_witness
  7. 0007apply mul_double_right