BT00U6 · Bertrand theorem

primorial_factor_choice_functional

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

The prime-or-one selector factor at a fixed index is unique.

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

∀ i. ∀ a. ∀ z. Prime(S i) ∧ a = S i ∨ ¬Prime(S i) ∧ a = 1 → Prime(S i) ∧ z = S i ∨ ¬Prime(S i) ∧ z = 1 → a = z

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

PD0004 Prime

4 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall i a z. (((((~(S (i) = 1) /\ forall bpr_left_bpfcf_left_prime bpr_right_bpfcf_left_prime. S (i) = bpr_left_bpfcf_left_prime * bpr_right_bpfcf_left_prime -> bpr_left_bpfcf_left_prime = 1 \/ bpr_right_bpfcf_left_prime = 1)) /\ a = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfcf_left_prime bpr_right_bpfcf_left_prime. S (i) = bpr_left_bpfcf_left_prime * bpr_right_bpfcf_left_prime -> bpr_left_bpfcf_left_prime = 1 \/ bpr_right_bpfcf_left_prime = 1)) /\ a = 1))) -> (((((~(S (i) = 1) /\ forall bpr_left_bpfcf_right_prime bpr_right_bpfcf_right_prime. S (i) = bpr_left_bpfcf_right_prime * bpr_right_bpfcf_right_prime -> bpr_left_bpfcf_right_prime = 1 \/ bpr_right_bpfcf_right_prime = 1)) /\ z = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfcf_right_prime bpr_right_bpfcf_right_prime. S (i) = bpr_left_bpfcf_right_prime * bpr_right_bpfcf_right_prime -> bpr_left_bpfcf_right_prime = 1 \/ bpr_right_bpfcf_right_prime = 1)) /\ z = 1))) -> a = z

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

BT00UW primorial_interval_factor_prefix_shift

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

28 script commands · 15 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro i
  2. L2
    intro a
  3. L3
    intro z
  4. L4
    intro hleft
  5. L5
    intro hright
02Separate the logical casesL6–9

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

  1. L6
    cases hleft
  2. L7
    cases hleft_left
  3. L8
    cases hright
  4. L9
    cases hright_left
03Calculate and transport equalitiesL10–10

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

  1. L10
    trans S i
04Use earlier factsL11–11

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

  1. L11
    exact hleft_left_right
05Calculate and transport equalitiesL12–12

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

  1. L12
    symm
06Use earlier factsL13–13

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

  1. L13
    exact hright_left_right
07Separate the logical casesL14–15

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

  1. L14
    cases hright_right
  2. L15
    exfalso
08Use earlier factsL16–17

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

  1. L16
    apply hright_right_left
  2. L17
    exact hleft_left_left
09Separate the logical casesL18–21

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

  1. L18
    cases hleft_right
  2. L19
    cases hright
  3. L20
    cases hright_left
  4. L21
    exfalso
10Use earlier factsL22–23

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

  1. L22
    apply hleft_right_left
  2. L23
    exact hright_left_left
11Separate the logical casesL24–24

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

  1. L24
    cases hright_right
12Calculate and transport equalitiesL25–25

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

  1. L25
    trans 1
13Use earlier factsL26–26

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

  1. L26
    exact hleft_right_right
14Calculate and transport equalitiesL27–27

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

  1. L27
    symm
15Use earlier factsL28–28

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

  1. L28
    exact hright_right_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro i
  2. 0002intro a
  3. 0003intro z
  4. 0004intro hleft
  5. 0005intro hright
  6. 0006cases hleft
  7. 0007cases hleft_left
  8. 0008cases hright
  9. 0009cases hright_left
  10. 0010trans S i
  11. 0011exact hleft_left_right
  12. 0012symm
  13. 0013exact hright_left_right
  14. 0014cases hright_right
  15. 0015exfalso
  16. 0016apply hright_right_left
  17. 0017exact hleft_left_left
  18. 0018cases hleft_right
  19. 0019cases hright
  20. 0020cases hright_left
  21. 0021exfalso
  22. 0022apply hleft_right_left
  23. 0023exact hright_left_left
  24. 0024cases hright_right
  25. 0025trans 1
  26. 0026exact hleft_right_right
  27. 0027symm
  28. 0028exact hright_right_right