PA00CK

odd_product_division_mod_two

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

Odd scale and modulus transport an exact division equation to x == q+r modulo two.

Exact expanded PA statement

forall p a x q r. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> (exists sdp_odd_scale. a = 2 * sdp_odd_scale + 1) -> a * x = p * q + r -> (exists sdp_u_product_division_result sdp_v_product_division_result. (x) + 2 * sdp_u_product_division_result = (q + r) + 2 * sdp_v_product_division_result)

Structural proof guide

Generated structural guide

Odd scale and modulus transport an exact division equation to x == q+r modulo two.

Use the direct prerequisites parity_cases, odd_multiplier_parity_iff, odd_division_parity_iff, matching_parity_mod_two as previously established PA formulas.

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

Referenced ingredients

PA0057 parity_cases PA00C9 odd_multiplier_parity_iff PA00CG odd_division_parity_iff PA00CJ matching_parity_mod_two

Proof neighborhood

Direct dependencies

PA0057 parity_cases PA00C9 odd_multiplier_parity_iff PA00CG odd_division_parity_iff PA00CJ matching_parity_mod_two

Direct dependents

PA00CN odd_scaled_division_signed_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.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hp
  7. 0007intro ha
  8. 0008intro hdivision
  9. 0009have hproduct : ((((exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even) -> (exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even)) /\ ((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) -> (exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even))) /\ (((exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1) -> (exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1)) /\ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) -> (exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1))))
  10. 0010specialize odd_multiplier_parity_iff a
  11. 0011specialize odd_multiplier_parity_iff x
  12. 0012apply odd_multiplier_parity_iff
  13. 0013exact ha
  14. 0014have hquotient : ((((exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even) -> (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) /\ ((exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even) -> (exists sdp_even_proof_ax_even. a * x = 2 * sdp_even_proof_ax_even))) /\ (((exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1) -> (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)) /\ ((exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1) -> (exists sdp_odd_proof_ax_odd. a * x = 2 * sdp_odd_proof_ax_odd + 1))))
  15. 0015specialize odd_division_parity_iff p
  16. 0016specialize odd_division_parity_iff q
  17. 0017specialize odd_division_parity_iff r
  18. 0018specialize odd_division_parity_iff (a * x)
  19. 0019apply odd_division_parity_iff
  20. 0020exact hp
  21. 0021exact hdivision
  22. 0022cases hproduct
  23. 0023cases hproduct_left
  24. 0024cases hproduct_right
  25. 0025cases hquotient
  26. 0026cases hquotient_left
  27. 0027cases hquotient_right
  28. 0028have hxcases : exists k. x = 2 * k \/ x = 2 * k + 1
  29. 0029specialize parity_cases x
  30. 0030exact parity_cases
  31. 0031cases hxcases
  32. 0032cases hxcases_witness
  33. 0033have hmatching : (((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) /\ (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) \/ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) /\ (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)))
  34. 0034left
  35. 0035split
  36. 0036exists x1
  37. 0037exact hxcases_witness_left
  38. 0038apply hquotient_left_left
  39. 0039apply hproduct_left_right
  40. 0040exists x1
  41. 0041exact hxcases_witness_left
  42. 0042specialize matching_parity_mod_two x
  43. 0043specialize matching_parity_mod_two (q + r)
  44. 0044apply matching_parity_mod_two
  45. 0045exact hmatching
  46. 0046have hmatching : (((exists sdp_even_proof_x_even. x = 2 * sdp_even_proof_x_even) /\ (exists sdp_even_proof_qr_even. q + r = 2 * sdp_even_proof_qr_even)) \/ ((exists sdp_odd_proof_x_odd. x = 2 * sdp_odd_proof_x_odd + 1) /\ (exists sdp_odd_proof_qr_odd. q + r = 2 * sdp_odd_proof_qr_odd + 1)))
  47. 0047right
  48. 0048split
  49. 0049exists x1
  50. 0050exact hxcases_witness_right
  51. 0051apply hquotient_right_left
  52. 0052apply hproduct_right_right
  53. 0053exists x1
  54. 0054exact hxcases_witness_right
  55. 0055specialize matching_parity_mod_two x
  56. 0056specialize matching_parity_mod_two (q + r)
  57. 0057apply matching_parity_mod_two
  58. 0058exact hmatching