BT011C · Bertrand theorem

scaled_remainder_lift

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Scale a quotient-remainder equation and normalize its new tail.

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

forall d x q t c r s u. x = d * q + t -> c * t + r = d * s + u -> c * x + r = d * (c * q + s) + u

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall d x q t c r s u. x = d * q + t -> c * t + r = d * s + u -> c * x + r = d * (c * q + s) + u

Proof neighborhood

Direct theorem prerequisites

BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT0003 add_assoc

Direct theorem dependents

BT011E double_scaled_remainder_lift BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

39 script commands · 6 reading checkpoints · 4 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 (4)
mul addmul assocmul commadd assoc
01Fix variables and assumptionsL1–10

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

  1. L1
    intro d
  2. L2
    intro x
  3. L3
    intro q
  4. L4
    intro t
  5. L5
    intro c
  6. L6
    intro r
  7. L7
    intro s
  8. L8
    intro u
  9. L9
    intro hx
  10. L10
    intro htail
02Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite hx
03Establish hdistL12–17

Establish this local claim before using it. It is not an additional assumption.

  1. L12
    have hdist : c * (d * q + t) = c * (d * q) + c * t
  2. L13
    specialize mul_add c
  3. L14
    specialize mul_add (d * q)
  4. L15
    specialize mul_add t
  5. L16
    exact mul_add
  6. L17
    rewrite hdist
04Establish hassocL18–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L18
    have hassoc : (c * (d * q) + c * t) + r = c * (d * q) + (c * t + r)
  2. L19
    apply add_assoc
  3. L20
    rewrite hassoc
  4. L21
    rewrite htail
05Establish hfrontL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L22
    have hfront : c * (d * q) = d * (c * q)
  2. L23
    trans (c * d) * q
  3. L24
    symm
  4. L25
    apply mul_assoc
  5. L26
    trans (d * c) * q
  6. L27
    congr
  7. L28
    apply mul_comm
  8. L29
    refl
  9. L30
    apply mul_assoc
  10. L31
    rewrite hfront
06Establish hdist2L32–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add assoc.

  1. L32
    have hdist2 : d * (c * q + s) = d * (c * q) + d * s
  2. L33
    specialize mul_add d
  3. L34
    specialize mul_add (c * q)
  4. L35
    specialize mul_add s
  5. L36
    exact mul_add
  6. L37
    rewrite hdist2
  7. L38
    symm
  8. L39
    apply add_assoc

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro d
  2. 0002intro x
  3. 0003intro q
  4. 0004intro t
  5. 0005intro c
  6. 0006intro r
  7. 0007intro s
  8. 0008intro u
  9. 0009intro hx
  10. 0010intro htail
  11. 0011rewrite hx
  12. 0012have hdist : c * (d * q + t) = c * (d * q) + c * t
  13. 0013specialize mul_add c
  14. 0014specialize mul_add (d * q)
  15. 0015specialize mul_add t
  16. 0016exact mul_add
  17. 0017rewrite hdist
  18. 0018have hassoc : (c * (d * q) + c * t) + r = c * (d * q) + (c * t + r)
  19. 0019apply add_assoc
  20. 0020rewrite hassoc
  21. 0021rewrite htail
  22. 0022have hfront : c * (d * q) = d * (c * q)
  23. 0023trans (c * d) * q
  24. 0024symm
  25. 0025apply mul_assoc
  26. 0026trans (d * c) * q
  27. 0027congr
  28. 0028apply mul_comm
  29. 0029refl
  30. 0030apply mul_assoc
  31. 0031rewrite hfront
  32. 0032have hdist2 : d * (c * q + s) = d * (c * q) + d * s
  33. 0033specialize mul_add d
  34. 0034specialize mul_add (c * q)
  35. 0035specialize mul_add s
  36. 0036exact mul_add
  37. 0037rewrite hdist2
  38. 0038symm
  39. 0039apply add_assoc