BT00AA · Bertrand theorem

finite_lt_succ_eq_or_lt

Stable checked-use theorem · independently kernel verified

A value below a successor is the predecessor or lies below it.

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

∀ n. ∀ x. Lt(x,S n) → x = n ∨ Lt(x,n)

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

2 occurrences

In local proof propositions

PD0001 Le

1 occurrences

Exact expanded native-PA statement
forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n

Proof neighborhood

Direct theorem prerequisites

BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct theorem dependents

BT00S0 prime_power_quotient_prefix_exists BT00SE eisenstein_initial_segment_prefix_extend BT00T2 beta_pascal_zero_row_extend BT00T4 beta_pascal_row_step_extend BT00T6 beta_pascal_table_prefix_extend BT00U7 primorial_factor_prefix_extend BT00UR primorial_interval_factor_prefix_extend BT00XW double_quotient_carry_prefix_extend BT00YP prime_contribution_prefix_extend BT010K prime_contribution_interval_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

12 script commands · 2 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 (2)
le of succ le succle eq or lt
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro x
  3. L3
    intro hlt
02Establish hleL4–12

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

  1. L4
  2. L5
    specialize le_of_succ_le_succ x
  3. L6
    specialize le_of_succ_le_succ n
  4. L7
    apply le_of_succ_le_succ
  5. L8
    exact hlt
  6. L9
    specialize le_eq_or_lt x
  7. L10
    specialize le_eq_or_lt n
  8. L11
    apply le_eq_or_lt
  9. L12
    exact hle

Library-wide reading audit

Original defined command ledger · 12 lines
  1. 0001intro n
  2. 0002intro x
  3. 0003intro hlt
  4. 0004have hle : Le(x,n)
    Exact native replay linehave hle : exists h. h + x = n
  5. 0005specialize le_of_succ_le_succ x
  6. 0006specialize le_of_succ_le_succ n
  7. 0007apply le_of_succ_le_succ
  8. 0008exact hlt
  9. 0009specialize le_eq_or_lt x
  10. 0010specialize le_eq_or_lt n
  11. 0011apply le_eq_or_lt
  12. 0012exact hle