PA00CC

odd_division_even_iff

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

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

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_even_division_n_even. n = 2 * pod_even_division_n_even) -> (exists pod_even_division_qr_even. q + r = 2 * pod_even_division_qr_even)) /\ ((exists pod_even_division_qr_even. q + r = 2 * pod_even_division_qr_even) -> (exists pod_even_division_n_even. n = 2 * pod_even_division_n_even))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites odd_multiplier_even_product_iff, odd_multiplier_odd_product_iff, even_sum_iff_same_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 PA00CB even_sum_iff_same_parity

Proof neighborhood

Direct dependencies

PA00C7 odd_multiplier_even_product_iff PA00C8 odd_multiplier_odd_product_iff PA00CB even_sum_iff_same_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even) -> ((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1))))) /\ (((((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))) -> (exists pod_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even)))
  18. 0018specialize even_sum_iff_same_parity (p * q)
  19. 0019specialize even_sum_iff_same_parity r
  20. 0020exact even_sum_iff_same_parity
  21. 0021have hright : (((exists pod_even_proof_qr_even. q + r = 2 * pod_even_proof_qr_even) -> ((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1))))) /\ (((((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))) -> (exists pod_even_proof_qr_even. q + r = 2 * pod_even_proof_qr_even)))
  22. 0022specialize even_sum_iff_same_parity q
  23. 0023specialize even_sum_iff_same_parity r
  24. 0024exact even_sum_iff_same_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_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  32. 0032rewrite <- hdivision
  33. 0033exact hn
  34. 0034apply hright_right
  35. 0035have hsame : (((exists pod_even_proof_pq_even. p * q = 2 * pod_even_proof_pq_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_pq_odd. p * q = 2 * pod_odd_proof_pq_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  36. 0036apply hleft_left
  37. 0037exact hpqr
  38. 0038cases hsame
  39. 0039cases hsame_left
  40. 0040left
  41. 0041split
  42. 0042apply hmul_even_left
  43. 0043exact hsame_left_left
  44. 0044exact hsame_left_right
  45. 0045cases hsame_right
  46. 0046right
  47. 0047split
  48. 0048apply hmul_odd_left
  49. 0049exact hsame_right_left
  50. 0050exact hsame_right_right
  51. 0051intro hqr
  52. 0052have hpqr : exists pod_even_proof_pqr_even. p * q + r = 2 * pod_even_proof_pqr_even
  53. 0053apply hleft_right
  54. 0054have hsame : (((exists pod_even_proof_q_even. q = 2 * pod_even_proof_q_even) /\ (exists pod_even_proof_r_even. r = 2 * pod_even_proof_r_even)) \/ ((exists pod_odd_proof_q_odd. q = 2 * pod_odd_proof_q_odd + 1) /\ (exists pod_odd_proof_r_odd. r = 2 * pod_odd_proof_r_odd + 1)))
  55. 0055apply hright_left
  56. 0056exact hqr
  57. 0057cases hsame
  58. 0058cases hsame_left
  59. 0059left
  60. 0060split
  61. 0061apply hmul_even_right
  62. 0062exact hsame_left_left
  63. 0063exact hsame_left_right
  64. 0064cases hsame_right
  65. 0065right
  66. 0066split
  67. 0067apply hmul_odd_right
  68. 0068exact hsame_right_left
  69. 0069exact hsame_right_right
  70. 0070rewrite hdivision
  71. 0071exact hpqr