PA00CF

odd_division_odd_iff

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

For odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.

Exact expanded PA statement

forall p q r n. (exists pod_odd_multiplier. p = 2 * pod_odd_multiplier + 1) -> n = p * q + r -> ((((exists pod_odd_division_n_odd. n = 2 * pod_odd_division_n_odd + 1) -> (exists pod_odd_division_qr_odd. q + r = 2 * pod_odd_division_qr_odd + 1)) /\ ((exists pod_odd_division_qr_odd. q + r = 2 * pod_odd_division_qr_odd + 1) -> (exists pod_odd_division_n_odd. n = 2 * pod_odd_division_n_odd + 1))))

Structural proof guide

Generated structural guide

For odd divisor coefficient p, n=p*q+r is odd exactly when q+r is odd.

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

The proof proceeds by case analysis (10), intermediate claims (8), equality transport (2).

Referenced ingredients

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CE odd_sum_iff_opposite_parity

Proof neighborhood

Direct dependencies

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CE odd_sum_iff_opposite_parity

Direct dependents

PA00CG odd_division_parity_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 r
  4. 0004intro n
  5. 0005intro hp
  6. 0006intro hdivision
  7. 0007have hmul_even : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) -> (exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even)) /\ ((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) -> (exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even)))
  8. 0008specialize odd_multiplier_even_product_iff p
  9. 0009specialize odd_multiplier_even_product_iff q
  10. 0010apply odd_multiplier_even_product_iff
  11. 0011exact hp
  12. 0012have hmul_odd : (((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) -> (exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1)) /\ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) -> (exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1)))
  13. 0013specialize odd_multiplier_odd_product_iff p
  14. 0014specialize odd_multiplier_odd_product_iff q
  15. 0015apply odd_multiplier_odd_product_iff
  16. 0016exact hp
  17. 0017have hleft : (((exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1) -> ((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even))))) /\ (((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))) -> (exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1)))
  18. 0018specialize odd_sum_iff_opposite_parity (p * q)
  19. 0019specialize odd_sum_iff_opposite_parity r
  20. 0020exact odd_sum_iff_opposite_parity
  21. 0021have hright : (((exists pod_odd_proof_qr_odd. q + r = 2 * pod_odd_proof_qr_odd + 1) -> ((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even))))) /\ (((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))) -> (exists pod_odd_proof_qr_odd. q + r = 2 * pod_odd_proof_qr_odd + 1)))
  22. 0022specialize odd_sum_iff_opposite_parity q
  23. 0023specialize odd_sum_iff_opposite_parity r
  24. 0024exact odd_sum_iff_opposite_parity
  25. 0025cases hmul_even
  26. 0026cases hmul_odd
  27. 0027cases hleft
  28. 0028cases hright
  29. 0029split
  30. 0030intro hn
  31. 0031have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  32. 0032rewrite <- hdivision
  33. 0033exact hn
  34. 0034apply hright_right
  35. 0035have hopposite : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  36. 0036apply hleft_left
  37. 0037exact hpqr
  38. 0038cases hopposite
  39. 0039cases hopposite_left
  40. 0040left
  41. 0041split
  42. 0042apply hmul_even_left
  43. 0043exact hopposite_left_left
  44. 0044exact hopposite_left_right
  45. 0045cases hopposite_right
  46. 0046right
  47. 0047split
  48. 0048apply hmul_odd_left
  49. 0049exact hopposite_right_left
  50. 0050exact hopposite_right_right
  51. 0051intro hqr
  52. 0052have hpqr : exists pod_odd_proof_pqr_odd. p * q + r = 2 * pod_odd_proof_pqr_odd + 1
  53. 0053apply hleft_right
  54. 0054have hopposite : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)))
  55. 0055apply hright_left
  56. 0056exact hqr
  57. 0057cases hopposite
  58. 0058cases hopposite_left
  59. 0059left
  60. 0060split
  61. 0061apply hmul_even_right
  62. 0062exact hopposite_left_left
  63. 0063exact hopposite_left_right
  64. 0064cases hopposite_right
  65. 0065right
  66. 0066split
  67. 0067apply hmul_odd_right
  68. 0068exact hopposite_right_left
  69. 0069exact hopposite_right_right
  70. 0070rewrite hdivision
  71. 0071exact hpqr