PA00C7

odd_multiplier_even_product_iff

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

Multiplication by an odd natural preserves and reflects evenness.

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))))

Structural proof guide

Generated structural guide

Multiplication by an odd natural preserves and reflects evenness.

Use the direct prerequisites parity_cases, odd_mul_odd, even_not_odd, even_mul_right as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2).

Referenced ingredients

PA0057 parity_cases PA006D odd_mul_odd PA0059 even_not_odd PA006E even_mul_right

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA006D odd_mul_odd PA0059 even_not_odd PA006E even_mul_right

Direct dependents

PA00C9 odd_multiplier_parity_iff PA00CC odd_division_even_iff PA00CF odd_division_odd_iff

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 p
  2. 0002intro q
  3. 0003intro hp
  4. 0004split
  5. 0005intro hproduct
  6. 0006have hqcases : exists k. q = 2 * k \/ q = 2 * k + 1
  7. 0007specialize parity_cases q
  8. 0008exact parity_cases
  9. 0009cases hqcases
  10. 0010cases hqcases_witness
  11. 0011exists x
  12. 0012exact hqcases_witness_left
  13. 0013exfalso
  14. 0014have hproduct_odd : exists pod_odd_even_iff_contradiction. p * q = 2 * pod_odd_even_iff_contradiction + 1
  15. 0015specialize odd_mul_odd p
  16. 0016specialize odd_mul_odd q
  17. 0017apply odd_mul_odd
  18. 0018exact hp
  19. 0019exists x
  20. 0020exact hqcases_witness_right
  21. 0021specialize even_not_odd (p * q)
  22. 0022apply even_not_odd
  23. 0023exact hproduct
  24. 0024exact hproduct_odd
  25. 0025intro hq
  26. 0026specialize even_mul_right p
  27. 0027specialize even_mul_right q
  28. 0028apply even_mul_right
  29. 0029exact hq