BT0085 · Bertrand theorem

beta_range_succ_extend

Stable checked-use theorem · independently kernel verified

Recode a consecutive prefix and append its next value.

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

∀ b. ∀ c. ∀ a. ∀ l. ∀ sl. sl = S l → Range(b,c,a,l) → ∃ x. ∃ y. Range(x,y,a,sl)

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

PD0018 Range

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

2 occurrences

Exact expanded native-PA statement
forall b c a l sl. sl = S l -> (forall ff_i_before. (exists ff_lt_before_bound. ff_lt_before_bound + S ff_i_before = l) -> (((exists ff_h_before_decoded. ff_h_before_decoded + S (a + ff_i_before) = S ((S (ff_i_before)) * c)) /\ exists ff_q_before_decoded. b = ff_q_before_decoded * S ((S (ff_i_before)) * c) + (a + ff_i_before)))) -> exists z d. (forall ff_i_after. (exists ff_lt_after_bound. ff_lt_after_bound + S ff_i_after = sl) -> (((exists ff_h_after_decoded. ff_h_after_decoded + S (a + ff_i_after) = S ((S (ff_i_after)) * d)) /\ exists ff_q_after_decoded. z = ff_q_after_decoded * S ((S (ff_i_after)) * d) + (a + ff_i_after))))

Proof neighborhood

Direct theorem prerequisites

BT005D beta_prefix_extend BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct theorem dependents

BT0086 beta_range_exists

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

42 script commands · 11 reading checkpoints · 2 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)
beta prefix extendle of succ le succle eq or lt
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro l
  5. L5
    intro sl
  6. L6
    intro hsl
  7. L7
    intro hrange
02Use earlier factsL8–11

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

  1. L8
    specialize beta_prefix_extend l
  2. L9
    specialize beta_prefix_extend b
  3. L10
    specialize beta_prefix_extend c
  4. L11
    specialize beta_prefix_extend (a + l)
03Separate the logical casesL12–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases beta_prefix_extend
  2. L13
    cases beta_prefix_extend_witness
  3. L14
    cases beta_prefix_extend_witness_witness
04Construct an explicit witnessL15–16

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

  1. L15
    exists x
  2. L16
    exists x1
05Fix variables and assumptionsL17–18

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

  1. L17
    intro i
  2. L18
    intro hi
06Calculate and transport equalitiesL19–19

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

  1. L19
    rewrite hsl at hi
07Establish hilL20–24

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

  1. L20
  2. L21
    specialize le_of_succ_le_succ i
  3. L22
    specialize le_of_succ_le_succ l
  4. L23
    apply le_of_succ_le_succ
  5. L24
    exact hi
08Establish hsplitL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L25
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L26
    specialize le_eq_or_lt i
  3. L27
    specialize le_eq_or_lt l
  4. L28
    apply le_eq_or_lt
  5. L29
    exact hil
09Separate the logical casesL30–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hsplit
10Calculate and transport equalitiesL31–34

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

  1. L31
    rewrite hsplit_left
  2. L32
    rewrite hsplit_left
  3. L33
    rewrite hsplit_left
  4. L34
    rewrite hsplit_left
11Use earlier factsL35–42

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

  1. L35
    exact beta_prefix_extend_witness_witness_left
  2. L36
    specialize beta_prefix_extend_witness_witness_right i
  3. L37
    specialize beta_prefix_extend_witness_witness_right (a + i)
  4. L38
    apply beta_prefix_extend_witness_witness_right
  5. L39
    exact hsplit_right
  6. L40
    specialize hrange i
  7. L41
    apply hrange
  8. L42
    exact hsplit_right

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro sl
  6. 0006intro hsl
  7. 0007intro hrange
  8. 0008specialize beta_prefix_extend l
  9. 0009specialize beta_prefix_extend b
  10. 0010specialize beta_prefix_extend c
  11. 0011specialize beta_prefix_extend (a + l)
  12. 0012cases beta_prefix_extend
  13. 0013cases beta_prefix_extend_witness
  14. 0014cases beta_prefix_extend_witness_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017intro i
  18. 0018intro hi
  19. 0019rewrite hsl at hi
  20. 0020have hil : Le(i,l)
    Exact native replay linehave hil : exists h. h + i = l
  21. 0021specialize le_of_succ_le_succ i
  22. 0022specialize le_of_succ_le_succ l
  23. 0023apply le_of_succ_le_succ
  24. 0024exact hi
  25. 0025have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  26. 0026specialize le_eq_or_lt i
  27. 0027specialize le_eq_or_lt l
  28. 0028apply le_eq_or_lt
  29. 0029exact hil
  30. 0030cases hsplit
  31. 0031rewrite hsplit_left
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034rewrite hsplit_left
  35. 0035exact beta_prefix_extend_witness_witness_left
  36. 0036specialize beta_prefix_extend_witness_witness_right i
  37. 0037specialize beta_prefix_extend_witness_witness_right (a + i)
  38. 0038apply beta_prefix_extend_witness_witness_right
  39. 0039exact hsplit_right
  40. 0040specialize hrange i
  41. 0041apply hrange
  42. 0042exact hsplit_right