PA00CM

signed_remainder_sum_mod_two

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

A lower/reflected signed remainder changes q+r to q+m+s only by an even amount.

Exact expanded PA statement

forall p q r m s. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))) -> (exists sdp_u_signed_sum_result sdp_v_signed_sum_result. (q + r) + 2 * sdp_u_signed_sum_result = (q + m + s) + 2 * sdp_v_signed_sum_result)

Structural proof guide

Generated structural guide

A lower/reflected signed remainder changes q+r to q+m+s only by an even amount.

Use the direct prerequisites odd_reflected_remainder_mod_two, mod_eq_refl, mod_eq_add, add_assoc as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (3), equality transport (6).

Referenced ingredients

PA00CL odd_reflected_remainder_mod_two PA0023 mod_eq_refl PA0022 mod_eq_add PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA00CL odd_reflected_remainder_mod_two PA0023 mod_eq_refl PA0022 mod_eq_add PA0009 add_assoc

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 q
  3. 0003intro r
  4. 0004intro m
  5. 0005intro s
  6. 0006intro hp
  7. 0007intro hbranch
  8. 0008cases hbranch
  9. 0009cases hbranch_left
  10. 0010rewrite hbranch_left_left
  11. 0011rewrite hbranch_left_right
  12. 0012exists 0
  13. 0013exists 0
  14. 0014rewrite PA5
  15. 0015rewrite PA5
  16. 0016symm
  17. 0017apply PA3
  18. 0018cases hbranch_right
  19. 0019have hrmod : exists sdp_u_proof_r_reflected sdp_v_proof_r_reflected. (r) + 2 * sdp_u_proof_r_reflected = (m + 1) + 2 * sdp_v_proof_r_reflected
  20. 0020specialize odd_reflected_remainder_mod_two p
  21. 0021specialize odd_reflected_remainder_mod_two r
  22. 0022specialize odd_reflected_remainder_mod_two m
  23. 0023apply odd_reflected_remainder_mod_two
  24. 0024exact hp
  25. 0025exact hbranch_right_right
  26. 0026have hqmod : exists sdp_u_proof_q_refl sdp_v_proof_q_refl. (q) + 2 * sdp_u_proof_q_refl = (q) + 2 * sdp_v_proof_q_refl
  27. 0027specialize mod_eq_refl 2
  28. 0028specialize mod_eq_refl q
  29. 0029exact mod_eq_refl
  30. 0030have hsum : exists sdp_u_proof_signed_upper sdp_v_proof_signed_upper. (q + r) + 2 * sdp_u_proof_signed_upper = (q + (m + 1)) + 2 * sdp_v_proof_signed_upper
  31. 0031specialize mod_eq_add 2
  32. 0032specialize mod_eq_add q
  33. 0033specialize mod_eq_add q
  34. 0034specialize mod_eq_add r
  35. 0035specialize mod_eq_add (m + 1)
  36. 0036apply mod_eq_add
  37. 0037exact hqmod
  38. 0038exact hrmod
  39. 0039rewrite hbranch_right_left
  40. 0040specialize add_assoc q
  41. 0041specialize add_assoc m
  42. 0042specialize add_assoc 1
  43. 0043rewrite add_assoc
  44. 0044exact hsum