BT0121 · Bertrand theorem

bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen

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

The compact checked cover from 163 to 317.

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(18 · 17 + 11,13 · 12 + 7 + (13 · 12 + 7))

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_one_sixty_three_three_seventeen. bpr_le_gap_bb8c_one_sixty_three_three_seventeen + (18 * 17 + 11) = (13 * 12 + 7 + (13 * 12 + 7))

Proof neighborhood

Direct theorem prerequisites

BT000B add_mul BT0007 mul_add BT0003 add_assoc BT0002 add_comm BT011O bertrand_add_swap_nested BT011P bertrand_add_six_permute

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

67 script commands · 25 reading checkpoints · 11 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 (6)
add mulmul addadd assocadd commbertrand add swap nestedbertrand add six permute
01Establish h18L1–2

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

  1. L1
    have h18 : 18 = 13 + 5
  2. L2
    norm_num
02Establish h17L3–4

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

  1. L3
    have h17 : 17 = 12 + 5
  2. L4
    norm_num
03Establish h11L5–6

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

  1. L5
    have h11 : 11 = 7 + 4
  2. L6
    norm_num
04Establish hcarrierL7–9

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

  1. L7
    have hcarrier : 18 * 17 + 11 = (13 * 12 + 7) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  2. L8
    rewrite h18
  3. L9
    rewrite h17
05Establish houterL10–12

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

  1. L10
    have houter : (13 + 5) * (12 + 5) = 13 * (12 + 5) + 5 * (12 + 5)
  2. L11
    apply add_mul
  3. L12
    rewrite houter
06Establish hleft_distL13–15

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

  1. L13
    have hleft_dist : 13 * (12 + 5) = 13 * 12 + 13 * 5
  2. L14
    apply mul_add
  3. L15
    rewrite hleft_dist
07Establish hright_distL16–23

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

  1. L16
    have hright_dist : 5 * (12 + 5) = 5 * 12 + 5 * 5
  2. L17
    apply mul_add
  3. L18
    rewrite hright_dist
  4. L19
    trans ((13 * 12 + 13 * 5) + (5 * 12 + 5 * 5)) + (7 + 4)
  5. L20
    congr
  6. L21
    refl
  7. L22
    exact h11
  8. L23
    apply bertrand_add_six_permute
08Establish hgapL24–24

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

  1. L24
    have hgap : 9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)) = 13 * 12 + 7
09Establish h13L25–26

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

  1. L25
    have h13 : 13 = 5 + 8
  2. L26
    norm_num
10Establish hAexpandL27–36

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

  1. L27
    have hAexpand : 13 * 12 + 7 = (5 * 12 + 8 * 12) + 7
  2. L28
    trans (5 + 8) * 12 + 7
  3. L29
    congr
  4. L30
    congr
  5. L31
    exact h13
  6. L32
    refl
  7. L33
    refl
  8. L34
    trans (5 * 12 + 8 * 12) + 7
  9. L35
    congr
  10. L36
    apply add_mul
11Calculate and transport equalitiesL37–42

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

  1. L37
    refl
  2. L38
    refl
  3. L39
    rewrite hAexpand
  4. L40
    trans 9 + (13 * 5 + (5 * 12 + (5 * 5 + 4)))
  5. L41
    congr
  6. L42
    refl
12Use earlier factsL43–43

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

  1. L43
    apply add_assoc
13Calculate and transport equalitiesL44–46

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

  1. L44
    trans 9 + (5 * 12 + (13 * 5 + (5 * 5 + 4)))
  2. L45
    congr
  3. L46
    refl
14Use earlier factsL47–47

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

  1. L47
    apply bertrand_add_swap_nested
15Calculate and transport equalitiesL48–48

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

  1. L48
    trans 5 * 12 + (9 + (13 * 5 + (5 * 5 + 4)))
16Use earlier factsL49–49

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

  1. L49
    apply bertrand_add_swap_nested
17Establish htailL50–54

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

  1. L50
    have htail : 9 + (13 * 5 + (5 * 5 + 4)) = 8 * 12 + 7
  2. L51
    norm_num
  3. L52
    rewrite htail
  4. L53
    symm
  5. L54
    apply add_assoc
18Construct an explicit witnessL55–55

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

  1. L55
    exists 9
19Calculate and transport equalitiesL56–58

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

  1. L56
    rewrite hcarrier
  2. L57
    trans (9 + (13 * 12 + 7)) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  3. L58
    symm
20Use earlier factsL59–59

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

  1. L59
    apply add_assoc
21Calculate and transport equalitiesL60–61

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

  1. L60
    trans ((13 * 12 + 7) + 9) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  2. L61
    congr
22Use earlier factsL62–62

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

  1. L62
    apply add_comm
23Calculate and transport equalitiesL63–64

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

  1. L63
    refl
  2. L64
    trans (13 * 12 + 7) + (9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)))
24Use earlier factsL65–65

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

  1. L65
    apply add_assoc
25Calculate and transport equalitiesL66–67

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

  1. L66
    rewrite hgap
  2. L67
    refl

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001have h18 : 18 = 13 + 5
  2. 0002norm_num
  3. 0003have h17 : 17 = 12 + 5
  4. 0004norm_num
  5. 0005have h11 : 11 = 7 + 4
  6. 0006norm_num
  7. 0007have hcarrier : 18 * 17 + 11 = (13 * 12 + 7) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  8. 0008rewrite h18
  9. 0009rewrite h17
  10. 0010have houter : (13 + 5) * (12 + 5) = 13 * (12 + 5) + 5 * (12 + 5)
  11. 0011apply add_mul
  12. 0012rewrite houter
  13. 0013have hleft_dist : 13 * (12 + 5) = 13 * 12 + 13 * 5
  14. 0014apply mul_add
  15. 0015rewrite hleft_dist
  16. 0016have hright_dist : 5 * (12 + 5) = 5 * 12 + 5 * 5
  17. 0017apply mul_add
  18. 0018rewrite hright_dist
  19. 0019trans ((13 * 12 + 13 * 5) + (5 * 12 + 5 * 5)) + (7 + 4)
  20. 0020congr
  21. 0021refl
  22. 0022exact h11
  23. 0023apply bertrand_add_six_permute
  24. 0024have hgap : 9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)) = 13 * 12 + 7
  25. 0025have h13 : 13 = 5 + 8
  26. 0026norm_num
  27. 0027have hAexpand : 13 * 12 + 7 = (5 * 12 + 8 * 12) + 7
  28. 0028trans (5 + 8) * 12 + 7
  29. 0029congr
  30. 0030congr
  31. 0031exact h13
  32. 0032refl
  33. 0033refl
  34. 0034trans (5 * 12 + 8 * 12) + 7
  35. 0035congr
  36. 0036apply add_mul
  37. 0037refl
  38. 0038refl
  39. 0039rewrite hAexpand
  40. 0040trans 9 + (13 * 5 + (5 * 12 + (5 * 5 + 4)))
  41. 0041congr
  42. 0042refl
  43. 0043apply add_assoc
  44. 0044trans 9 + (5 * 12 + (13 * 5 + (5 * 5 + 4)))
  45. 0045congr
  46. 0046refl
  47. 0047apply bertrand_add_swap_nested
  48. 0048trans 5 * 12 + (9 + (13 * 5 + (5 * 5 + 4)))
  49. 0049apply bertrand_add_swap_nested
  50. 0050have htail : 9 + (13 * 5 + (5 * 5 + 4)) = 8 * 12 + 7
  51. 0051norm_num
  52. 0052rewrite htail
  53. 0053symm
  54. 0054apply add_assoc
  55. 0055exists 9
  56. 0056rewrite hcarrier
  57. 0057trans (9 + (13 * 12 + 7)) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  58. 0058symm
  59. 0059apply add_assoc
  60. 0060trans ((13 * 12 + 7) + 9) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  61. 0061congr
  62. 0062apply add_comm
  63. 0063refl
  64. 0064trans (13 * 12 + 7) + (9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)))
  65. 0065apply add_assoc
  66. 0066rewrite hgap
  67. 0067refl