BT011E · Bertrand theorem

double_scaled_remainder_lift

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

Compose the two bounded scaling steps used by the 521 certificate.

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 s r u v. x = d * q + t -> 11 * t = d * s + r -> 2 * r + 37 = d * u + v -> 2 * (11 * x) + 37 = d * (2 * (11 * q + s) + u) + v

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 s r u v. x = d * q + t -> 11 * t = d * s + r -> 2 * r + 37 = d * u + v -> 2 * (11 * x) + 37 = d * (2 * (11 * q + s) + u) + v

Proof neighborhood

Direct theorem prerequisites

BT011C scaled_remainder_lift

Direct theorem dependents

BT011N prime_five_hundred_twenty_one

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

38 script commands · 7 reading checkpoints · 1 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 (1)
scaled remainder lift
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 s
  6. L6
    intro r
  7. L7
    intro u
  8. L8
    intro v
  9. L9
    intro hx
  10. L10
    intro hfirst_tail
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsecond_tail
03Establish hfirstL12–21

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

  1. L12
    have hfirst : 11 * x = d * (11 * q + s) + r
  2. L13
    trans 11 * x + 0
  3. L14
    symm
  4. L15
    apply PA3
  5. L16
    specialize scaled_remainder_lift d
  6. L17
    specialize scaled_remainder_lift x
  7. L18
    specialize scaled_remainder_lift q
  8. L19
    specialize scaled_remainder_lift t
  9. L20
    specialize scaled_remainder_lift 11
  10. L21
    specialize scaled_remainder_lift 0
04Use earlier factsL22–25

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

  1. L22
    specialize scaled_remainder_lift s
  2. L23
    specialize scaled_remainder_lift r
  3. L24
    apply scaled_remainder_lift
  4. L25
    exact hx
05Calculate and transport equalitiesL26–26

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

  1. L26
    rewrite PA3
06Use earlier factsL27–36

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

  1. L27
    exact hfirst_tail
  2. L28
    specialize scaled_remainder_lift d
  3. L29
    specialize scaled_remainder_lift (11 * x)
  4. L30
    specialize scaled_remainder_lift (11 * q + s)
  5. L31
    specialize scaled_remainder_lift r
  6. L32
    specialize scaled_remainder_lift 2
  7. L33
    specialize scaled_remainder_lift 37
  8. L34
    specialize scaled_remainder_lift u
  9. L35
    specialize scaled_remainder_lift v
  10. L36
    apply scaled_remainder_lift
07Use earlier factsL37–38

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

  1. L37
    exact hfirst
  2. L38
    exact hsecond_tail

Library-wide reading audit

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