BT0119 · Bertrand theorem

prime_of_no_small_prime_divisor_below_square

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

Trial division by primes through B certifies numbers below (B+1)^2.

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. ∀ n. ¬n = 0 → ¬n = 1 → Lt(n,S B · S B) → (∀ x. Prime(x) → Le(x,B) → ¬Dvd(x,n)) → Prime(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

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime

5 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0004 Prime

3 occurrences

Exact expanded native-PA statement
forall B n. ~(n = 0) -> ~(n = 1) -> (exists bpr_gap_bb8pnsp_square. bpr_gap_bb8pnsp_square + S (n) = S B * S B) -> (forall p. ((~(p = 1) /\ forall bpr_left_bb8pnsp_prime bpr_right_bb8pnsp_prime. p = bpr_left_bb8pnsp_prime * bpr_right_bb8pnsp_prime -> bpr_left_bb8pnsp_prime = 1 \/ bpr_right_bb8pnsp_prime = 1)) -> (exists bpr_le_gap_bb8pnsp_bound. bpr_le_gap_bb8pnsp_bound + (p) = (B)) -> ~(exists bpr_quotient_bb8pnsp_divides. n = (p) * bpr_quotient_bb8pnsp_divides)) -> ((~(n = 1) /\ forall bpr_left_bb8pnsp_result bpr_right_bb8pnsp_result. n = bpr_left_bb8pnsp_result * bpr_right_bb8pnsp_result -> bpr_left_bb8pnsp_result = 1 \/ bpr_right_bb8pnsp_result = 1))

Proof neighborhood

Direct theorem prerequisites

BT003H prime_decidable BT0118 nonprime_has_small_prime_divisor_below_square

Direct theorem dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

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

26 script commands · 8 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)
prime decidablenonprime has small prime divisor below square
01Fix variables and assumptionsL1–6

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

  1. L1
    intro B
  2. L2
    intro n
  3. L3
    intro hn0
  4. L4
    intro hn1
  5. L5
    intro hsquare
  6. L6
    intro hexclude
02Use earlier factsL7–7

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

  1. L7
    specialize prime_decidable n
03Separate the logical casesL8–8

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

  1. L8
    cases prime_decidable
04Use earlier factsL9–9

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

  1. L9
    exact prime_decidable_left
05Separate the logical casesL10–10

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

  1. L10
    exfalso
06Establish hpL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonprime has small prime divisor below square.

  1. L11
    have hp : ∃ p. Prime(p) ∧ (Le(p,B) ∧ Dvd(p,n))Definitions: Prime(p)Le(p,B)Dvd(p,n)Original native command in the exact edition
  2. L12
    specialize nonprime_has_small_prime_divisor_below_square B
  3. L13
    specialize nonprime_has_small_prime_divisor_below_square n
  4. L14
    apply nonprime_has_small_prime_divisor_below_square
  5. L15
    exact hn0
  6. L16
    exact hn1
  7. L17
    exact hsquare
  8. L18
    exact prime_decidable_right
07Separate the logical casesL19–21

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

  1. L19
    cases hp
  2. L20
    cases hp_witness
  3. L21
    cases hp_witness_right
08Use earlier factsL22–26

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

  1. L22
    specialize hexclude x
  2. L23
    apply hexclude
  3. L24
    exact hp_witness_left
  4. L25
    exact hp_witness_right_left
  5. L26
    exact hp_witness_right_right

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro B
  2. 0002intro n
  3. 0003intro hn0
  4. 0004intro hn1
  5. 0005intro hsquare
  6. 0006intro hexclude
  7. 0007specialize prime_decidable n
  8. 0008cases prime_decidable
  9. 0009exact prime_decidable_left
  10. 0010exfalso
  11. 0011have hp : ∃ p. Prime(p) ∧ (Le(p,B) ∧ Dvd(p,n))
    Exact native replay linehave hp : exists p. ((~(p = 1) /\ forall bpr_left_bb8npsp_prime bpr_right_bb8npsp_prime. p = bpr_left_bb8npsp_prime * bpr_right_bb8npsp_prime -> bpr_left_bb8npsp_prime = 1 \/ bpr_right_bb8npsp_prime = 1)) /\ ((exists bpr_le_gap_bb8npsp_bound. bpr_le_gap_bb8npsp_bound + (p) = (B)) /\ (exists bpr_quotient_bb8npsp_divides. n = (p) * bpr_quotient_bb8npsp_divides))
  12. 0012specialize nonprime_has_small_prime_divisor_below_square B
  13. 0013specialize nonprime_has_small_prime_divisor_below_square n
  14. 0014apply nonprime_has_small_prime_divisor_below_square
  15. 0015exact hn0
  16. 0016exact hn1
  17. 0017exact hsquare
  18. 0018exact prime_decidable_right
  19. 0019cases hp
  20. 0020cases hp_witness
  21. 0021cases hp_witness_right
  22. 0022specialize hexclude x
  23. 0023apply hexclude
  24. 0024exact hp_witness_left
  25. 0025exact hp_witness_right_left
  26. 0026exact hp_witness_right_right