BT001H · Bertrand theorem

lt_trichotomy

Stable checked-use theorem · independently kernel verified

Two naturals are equal or strictly ordered in exactly one displayed direction.

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

∀ a. ∀ b. a = b ∨ (Lt(a,b) ∨ Lt(b,a))

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

none

0 occurrences

Exact expanded native-PA statement
forall a b. a = b \/ ((exists k. k + S a = b) \/ exists k. k + S b = a)

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT004P beta_moduli_pairwise_coprime_bounded BT00PR prime_strictly_above_decidable BT00R2 ceil_div_six_functional BT00TJ choose_succ_succ

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

39 script commands · 28 reading checkpoints · 0 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.

01Induction on aL1–1

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

  1. L1
    induction a
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
03Separate the logical casesL3–3

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

  1. L3
    left
04Calculate and transport equalitiesL4–4

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

  1. L4
    refl
05Separate the logical casesL5–6

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

  1. L5
    right
  2. L6
    left
06Construct an explicit witnessL7–7

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

  1. L7
    exists b
07Calculate and transport equalitiesL8–8

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

  1. L8
    trans S (b + 0)
08Use earlier factsL9–9

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

  1. L9
    apply PA4
09Calculate and transport equalitiesL10–10

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

  1. L10
    congr
10Use earlier factsL11–11

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

  1. L11
    apply PA3
11Induction on bL12–12

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

  1. L12
    induction b
12Separate the logical casesL13–14

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

  1. L13
    right
  2. L14
    right
13Construct an explicit witnessL15–15

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

  1. L15
    exists a
14Calculate and transport equalitiesL16–16

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

  1. L16
    trans S (a + 0)
15Use earlier factsL17–17

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

  1. L17
    apply PA4
16Calculate and transport equalitiesL18–18

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

  1. L18
    congr
17Use earlier factsL19–20

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

  1. L19
    apply PA3
  2. L20
    specialize IH b
18Separate the logical casesL21–22

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

  1. L21
    cases IH
  2. L22
    left
19Calculate and transport equalitiesL23–23

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

  1. L23
    congr
20Use earlier factsL24–24

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

  1. L24
    exact IH_left
21Separate the logical casesL25–28

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

  1. L25
    cases IH_right
  2. L26
    right
  3. L27
    left
  4. L28
    cases IH_right_left
22Construct an explicit witnessL29–29

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

  1. L29
    exists x
23Calculate and transport equalitiesL30–31

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

  1. L30
    rewrite PA4
  2. L31
    congr
24Use earlier factsL32–32

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

  1. L32
    exact IH_right_left_witness
25Separate the logical casesL33–35

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

  1. L33
    right
  2. L34
    right
  3. L35
    cases IH_right_right
26Construct an explicit witnessL36–36

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

  1. L36
    exists x
27Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite PA4
  2. L38
    congr
28Use earlier factsL39–39

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

  1. L39
    exact IH_right_right_witness

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001induction a
  2. 0002induction b
  3. 0003left
  4. 0004refl
  5. 0005right
  6. 0006left
  7. 0007exists b
  8. 0008trans S (b + 0)
  9. 0009apply PA4
  10. 0010congr
  11. 0011apply PA3
  12. 0012induction b
  13. 0013right
  14. 0014right
  15. 0015exists a
  16. 0016trans S (a + 0)
  17. 0017apply PA4
  18. 0018congr
  19. 0019apply PA3
  20. 0020specialize IH b
  21. 0021cases IH
  22. 0022left
  23. 0023congr
  24. 0024exact IH_left
  25. 0025cases IH_right
  26. 0026right
  27. 0027left
  28. 0028cases IH_right_left
  29. 0029exists x
  30. 0030rewrite PA4
  31. 0031congr
  32. 0032exact IH_right_left_witness
  33. 0033right
  34. 0034right
  35. 0035cases IH_right_right
  36. 0036exists x
  37. 0037rewrite PA4
  38. 0038congr
  39. 0039exact IH_right_right_witness