BT0120 · Bertrand theorem

bertrand_cover_eighty_three_one_hundred_sixty_three

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

The compact checked cover from 83 to 163.

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

Le(13 · 12 + 7,9 · 9 + 2 + (9 · 9 + 2))

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

PD0001 Le

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
exists bpr_le_gap_bb8c_eighty_three_one_sixty_three. bpr_le_gap_bb8c_eighty_three_one_sixty_three + (13 * 12 + 7) = (9 * 9 + 2 + (9 * 9 + 2))

Proof neighborhood

Direct theorem prerequisites

BT000B add_mul BT0003 add_assoc BT0002 add_comm

Direct theorem dependents

BT0124 bertrand_small_closed_upper

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

40 script commands · 16 reading checkpoints · 6 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 (3)
add muladd assocadd comm
01Establish h13L1–2

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

  1. L1
    have h13 : 13 = 9 + 4
  2. L2
    norm_num
02Establish h9twelveL3–4

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

  1. L3
    have h9twelve : 9 * 12 = 9 * 9 + 27
  2. L4
    norm_num
03Establish h4twelveL5–6

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

  1. L5
    have h4twelve : 4 * 12 = 48
  2. L6
    norm_num
04Establish hcarrierL7–16

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

  1. L7
    have hcarrier : 13 * 12 + 7 = (9 * 9 + 2) + (8 * 10)
  2. L8
    rewrite h13
  3. L9
    specialize add_mul 9
  4. L10
    specialize add_mul 4
  5. L11
    specialize add_mul 12
  6. L12
    rewrite add_mul
  7. L13
    rewrite h9twelve
  8. L14
    rewrite h4twelve
  9. L15
    trans (9 * 9 + (27 + 48)) + 7
  10. L16
    congr
05Use earlier factsL17–17

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

  1. L17
    apply add_assoc
06Calculate and transport equalitiesL18–19

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

  1. L18
    refl
  2. L19
    trans 9 * 9 + ((27 + 48) + 7)
07Use earlier factsL20–20

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

  1. L20
    apply add_assoc
08Establish htailL21–25

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

  1. L21
    have htail : (27 + 48) + 7 = 2 + (8 * 10)
  2. L22
    norm_num
  3. L23
    rewrite htail
  4. L24
    symm
  5. L25
    apply add_assoc
09Construct an explicit witnessL26–26

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

  1. L26
    exists 3
10Calculate and transport equalitiesL27–29

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

  1. L27
    rewrite hcarrier
  2. L28
    trans (3 + (9 * 9 + 2)) + (8 * 10)
  3. L29
    symm
11Use earlier factsL30–30

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

  1. L30
    apply add_assoc
12Calculate and transport equalitiesL31–32

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

  1. L31
    trans ((9 * 9 + 2) + 3) + (8 * 10)
  2. L32
    congr
13Use earlier factsL33–33

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

  1. L33
    apply add_comm
14Calculate and transport equalitiesL34–35

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

  1. L34
    refl
  2. L35
    trans (9 * 9 + 2) + (3 + (8 * 10))
15Use earlier factsL36–36

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

  1. L36
    apply add_assoc
16Establish hgapL37–40

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

  1. L37
    have hgap : 3 + (8 * 10) = 9 * 9 + 2
  2. L38
    norm_num
  3. L39
    rewrite hgap
  4. L40
    refl

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001have h13 : 13 = 9 + 4
  2. 0002norm_num
  3. 0003have h9twelve : 9 * 12 = 9 * 9 + 27
  4. 0004norm_num
  5. 0005have h4twelve : 4 * 12 = 48
  6. 0006norm_num
  7. 0007have hcarrier : 13 * 12 + 7 = (9 * 9 + 2) + (8 * 10)
  8. 0008rewrite h13
  9. 0009specialize add_mul 9
  10. 0010specialize add_mul 4
  11. 0011specialize add_mul 12
  12. 0012rewrite add_mul
  13. 0013rewrite h9twelve
  14. 0014rewrite h4twelve
  15. 0015trans (9 * 9 + (27 + 48)) + 7
  16. 0016congr
  17. 0017apply add_assoc
  18. 0018refl
  19. 0019trans 9 * 9 + ((27 + 48) + 7)
  20. 0020apply add_assoc
  21. 0021have htail : (27 + 48) + 7 = 2 + (8 * 10)
  22. 0022norm_num
  23. 0023rewrite htail
  24. 0024symm
  25. 0025apply add_assoc
  26. 0026exists 3
  27. 0027rewrite hcarrier
  28. 0028trans (3 + (9 * 9 + 2)) + (8 * 10)
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031trans ((9 * 9 + 2) + 3) + (8 * 10)
  32. 0032congr
  33. 0033apply add_comm
  34. 0034refl
  35. 0035trans (9 * 9 + 2) + (3 + (8 * 10))
  36. 0036apply add_assoc
  37. 0037have hgap : 3 + (8 * 10) = 9 * 9 + 2
  38. 0038norm_num
  39. 0039rewrite hgap
  40. 0040refl