PA00C9 — odd_multiplier_parity

Exact expanded PA statement

forall p q. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> (((((exists pod_even_product_even. p * q = 2 * pod_even_product_even) -> (exists pod_even_factor_even. q = 2 * pod_even_factor_even)) /\ ((exists pod_even_factor_even. q = 2 * pod_even_factor_even) -> (exists pod_even_product_even. p * q = 2 * pod_even_product_even)))) /\ ((((exists pod_odd_product_odd. p * q = 2 * pod_odd_product_odd + 1) -> (exists pod_odd_factor_odd. q = 2 * pod_odd_factor_odd + 1)) /\ ((exists pod_odd_factor_odd. q = 2 * pod_odd_factor_odd + 1) -> (exists pod_odd_product_odd. p * q = 2 * pod_odd_product_odd + 1)))))

Structural proof guide

Generated structural guide

An odd multiplier preserves both parity classes exactly.

Use the direct prerequisites odd_multiplier_even_product_iff, odd_multiplier_odd_product_iff as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff

Proof neighborhood

Direct dependencies

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff

Direct dependents

PA00CK odd_product_division_mod_two

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.