PA00C8

odd_multiplier_odd_product_iff

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

Multiplication by an odd natural preserves and reflects oddness.

Exact expanded PA statement

forall p q. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> ((((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

Multiplication by an odd natural preserves and reflects oddness.

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

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

Referenced ingredients

PA0057 parity_cases PA006E even_mul_right PA0056 odd_not_even PA006D odd_mul_odd

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA006E even_mul_right PA0056 odd_not_even PA006D odd_mul_odd

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. 0011exfalso
  12. 0012have hproduct_even : exists pod_even_odd_iff_contradiction. p * q = 2 * pod_even_odd_iff_contradiction
  13. 0013specialize even_mul_right p
  14. 0014specialize even_mul_right q
  15. 0015apply even_mul_right
  16. 0016exists x
  17. 0017exact hqcases_witness_left
  18. 0018specialize odd_not_even (p * q)
  19. 0019apply odd_not_even
  20. 0020exact hproduct
  21. 0021exact hproduct_even
  22. 0022exists x
  23. 0023exact hqcases_witness_right
  24. 0024intro hq
  25. 0025specialize odd_mul_odd p
  26. 0026specialize odd_mul_odd q
  27. 0027apply odd_mul_odd
  28. 0028exact hp
  29. 0029exact hq