BT00UE · Bertrand theorem

primorial_positive

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

Every relational primorial value is a successor.

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

∀ m. ∀ z. Primorial(m,z) → ∃ x. z = S x

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

PD0043 Primorial

1 occurrences

In local proof propositions

PD0004 Prime PD0043 Primorial

3 occurrences

Exact expanded native-PA statement
forall m z. (exists bpr_code_bp_positive_source bpr_scale_bp_positive_source. ((forall bpr_index_bp_positive_source_mask. (exists bpr_gap_bp_positive_source_mask_bound. bpr_gap_bp_positive_source_mask_bound + S (bpr_index_bp_positive_source_mask) = m) -> exists bpr_value_bp_positive_source_mask. ((((exists bpr_height_bp_positive_source_mask_decoded. bpr_height_bp_positive_source_mask_decoded + S (bpr_value_bp_positive_source_mask) = S ((S (bpr_index_bp_positive_source_mask)) * bpr_scale_bp_positive_source)) /\ exists bpr_quotient_bp_positive_source_mask_decoded. bpr_code_bp_positive_source = bpr_quotient_bp_positive_source_mask_decoded * S ((S (bpr_index_bp_positive_source_mask)) * bpr_scale_bp_positive_source) + (bpr_value_bp_positive_source_mask))) /\ (((((~(S (bpr_index_bp_positive_source_mask) = 1) /\ forall bpr_left_bp_positive_source_mask_choice_prime bpr_right_bp_positive_source_mask_choice_prime. S (bpr_index_bp_positive_source_mask) = bpr_left_bp_positive_source_mask_choice_prime * bpr_right_bp_positive_source_mask_choice_prime -> bpr_left_bp_positive_source_mask_choice_prime = 1 \/ bpr_right_bp_positive_source_mask_choice_prime = 1)) /\ bpr_value_bp_positive_source_mask = S (bpr_index_bp_positive_source_mask)) \/ (~((~(S (bpr_index_bp_positive_source_mask) = 1) /\ forall bpr_left_bp_positive_source_mask_choice_prime bpr_right_bp_positive_source_mask_choice_prime. S (bpr_index_bp_positive_source_mask) = bpr_left_bp_positive_source_mask_choice_prime * bpr_right_bp_positive_source_mask_choice_prime -> bpr_left_bp_positive_source_mask_choice_prime = 1 \/ bpr_right_bp_positive_source_mask_choice_prime = 1)) /\ bpr_value_bp_positive_source_mask = 1))))) /\ (exists ff_u_bp_positive_source_product ff_v_bp_positive_source_product. ((((exists ff_h_bp_positive_source_product_start. ff_h_bp_positive_source_product_start + S (1) = S ((S (0)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_start. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_start * S ((S (0)) * ff_v_bp_positive_source_product) + (1))) /\ ((((exists ff_h_bp_positive_source_product_terminal. ff_h_bp_positive_source_product_terminal + S (z) = S ((S (m)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_terminal. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_terminal * S ((S (m)) * ff_v_bp_positive_source_product) + (z))) /\ forall ff_i_bp_positive_source_product. (exists ff_lt_bp_positive_source_product_bound. ff_lt_bp_positive_source_product_bound + S ff_i_bp_positive_source_product = m) -> exists ff_p_bp_positive_source_product ff_r_bp_positive_source_product ff_s_bp_positive_source_product. ((((exists ff_h_bp_positive_source_product_factor. ff_h_bp_positive_source_product_factor + S (ff_p_bp_positive_source_product) = S ((S (ff_i_bp_positive_source_product)) * bpr_scale_bp_positive_source)) /\ exists ff_q_bp_positive_source_product_factor. bpr_code_bp_positive_source = ff_q_bp_positive_source_product_factor * S ((S (ff_i_bp_positive_source_product)) * bpr_scale_bp_positive_source) + (ff_p_bp_positive_source_product))) /\ ((((exists ff_h_bp_positive_source_product_partial. ff_h_bp_positive_source_product_partial + S (ff_r_bp_positive_source_product) = S ((S (ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_partial. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_partial * S ((S (ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product) + (ff_r_bp_positive_source_product))) /\ ((((exists ff_h_bp_positive_source_product_successor. ff_h_bp_positive_source_product_successor + S (ff_s_bp_positive_source_product) = S ((S (S ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_successor. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_successor * S ((S (S ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product) + (ff_s_bp_positive_source_product))) /\ ff_s_bp_positive_source_product = ff_r_bp_positive_source_product * ff_p_bp_positive_source_product)))))))) -> exists r. z = S r

Proof neighborhood

Direct theorem prerequisites

BT0005 mul_succ_left BT00UC primorial_zero BT00UD primorial_succ_decompose

Direct theorem dependents

BT0111 no_bertrand_middle_contribution_interval_le_four_pow

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

42 script commands · 22 reading checkpoints · 3 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 (3)
mul succ leftprimorial zeroprimorial succ decompose
01Induction on mL1–3

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

  1. L1
    induction m
  2. L2
    intro z
  3. L3
    intro hprimorial
02Establish hzL4–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply primorial zero.

  1. L4
    have hz : z = 1
  2. L5
    apply primorial_zero
  3. L6
    exact hprimorial
03Construct an explicit witnessL7–7

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

  1. L7
    exists 0
04Calculate and transport equalitiesL8–8

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

  1. L8
    trans 1
05Use earlier factsL9–9

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

  1. L9
    exact hz
06Calculate and transport equalitiesL10–10

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

  1. L10
    refl
07Fix variables and assumptionsL11–12

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

  1. L11
    intro z
  2. L12
    intro hprimorial
08Establish hdecompositionL13–15

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

  1. L13
    have hdecomposition : ∃ p. ∃ r. (Prime(S m) ∧ p = S m ∨ ¬Prime(S m) ∧ p = 1) ∧ (Primorial(m,r) ∧ z = r · p)Definitions: Prime(S m)Primorial(m,r)Original native command in the exact edition
  2. L14
    apply primorial_succ_decompose
  3. L15
    exact hprimorial
09Separate the logical casesL16–19

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

  1. L16
    cases hdecomposition
  2. L17
    cases hdecomposition_witness
  3. L18
    cases hdecomposition_witness_witness
  4. L19
    cases hdecomposition_witness_witness_right
10Establish hpreviousL20–22

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

  1. L20
    have hprevious : exists t. x1 = S t
  2. L21
    apply IH
  3. L22
    exact hdecomposition_witness_witness_right_left
11Separate the logical casesL23–25

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

  1. L23
    cases hprevious
  2. L24
    cases hdecomposition_witness_witness_left
  3. L25
    cases hdecomposition_witness_witness_left_left
12Construct an explicit witnessL26–26

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

  1. L26
    exists x2 * S m + m
13Calculate and transport equalitiesL27–27

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

  1. L27
    trans x1 * x
14Use earlier factsL28–28

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

  1. L28
    exact hdecomposition_witness_witness_right_right
15Calculate and transport equalitiesL29–31

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

  1. L29
    rewrite hprevious_witness
  2. L30
    rewrite hdecomposition_witness_witness_left_left_right
  3. L31
    trans x2 * S m + S m
16Use earlier factsL32–33

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

  1. L32
    apply mul_succ_left
  2. L33
    apply PA4
17Separate the logical casesL34–34

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

  1. L34
    cases hdecomposition_witness_witness_left_right
18Construct an explicit witnessL35–35

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

  1. L35
    exists x2 * 1 + 0
19Calculate and transport equalitiesL36–36

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

  1. L36
    trans x1 * x
20Use earlier factsL37–37

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

  1. L37
    exact hdecomposition_witness_witness_right_right
21Calculate and transport equalitiesL38–40

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

  1. L38
    rewrite hprevious_witness
  2. L39
    rewrite hdecomposition_witness_witness_left_right_right
  3. L40
    trans x2 * 1 + 1
22Use earlier factsL41–42

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

  1. L41
    apply mul_succ_left
  2. L42
    apply PA4

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001induction m
  2. 0002intro z
  3. 0003intro hprimorial
  4. 0004have hz : z = 1
  5. 0005apply primorial_zero
  6. 0006exact hprimorial
  7. 0007exists 0
  8. 0008trans 1
  9. 0009exact hz
  10. 0010refl
  11. 0011intro z
  12. 0012intro hprimorial
  13. 0013have hdecomposition : ∃ p. ∃ r. (Prime(S m) ∧ p = S m ∨ ¬Prime(S m) ∧ p = 1) ∧ (Primorial(m,r) ∧ z = r · p)
    Exact native replay linehave hdecomposition : exists p r. (((((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = 1))) /\ ((exists bpr_code_bp_succ_predecessor bpr_scale_bp_succ_predecessor. ((forall bpr_index_bp_succ_predecessor_mask. (exists bpr_gap_bp_succ_predecessor_mask_bound. bpr_gap_bp_succ_predecessor_mask_bound + S (bpr_index_bp_succ_predecessor_mask) = m) -> exists bpr_value_bp_succ_predecessor_mask. ((((exists bpr_height_bp_succ_predecessor_mask_decoded. bpr_height_bp_succ_predecessor_mask_decoded + S (bpr_value_bp_succ_predecessor_mask) = S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor)) /\ exists bpr_quotient_bp_succ_predecessor_mask_decoded. bpr_code_bp_succ_predecessor = bpr_quotient_bp_succ_predecessor_mask_decoded * S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor) + (bpr_value_bp_succ_predecessor_mask))) /\ (((((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = S (bpr_index_bp_succ_predecessor_mask)) \/ (~((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = 1))))) /\ (exists ff_u_bp_succ_predecessor_product ff_v_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_start. ff_h_bp_succ_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_start. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_start * S ((S (0)) * ff_v_bp_succ_predecessor_product) + (1))) /\ ((((exists ff_h_bp_succ_predecessor_product_terminal. ff_h_bp_succ_predecessor_product_terminal + S (r) = S ((S (m)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_terminal. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_terminal * S ((S (m)) * ff_v_bp_succ_predecessor_product) + (r))) /\ forall ff_i_bp_succ_predecessor_product. (exists ff_lt_bp_succ_predecessor_product_bound. ff_lt_bp_succ_predecessor_product_bound + S ff_i_bp_succ_predecessor_product = m) -> exists ff_p_bp_succ_predecessor_product ff_r_bp_succ_predecessor_product ff_s_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_factor. ff_h_bp_succ_predecessor_product_factor + S (ff_p_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor)) /\ exists ff_q_bp_succ_predecessor_product_factor. bpr_code_bp_succ_predecessor = ff_q_bp_succ_predecessor_product_factor * S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor) + (ff_p_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_partial. ff_h_bp_succ_predecessor_product_partial + S (ff_r_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_partial. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_partial * S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_r_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_successor. ff_h_bp_succ_predecessor_product_successor + S (ff_s_bp_succ_predecessor_product) = S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_successor. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_successor * S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_s_bp_succ_predecessor_product))) /\ ff_s_bp_succ_predecessor_product = ff_r_bp_succ_predecessor_product * ff_p_bp_succ_predecessor_product)))))))) /\ z = r * p)
  14. 0014apply primorial_succ_decompose
  15. 0015exact hprimorial
  16. 0016cases hdecomposition
  17. 0017cases hdecomposition_witness
  18. 0018cases hdecomposition_witness_witness
  19. 0019cases hdecomposition_witness_witness_right
  20. 0020have hprevious : exists t. x1 = S t
  21. 0021apply IH
  22. 0022exact hdecomposition_witness_witness_right_left
  23. 0023cases hprevious
  24. 0024cases hdecomposition_witness_witness_left
  25. 0025cases hdecomposition_witness_witness_left_left
  26. 0026exists x2 * S m + m
  27. 0027trans x1 * x
  28. 0028exact hdecomposition_witness_witness_right_right
  29. 0029rewrite hprevious_witness
  30. 0030rewrite hdecomposition_witness_witness_left_left_right
  31. 0031trans x2 * S m + S m
  32. 0032apply mul_succ_left
  33. 0033apply PA4
  34. 0034cases hdecomposition_witness_witness_left_right
  35. 0035exists x2 * 1 + 0
  36. 0036trans x1 * x
  37. 0037exact hdecomposition_witness_witness_right_right
  38. 0038rewrite hprevious_witness
  39. 0039rewrite hdecomposition_witness_witness_left_right_right
  40. 0040trans x2 * 1 + 1
  41. 0041apply mul_succ_left
  42. 0042apply PA4