BT001K · Bertrand theorem

lt_not_eq_add_middle

Stable checked-use theorem · independently kernel verified

A strict upper bound prevents the lower term from containing that bound as an additive middle block.

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

∀ r. ∀ m. ∀ a. ∀ b. Lt(r,m) → ¬r = a + m + b

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

PD0002 Lt

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall r m a b. (exists k. k + S r = m) -> ~(r = (a + m) + b)

Proof neighborhood

Direct theorem prerequisites

BT0001 add_succ_left

Direct theorem dependents

BT001S positive_quotient_gap_impossible

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

44 script commands · 16 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)
add succ left
01Establish hbadL1–2

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

  1. L1
    have hbad : forall z a w b. ~(z = (a + (w + S z)) + b)
  2. L2
    intro z
02Induction on zL3–12

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

  1. L3
    induction z
  2. L4
    intro a
  3. L5
    intro w
  4. L6
    intro b
  5. L7
    intro hz
  6. L8
    apply PA1
  7. L9
    symm
  8. L10
    rewrite PA4 at hz
  9. L11
    rewrite PA4 at hz
  10. L12
    specialize add_succ_left (a + (w + 0))
03Use earlier factsL13–13

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

  1. L13
    specialize add_succ_left b
04Calculate and transport equalitiesL14–14

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

  1. L14
    rewrite add_succ_left at hz
05Use earlier factsL15–15

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

  1. L15
    exact hz
06Fix variables and assumptionsL16–19

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

  1. L16
    intro a
  2. L17
    intro w
  3. L18
    intro b
  4. L19
    intro hz
07Use earlier factsL20–24

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

  1. L20
    specialize IH a
  2. L21
    specialize IH w
  3. L22
    specialize IH b
  4. L23
    apply IH
  5. L24
    apply PA2
08Calculate and transport equalitiesL25–26

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

  1. L25
    rewrite PA4 at hz
  2. L26
    rewrite PA4 at hz
09Use earlier factsL27–28

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

  1. L27
    specialize add_succ_left (a + (w + S z))
  2. L28
    specialize add_succ_left b
10Calculate and transport equalitiesL29–29

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

  1. L29
    rewrite add_succ_left at hz
11Use earlier factsL30–30

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

  1. L30
    exact hz
12Fix variables and assumptionsL31–36

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

  1. L31
    intro r
  2. L32
    intro m
  3. L33
    intro a
  4. L34
    intro b
  5. L35
    intro hr
  6. L36
    intro heq
13Separate the logical casesL37–37

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

  1. L37
    cases hr
14Use earlier factsL38–42

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

  1. L38
    specialize hbad r
  2. L39
    specialize hbad a
  3. L40
    specialize hbad x
  4. L41
    specialize hbad b
  5. L42
    apply hbad
15Calculate and transport equalitiesL43–43

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

  1. L43
    rewrite <- hr_witness at heq
16Use earlier factsL44–44

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

  1. L44
    exact heq

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001have hbad : forall z a w b. ~(z = (a + (w + S z)) + b)
  2. 0002intro z
  3. 0003induction z
  4. 0004intro a
  5. 0005intro w
  6. 0006intro b
  7. 0007intro hz
  8. 0008apply PA1
  9. 0009symm
  10. 0010rewrite PA4 at hz
  11. 0011rewrite PA4 at hz
  12. 0012specialize add_succ_left (a + (w + 0))
  13. 0013specialize add_succ_left b
  14. 0014rewrite add_succ_left at hz
  15. 0015exact hz
  16. 0016intro a
  17. 0017intro w
  18. 0018intro b
  19. 0019intro hz
  20. 0020specialize IH a
  21. 0021specialize IH w
  22. 0022specialize IH b
  23. 0023apply IH
  24. 0024apply PA2
  25. 0025rewrite PA4 at hz
  26. 0026rewrite PA4 at hz
  27. 0027specialize add_succ_left (a + (w + S z))
  28. 0028specialize add_succ_left b
  29. 0029rewrite add_succ_left at hz
  30. 0030exact hz
  31. 0031intro r
  32. 0032intro m
  33. 0033intro a
  34. 0034intro b
  35. 0035intro hr
  36. 0036intro heq
  37. 0037cases hr
  38. 0038specialize hbad r
  39. 0039specialize hbad a
  40. 0040specialize hbad x
  41. 0041specialize hbad b
  42. 0042apply hbad
  43. 0043rewrite <- hr_witness at heq
  44. 0044exact heq