BT00UD · Bertrand theorem

primorial_succ_decompose

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

A successor primorial splits into its previous value and selector.

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(S m,z) → ∃ x. ∃ y. (Prime(S m) ∧ x = S m ∨ ¬Prime(S m) ∧ x = 1) ∧ (Primorial(m,y) ∧ z = y · 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

PD0004 Prime PD0043 Primorial

4 occurrences

In local proof propositions

PD0004 Prime PD0013 BetaAt PD0014 Product

5 occurrences

Exact expanded native-PA statement
forall m z. (exists bpr_code_bp_succ_source bpr_scale_bp_succ_source. ((forall bpr_index_bp_succ_source_mask. (exists bpr_gap_bp_succ_source_mask_bound. bpr_gap_bp_succ_source_mask_bound + S (bpr_index_bp_succ_source_mask) = S m) -> exists bpr_value_bp_succ_source_mask. ((((exists bpr_height_bp_succ_source_mask_decoded. bpr_height_bp_succ_source_mask_decoded + S (bpr_value_bp_succ_source_mask) = S ((S (bpr_index_bp_succ_source_mask)) * bpr_scale_bp_succ_source)) /\ exists bpr_quotient_bp_succ_source_mask_decoded. bpr_code_bp_succ_source = bpr_quotient_bp_succ_source_mask_decoded * S ((S (bpr_index_bp_succ_source_mask)) * bpr_scale_bp_succ_source) + (bpr_value_bp_succ_source_mask))) /\ (((((~(S (bpr_index_bp_succ_source_mask) = 1) /\ forall bpr_left_bp_succ_source_mask_choice_prime bpr_right_bp_succ_source_mask_choice_prime. S (bpr_index_bp_succ_source_mask) = bpr_left_bp_succ_source_mask_choice_prime * bpr_right_bp_succ_source_mask_choice_prime -> bpr_left_bp_succ_source_mask_choice_prime = 1 \/ bpr_right_bp_succ_source_mask_choice_prime = 1)) /\ bpr_value_bp_succ_source_mask = S (bpr_index_bp_succ_source_mask)) \/ (~((~(S (bpr_index_bp_succ_source_mask) = 1) /\ forall bpr_left_bp_succ_source_mask_choice_prime bpr_right_bp_succ_source_mask_choice_prime. S (bpr_index_bp_succ_source_mask) = bpr_left_bp_succ_source_mask_choice_prime * bpr_right_bp_succ_source_mask_choice_prime -> bpr_left_bp_succ_source_mask_choice_prime = 1 \/ bpr_right_bp_succ_source_mask_choice_prime = 1)) /\ bpr_value_bp_succ_source_mask = 1))))) /\ (exists ff_u_bp_succ_source_product ff_v_bp_succ_source_product. ((((exists ff_h_bp_succ_source_product_start. ff_h_bp_succ_source_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_start. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_start * S ((S (0)) * ff_v_bp_succ_source_product) + (1))) /\ ((((exists ff_h_bp_succ_source_product_terminal. ff_h_bp_succ_source_product_terminal + S (z) = S ((S (S m)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_terminal. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_terminal * S ((S (S m)) * ff_v_bp_succ_source_product) + (z))) /\ forall ff_i_bp_succ_source_product. (exists ff_lt_bp_succ_source_product_bound. ff_lt_bp_succ_source_product_bound + S ff_i_bp_succ_source_product = S m) -> exists ff_p_bp_succ_source_product ff_r_bp_succ_source_product ff_s_bp_succ_source_product. ((((exists ff_h_bp_succ_source_product_factor. ff_h_bp_succ_source_product_factor + S (ff_p_bp_succ_source_product) = S ((S (ff_i_bp_succ_source_product)) * bpr_scale_bp_succ_source)) /\ exists ff_q_bp_succ_source_product_factor. bpr_code_bp_succ_source = ff_q_bp_succ_source_product_factor * S ((S (ff_i_bp_succ_source_product)) * bpr_scale_bp_succ_source) + (ff_p_bp_succ_source_product))) /\ ((((exists ff_h_bp_succ_source_product_partial. ff_h_bp_succ_source_product_partial + S (ff_r_bp_succ_source_product) = S ((S (ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_partial. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_partial * S ((S (ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product) + (ff_r_bp_succ_source_product))) /\ ((((exists ff_h_bp_succ_source_product_successor. ff_h_bp_succ_source_product_successor + S (ff_s_bp_succ_source_product) = S ((S (S ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product)) /\ exists ff_q_bp_succ_source_product_successor. ff_u_bp_succ_source_product = ff_q_bp_succ_source_product_successor * S ((S (S ff_i_bp_succ_source_product)) * ff_v_bp_succ_source_product) + (ff_s_bp_succ_source_product))) /\ ff_s_bp_succ_source_product = ff_r_bp_succ_source_product * ff_p_bp_succ_source_product)))))))) -> (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))

Proof neighborhood

Direct theorem prerequisites

BT005J beta_product_succ_decompose BT0042 beta_at_unique BT000E le_refl BT0018 le_succ

Direct theorem dependents

BT00UE primorial_positive BT00VQ primorial_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

40 script commands · 18 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 (4)
beta product succ decomposebeta at uniquele reflle succ
01Fix variables and assumptionsL1–3

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

  1. L1
    intro m
  2. L2
    intro z
  3. L3
    intro hprimorial
02Separate the logical casesL4–6

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

  1. L4
    cases hprimorial
  2. L5
    cases hprimorial_witness
  3. L6
    cases hprimorial_witness_witness
03Establish hdecompositionL7–9

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

  1. L7
    have hdecomposition : ∃ p. ∃ r. BetaAt(x,x1,m,p) ∧ (Product(x,x1,m,r) ∧ z = r · p)Definitions: BetaAt(x,x1,m,p)Product(x,x1,m,r)Original native command in the exact edition
  2. L8
    apply beta_product_succ_decompose
  3. L9
    exact hprimorial_witness_witness_right
04Separate the logical casesL10–13

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

  1. L10
    cases hdecomposition
  2. L11
    cases hdecomposition_witness
  3. L12
    cases hdecomposition_witness_witness
  4. L13
    cases hdecomposition_witness_witness_right
05Establish hterminalL14–16

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

  1. L14
    have hterminal : ∃ a. BetaAt(x,x1,m,a) ∧ (Prime(S m) ∧ a = S m ∨ ¬Prime(S m) ∧ a = 1)Definitions: BetaAt(x,x1,m,a)Prime(S m)Original native command in the exact edition
  2. L15
    apply hprimorial_witness_witness_left
  3. L16
    apply le_refl
06Separate the logical casesL17–18

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

  1. L17
    cases hterminal
  2. L18
    cases hterminal_witness
07Establish hfactorL19–22

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

  1. L19
    have hfactor : x2 = x4
  2. L20
    apply beta_at_unique
  3. L21
    exact hdecomposition_witness_witness_left
  4. L22
    exact hterminal_witness_left
08Construct an explicit witnessL23–24

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

  1. L23
    exists x4
  2. L24
    exists x3
09Separate the logical casesL25–25

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

  1. L25
    split
10Use earlier factsL26–26

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

  1. L26
    exact hterminal_witness_right
11Separate the logical casesL27–27

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

  1. L27
    split
12Construct an explicit witnessL28–29

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

  1. L28
    exists x
  2. L29
    exists x1
13Separate the logical casesL30–30

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

  1. L30
    split
14Fix variables and assumptionsL31–32

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

  1. L31
    intro i
  2. L32
    intro hi
15Use earlier factsL33–36

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

  1. L33
    apply hprimorial_witness_witness_left
  2. L34
    apply le_succ
  3. L35
    exact hi
  4. L36
    exact hdecomposition_witness_witness_right_left
16Calculate and transport equalitiesL37–37

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

  1. L37
    trans x3 * x2
17Use earlier factsL38–38

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

  1. L38
    exact hdecomposition_witness_witness_right_right
18Calculate and transport equalitiesL39–40

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

  1. L39
    rewrite hfactor
  2. L40
    refl

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro m
  2. 0002intro z
  3. 0003intro hprimorial
  4. 0004cases hprimorial
  5. 0005cases hprimorial_witness
  6. 0006cases hprimorial_witness_witness
  7. 0007have hdecomposition : ∃ p. ∃ r. BetaAt(x,x1,m,p) ∧ (Product(x,x1,m,r) ∧ z = r · p)
    Exact native replay linehave hdecomposition : exists p r. (((exists bpr_height_bp_succ_last_factor. bpr_height_bp_succ_last_factor + S (p) = S ((S (m)) * x1)) /\ exists bpr_quotient_bp_succ_last_factor. x = bpr_quotient_bp_succ_last_factor * S ((S (m)) * x1) + (p))) /\ ((exists ff_u_bp_succ_prefix_product ff_v_bp_succ_prefix_product. ((((exists ff_h_bp_succ_prefix_product_start. ff_h_bp_succ_prefix_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_start. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_start * S ((S (0)) * ff_v_bp_succ_prefix_product) + (1))) /\ ((((exists ff_h_bp_succ_prefix_product_terminal. ff_h_bp_succ_prefix_product_terminal + S (r) = S ((S (m)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_terminal. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_terminal * S ((S (m)) * ff_v_bp_succ_prefix_product) + (r))) /\ forall ff_i_bp_succ_prefix_product. (exists ff_lt_bp_succ_prefix_product_bound. ff_lt_bp_succ_prefix_product_bound + S ff_i_bp_succ_prefix_product = m) -> exists ff_p_bp_succ_prefix_product ff_r_bp_succ_prefix_product ff_s_bp_succ_prefix_product. ((((exists ff_h_bp_succ_prefix_product_factor. ff_h_bp_succ_prefix_product_factor + S (ff_p_bp_succ_prefix_product) = S ((S (ff_i_bp_succ_prefix_product)) * x1)) /\ exists ff_q_bp_succ_prefix_product_factor. x = ff_q_bp_succ_prefix_product_factor * S ((S (ff_i_bp_succ_prefix_product)) * x1) + (ff_p_bp_succ_prefix_product))) /\ ((((exists ff_h_bp_succ_prefix_product_partial. ff_h_bp_succ_prefix_product_partial + S (ff_r_bp_succ_prefix_product) = S ((S (ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_partial. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_partial * S ((S (ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product) + (ff_r_bp_succ_prefix_product))) /\ ((((exists ff_h_bp_succ_prefix_product_successor. ff_h_bp_succ_prefix_product_successor + S (ff_s_bp_succ_prefix_product) = S ((S (S ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product)) /\ exists ff_q_bp_succ_prefix_product_successor. ff_u_bp_succ_prefix_product = ff_q_bp_succ_prefix_product_successor * S ((S (S ff_i_bp_succ_prefix_product)) * ff_v_bp_succ_prefix_product) + (ff_s_bp_succ_prefix_product))) /\ ff_s_bp_succ_prefix_product = ff_r_bp_succ_prefix_product * ff_p_bp_succ_prefix_product)))))) /\ z = r * p)
  8. 0008apply beta_product_succ_decompose
  9. 0009exact hprimorial_witness_witness_right
  10. 0010cases hdecomposition
  11. 0011cases hdecomposition_witness
  12. 0012cases hdecomposition_witness_witness
  13. 0013cases hdecomposition_witness_witness_right
  14. 0014have hterminal : ∃ a. BetaAt(x,x1,m,a) ∧ (Prime(S m) ∧ a = S m ∨ ¬Prime(S m) ∧ a = 1)
    Exact native replay linehave hterminal : exists a. ((((exists bpr_height_bp_succ_mask_terminal. bpr_height_bp_succ_mask_terminal + S (a) = S ((S (m)) * x1)) /\ exists bpr_quotient_bp_succ_mask_terminal. x = bpr_quotient_bp_succ_mask_terminal * S ((S (m)) * x1) + (a))) /\ (((((~(S (m) = 1) /\ forall bpr_left_bp_succ_mask_choice_prime bpr_right_bp_succ_mask_choice_prime. S (m) = bpr_left_bp_succ_mask_choice_prime * bpr_right_bp_succ_mask_choice_prime -> bpr_left_bp_succ_mask_choice_prime = 1 \/ bpr_right_bp_succ_mask_choice_prime = 1)) /\ a = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bp_succ_mask_choice_prime bpr_right_bp_succ_mask_choice_prime. S (m) = bpr_left_bp_succ_mask_choice_prime * bpr_right_bp_succ_mask_choice_prime -> bpr_left_bp_succ_mask_choice_prime = 1 \/ bpr_right_bp_succ_mask_choice_prime = 1)) /\ a = 1))))
  15. 0015apply hprimorial_witness_witness_left
  16. 0016apply le_refl
  17. 0017cases hterminal
  18. 0018cases hterminal_witness
  19. 0019have hfactor : x2 = x4
  20. 0020apply beta_at_unique
  21. 0021exact hdecomposition_witness_witness_left
  22. 0022exact hterminal_witness_left
  23. 0023exists x4
  24. 0024exists x3
  25. 0025split
  26. 0026exact hterminal_witness_right
  27. 0027split
  28. 0028exists x
  29. 0029exists x1
  30. 0030split
  31. 0031intro i
  32. 0032intro hi
  33. 0033apply hprimorial_witness_witness_left
  34. 0034apply le_succ
  35. 0035exact hi
  36. 0036exact hdecomposition_witness_witness_right_left
  37. 0037trans x3 * x2
  38. 0038exact hdecomposition_witness_witness_right_right
  39. 0039rewrite hfactor
  40. 0040refl