PA00C4

predecessor_multiple_mod_complement

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

The predecessor multiplier is congruent to the complementary remainder.

Exact expanded PA statement

forall p k m t. p = S k -> t + m = p -> (exists wpp_mod_left_gsd_predecessor_mod wpp_mod_right_gsd_predecessor_mod. (k * m) + p * wpp_mod_left_gsd_predecessor_mod = (t) + p * wpp_mod_right_gsd_predecessor_mod)

Structural proof guide

Generated structural guide

The predecessor multiplier is congruent to the complementary remainder.

Use the direct prerequisites mul_one, mul_succ_left, add_assoc, add_comm as previously established PA formulas.

The proof proceeds by certified simplification (1).

Referenced ingredients

PA0002 mul_one PA000G mul_succ_left PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0002 mul_one PA000G mul_succ_left PA0009 add_assoc PA000F add_comm

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 k
  3. 0003intro m
  4. 0004intro t
  5. 0005intro hp
  6. 0006intro hsum
  7. 0007exists 1
  8. 0008exists m
  9. 0009trans k * m + p
  10. 0010congr
  11. 0011refl
  12. 0012apply mul_one
  13. 0013trans k * m + (t + m)
  14. 0014congr
  15. 0015refl
  16. 0016symm
  17. 0017exact hsum
  18. 0018trans t + (k * m + m)
  19. 0019simp [add_assoc, add_comm]
  20. 0020trans t + (S k) * m
  21. 0021congr
  22. 0022refl
  23. 0023symm
  24. 0024apply mul_succ_left
  25. 0025congr
  26. 0026refl
  27. 0027congr
  28. 0028symm
  29. 0029exact hp
  30. 0030refl