BT004N · Bertrand theorem

bounded_common_multiple_exists

Stable checked-use theorem · independently kernel verified

Every finite initial interval has a nonzero common-multiple surrogate.

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. ¬c = 0 ∧ (∀ x. (∃ y. S x + S y = S B) → Dvd(S x,c))

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

PD0003 Dvd

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall B. exists c. (~(c = 0) /\ forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k)

Proof neighborhood

Direct theorem prerequisites

BT004M bounded_common_multiple_step BT000C succ_ne_zero BT001X add_eq_zero_left

Direct theorem dependents

BT005D beta_prefix_extend

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

29 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)
bounded common multiple stepsucc ne zeroadd eq zero left
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–2

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
03Construct an explicit witnessL3–3

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

  1. L3
    exists 1
04Separate the logical casesL4–4

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

  1. L4
    split
05Use earlier factsL5–6

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

  1. L5
    specialize succ_ne_zero 0
  2. L6
    exact succ_ne_zero
06Fix variables and assumptionsL7–8

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

  1. L7
    intro t
  2. L8
    intro ht
07Separate the logical casesL9–10

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

  1. L9
    cases ht
  2. L10
    exfalso
08Establish hzL11–14

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

  1. L11
    have hz : S t + x = 0
  2. L12
    rewrite PA4 at ht_witness
  3. L13
    apply PA2
  4. L14
    exact ht_witness
09Establish hst0L15–22

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

  1. L15
    have hst0 : S t = 0
  2. L16
    specialize add_eq_zero_left (S t)
  3. L17
    specialize add_eq_zero_left x
  4. L18
    apply add_eq_zero_left
  5. L19
    exact hz
  6. L20
    specialize succ_ne_zero t
  7. L21
    apply succ_ne_zero
  8. L22
    exact hst0
10Separate the logical casesL23–24

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

  1. L23
    cases IH
  2. L24
    cases IH_witness
11Use earlier factsL25–29

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

  1. L25
    specialize bounded_common_multiple_step B
  2. L26
    specialize bounded_common_multiple_step x
  3. L27
    apply bounded_common_multiple_step
  4. L28
    exact IH_witness_left
  5. L29
    exact IH_witness_right

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003exists 1
  4. 0004split
  5. 0005specialize succ_ne_zero 0
  6. 0006exact succ_ne_zero
  7. 0007intro t
  8. 0008intro ht
  9. 0009cases ht
  10. 0010exfalso
  11. 0011have hz : S t + x = 0
  12. 0012rewrite PA4 at ht_witness
  13. 0013apply PA2
  14. 0014exact ht_witness
  15. 0015have hst0 : S t = 0
  16. 0016specialize add_eq_zero_left (S t)
  17. 0017specialize add_eq_zero_left x
  18. 0018apply add_eq_zero_left
  19. 0019exact hz
  20. 0020specialize succ_ne_zero t
  21. 0021apply succ_ne_zero
  22. 0022exact hst0
  23. 0023cases IH
  24. 0024cases IH_witness
  25. 0025specialize bounded_common_multiple_step B
  26. 0026specialize bounded_common_multiple_step x
  27. 0027apply bounded_common_multiple_step
  28. 0028exact IH_witness_left
  29. 0029exact IH_witness_right