PA00C4 · theorem

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.

Statement with defined notation

∀ p. ∀ k. ∀ m. ∀ t. p = S k → t + m = p → ModEq(p,k · m,t)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA0002 mul_one PA000G mul_succ_left PA0009 add_assoc PA000F add_comm

Direct theorem dependents

PA00C6 odd_signed_division_branch_exact

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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