BT00PR · Bertrand theorem

prime_strictly_above_decidable

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Being prime and strictly above a fixed lower endpoint is decidable.

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

∀ l. ∀ p. Prime(p) ∧ Lt(l,p) ∨ ¬(Prime(p) ∧ Lt(l,p))

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 PD0004 Prime

4 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall l p. ((((~(p = 1) /\ forall frm_prime_left_bpi_above_decidable_prime frm_prime_right_bpi_above_decidable_prime. p = frm_prime_left_bpi_above_decidable_prime * frm_prime_right_bpi_above_decidable_prime -> frm_prime_left_bpi_above_decidable_prime = 1 \/ frm_prime_right_bpi_above_decidable_prime = 1)) /\ (exists frm_gap_bpi_above_decidable_lower. frm_gap_bpi_above_decidable_lower + S l = p))) \/ ~((((~(p = 1) /\ forall frm_prime_left_bpi_above_decidable_prime frm_prime_right_bpi_above_decidable_prime. p = frm_prime_left_bpi_above_decidable_prime * frm_prime_right_bpi_above_decidable_prime -> frm_prime_left_bpi_above_decidable_prime = 1 \/ frm_prime_right_bpi_above_decidable_prime = 1)) /\ (exists frm_gap_bpi_above_decidable_lower. frm_gap_bpi_above_decidable_lower + S l = p)))

Proof neighborhood

Direct theorem prerequisites

BT003H prime_decidable BT001H lt_trichotomy BT0019 lt_to_le BT001I lt_not_le BT000E le_refl

Direct theorem dependents

BT00PS bounded_prime_interval_search

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

38 script commands · 20 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.

Named ingredients (5)
prime decidablelt trichotomylt to lelt not lele refl
01Fix variables and assumptionsL1–2

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

  1. L1
    intro l
  2. L2
    intro p
02Use earlier factsL3–3

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

  1. L3
    specialize prime_decidable p
03Separate the logical casesL4–4

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

  1. L4
    cases prime_decidable
04Use earlier factsL5–6

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

  1. L5
    specialize lt_trichotomy l
  2. L6
    specialize lt_trichotomy p
05Separate the logical casesL7–8

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

  1. L7
    cases lt_trichotomy
  2. L8
    right
06Fix variables and assumptionsL9–9

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

  1. L9
    intro habove
07Separate the logical casesL10–10

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

  1. L10
    cases habove
08Use earlier factsL11–13

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

  1. L11
    specialize lt_not_le p
  2. L12
    specialize lt_not_le p
  3. L13
    apply lt_not_le
09Calculate and transport equalitiesL14–14

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

  1. L14
    rewrite lt_trichotomy_left at habove_right
10Use earlier factsL15–17

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

  1. L15
    exact habove_right
  2. L16
    specialize le_refl p
  3. L17
    exact le_refl
11Separate the logical casesL18–20

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

  1. L18
    cases lt_trichotomy_right
  2. L19
    left
  3. L20
    split
12Use earlier factsL21–22

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

  1. L21
    exact prime_decidable_left
  2. L22
    exact lt_trichotomy_right_left
13Separate the logical casesL23–23

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

  1. L23
    right
14Fix variables and assumptionsL24–24

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

  1. L24
    intro habove
15Separate the logical casesL25–25

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

  1. L25
    cases habove
16Use earlier factsL26–33

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

  1. L26
    specialize lt_not_le p
  2. L27
    specialize lt_not_le l
  3. L28
    apply lt_not_le
  4. L29
    exact lt_trichotomy_right_right
  5. L30
    specialize lt_to_le l
  6. L31
    specialize lt_to_le p
  7. L32
    apply lt_to_le
  8. L33
    exact habove_right
17Separate the logical casesL34–34

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

  1. L34
    right
18Fix variables and assumptionsL35–35

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

  1. L35
    intro habove
19Separate the logical casesL36–36

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

  1. L36
    cases habove
20Use earlier factsL37–38

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

  1. L37
    apply prime_decidable_right
  2. L38
    exact habove_left

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro l
  2. 0002intro p
  3. 0003specialize prime_decidable p
  4. 0004cases prime_decidable
  5. 0005specialize lt_trichotomy l
  6. 0006specialize lt_trichotomy p
  7. 0007cases lt_trichotomy
  8. 0008right
  9. 0009intro habove
  10. 0010cases habove
  11. 0011specialize lt_not_le p
  12. 0012specialize lt_not_le p
  13. 0013apply lt_not_le
  14. 0014rewrite lt_trichotomy_left at habove_right
  15. 0015exact habove_right
  16. 0016specialize le_refl p
  17. 0017exact le_refl
  18. 0018cases lt_trichotomy_right
  19. 0019left
  20. 0020split
  21. 0021exact prime_decidable_left
  22. 0022exact lt_trichotomy_right_left
  23. 0023right
  24. 0024intro habove
  25. 0025cases habove
  26. 0026specialize lt_not_le p
  27. 0027specialize lt_not_le l
  28. 0028apply lt_not_le
  29. 0029exact lt_trichotomy_right_right
  30. 0030specialize lt_to_le l
  31. 0031specialize lt_to_le p
  32. 0032apply lt_to_le
  33. 0033exact habove_right
  34. 0034right
  35. 0035intro habove
  36. 0036cases habove
  37. 0037apply prime_decidable_right
  38. 0038exact habove_left