PA00C5

canonical_remainder_from_mod

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

A bounded value congruent to an exact division input is its canonical remainder.

Exact expanded PA statement

forall p n q r t. n = p * q + r -> (exists gsp_lt_gap_gsd_r_below_p. gsp_lt_gap_gsd_r_below_p + S r = p) -> (exists gsp_lt_gap_gsd_canonical_t_below. gsp_lt_gap_gsd_canonical_t_below + S t = p) -> (exists wpp_mod_left_gsd_n_mod_t wpp_mod_right_gsd_n_mod_t. (n) + p * wpp_mod_left_gsd_n_mod_t = (t) + p * wpp_mod_right_gsd_n_mod_t) -> r = t

Structural proof guide

Generated structural guide

A bounded value congruent to an exact division input is its canonical remainder.

Use the direct prerequisites mul_comm, remainder_decomposition_to_mod_eq, mod_eq_symm, mod_eq_trans, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by intermediate claims (4).

Referenced ingredients

PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct dependents

PA00C6 odd_signed_division_branch_exact

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 n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro t
  6. 0006intro hdivision
  7. 0007intro hrbelow
  8. 0008intro htbelow
  9. 0009intro hnmodt
  10. 0010have hdirected : n = q * p + r
  11. 0011trans p * q + r
  12. 0012exact hdivision
  13. 0013congr
  14. 0014apply mul_comm
  15. 0015refl
  16. 0016have hnmodr : exists wpp_mod_left_gsd_proof_n_mod_r wpp_mod_right_gsd_proof_n_mod_r. (n) + p * wpp_mod_left_gsd_proof_n_mod_r = (r) + p * wpp_mod_right_gsd_proof_n_mod_r
  17. 0017specialize remainder_decomposition_to_mod_eq p
  18. 0018specialize remainder_decomposition_to_mod_eq n
  19. 0019specialize remainder_decomposition_to_mod_eq q
  20. 0020specialize remainder_decomposition_to_mod_eq r
  21. 0021apply remainder_decomposition_to_mod_eq
  22. 0022exact hdirected
  23. 0023have hrmodn : exists wpp_mod_left_gsd_proof_r_mod_n wpp_mod_right_gsd_proof_r_mod_n. (r) + p * wpp_mod_left_gsd_proof_r_mod_n = (n) + p * wpp_mod_right_gsd_proof_r_mod_n
  24. 0024specialize mod_eq_symm p
  25. 0025specialize mod_eq_symm n
  26. 0026specialize mod_eq_symm r
  27. 0027apply mod_eq_symm
  28. 0028exact hnmodr
  29. 0029have hrmodt : exists wpp_mod_left_gsd_proof_r_mod_t wpp_mod_right_gsd_proof_r_mod_t. (r) + p * wpp_mod_left_gsd_proof_r_mod_t = (t) + p * wpp_mod_right_gsd_proof_r_mod_t
  30. 0030specialize mod_eq_trans p
  31. 0031specialize mod_eq_trans r
  32. 0032specialize mod_eq_trans n
  33. 0033specialize mod_eq_trans t
  34. 0034apply mod_eq_trans
  35. 0035exact hrmodn
  36. 0036exact hnmodt
  37. 0037specialize mod_eq_bounded_unique p
  38. 0038specialize mod_eq_bounded_unique r
  39. 0039specialize mod_eq_bounded_unique t
  40. 0040apply mod_eq_bounded_unique
  41. 0041exact hrbelow
  42. 0042exact htbelow
  43. 0043exact hrmodt