PA00C4

predecessor_multiple_mod_complement

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

The predecessor multiplier is congruent to the complementary remainder.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

30 script commands · 11 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
mul onemul succ left
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro m
  4. L4
    intro t
  5. L5
    intro hp
  6. L6
    intro hsum
02Construct an explicit witnessL7–8

Supply the displayed value, then prove that it has the required property.

  1. L7
    exists 1
  2. L8
    exists m
03Calculate and transport equalitiesL9–11

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    trans k * m + p
  2. L10
    congr
  3. L11
    refl
04Use earlier factsL12–12

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L12
    apply mul_one
05Calculate and transport equalitiesL13–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    trans k * m + (t + m)
  2. L14
    congr
  3. L15
    refl
  4. L16
    symm
06Use earlier factsL17–17

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    exact hsum
07Calculate and transport equalitiesL18–23

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L18
    trans t + (k * m + m)
  2. L19
    simp [add_assoc, add_comm]
  3. L20
    trans t + (S k) * m
  4. L21
    congr
  5. L22
    refl
  6. L23
    symm
08Use earlier factsL24–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    apply mul_succ_left
09Calculate and transport equalitiesL25–28

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    congr
  2. L26
    refl
  3. L27
    congr
  4. L28
    symm
10Use earlier factsL29–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact hp
11Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    refl

Library-wide reading audit

Original exact command ledger · 30 lines
  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