PA00CN

odd_scaled_division_signed_mod_two

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

The generic Gauss-Eisenstein pointwise join: x == q+m+s modulo two.

Exact expanded PA statement

forall p a x q r m s. (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 -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))) -> (exists sdp_u_signed_final_result sdp_v_signed_final_result. (x) + 2 * sdp_u_signed_final_result = (q + m + s) + 2 * sdp_v_signed_final_result)

Structural proof guide

Generated structural guide

The generic Gauss-Eisenstein pointwise join: x == q+m+s modulo two.

Use the direct prerequisites odd_product_division_mod_two, signed_remainder_sum_mod_two, mod_eq_trans as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA00CK odd_product_division_mod_two PA00CM signed_remainder_sum_mod_two PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00CK odd_product_division_mod_two PA00CM signed_remainder_sum_mod_two PA0024 mod_eq_trans

Direct dependents

PA00CO odd_signed_division_congruence_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 m
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hdivision
  11. 0011intro hbranch
  12. 0012have hxqr : exists sdp_u_proof_final_x_qr sdp_v_proof_final_x_qr. (x) + 2 * sdp_u_proof_final_x_qr = (q + r) + 2 * sdp_v_proof_final_x_qr
  13. 0013specialize odd_product_division_mod_two p
  14. 0014specialize odd_product_division_mod_two a
  15. 0015specialize odd_product_division_mod_two x
  16. 0016specialize odd_product_division_mod_two q
  17. 0017specialize odd_product_division_mod_two r
  18. 0018apply odd_product_division_mod_two
  19. 0019exact hp
  20. 0020exact ha
  21. 0021exact hdivision
  22. 0022have hqrsigned : exists sdp_u_proof_final_qr_signed sdp_v_proof_final_qr_signed. (q + r) + 2 * sdp_u_proof_final_qr_signed = (q + m + s) + 2 * sdp_v_proof_final_qr_signed
  23. 0023specialize signed_remainder_sum_mod_two p
  24. 0024specialize signed_remainder_sum_mod_two q
  25. 0025specialize signed_remainder_sum_mod_two r
  26. 0026specialize signed_remainder_sum_mod_two m
  27. 0027specialize signed_remainder_sum_mod_two s
  28. 0028apply signed_remainder_sum_mod_two
  29. 0029exact hp
  30. 0030exact hbranch
  31. 0031specialize mod_eq_trans 2
  32. 0032specialize mod_eq_trans x
  33. 0033specialize mod_eq_trans (q + r)
  34. 0034specialize mod_eq_trans (q + m + s)
  35. 0035apply mod_eq_trans
  36. 0036exact hxqr
  37. 0037exact hqrsigned