BT00VQ · Bertrand theorem

primorial_one

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

The inclusive Primorial at one is exactly one.

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

∀ z. Primorial(1,z) → z = 1

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 z. (exists bpr_code_bpo_source bpr_scale_bpo_source. ((forall bpr_index_bpo_source_mask. (exists bpr_gap_bpo_source_mask_bound. bpr_gap_bpo_source_mask_bound + S (bpr_index_bpo_source_mask) = 1) -> exists bpr_value_bpo_source_mask. ((((exists bpr_height_bpo_source_mask_decoded. bpr_height_bpo_source_mask_decoded + S (bpr_value_bpo_source_mask) = S ((S (bpr_index_bpo_source_mask)) * bpr_scale_bpo_source)) /\ exists bpr_quotient_bpo_source_mask_decoded. bpr_code_bpo_source = bpr_quotient_bpo_source_mask_decoded * S ((S (bpr_index_bpo_source_mask)) * bpr_scale_bpo_source) + (bpr_value_bpo_source_mask))) /\ (((((~(S (bpr_index_bpo_source_mask) = 1) /\ forall bpr_left_bpo_source_mask_choice_prime bpr_right_bpo_source_mask_choice_prime. S (bpr_index_bpo_source_mask) = bpr_left_bpo_source_mask_choice_prime * bpr_right_bpo_source_mask_choice_prime -> bpr_left_bpo_source_mask_choice_prime = 1 \/ bpr_right_bpo_source_mask_choice_prime = 1)) /\ bpr_value_bpo_source_mask = S (bpr_index_bpo_source_mask)) \/ (~((~(S (bpr_index_bpo_source_mask) = 1) /\ forall bpr_left_bpo_source_mask_choice_prime bpr_right_bpo_source_mask_choice_prime. S (bpr_index_bpo_source_mask) = bpr_left_bpo_source_mask_choice_prime * bpr_right_bpo_source_mask_choice_prime -> bpr_left_bpo_source_mask_choice_prime = 1 \/ bpr_right_bpo_source_mask_choice_prime = 1)) /\ bpr_value_bpo_source_mask = 1))))) /\ (exists ff_u_bpo_source_product ff_v_bpo_source_product. ((((exists ff_h_bpo_source_product_start. ff_h_bpo_source_product_start + S (1) = S ((S (0)) * ff_v_bpo_source_product)) /\ exists ff_q_bpo_source_product_start. ff_u_bpo_source_product = ff_q_bpo_source_product_start * S ((S (0)) * ff_v_bpo_source_product) + (1))) /\ ((((exists ff_h_bpo_source_product_terminal. ff_h_bpo_source_product_terminal + S (z) = S ((S (1)) * ff_v_bpo_source_product)) /\ exists ff_q_bpo_source_product_terminal. ff_u_bpo_source_product = ff_q_bpo_source_product_terminal * S ((S (1)) * ff_v_bpo_source_product) + (z))) /\ forall ff_i_bpo_source_product. (exists ff_lt_bpo_source_product_bound. ff_lt_bpo_source_product_bound + S ff_i_bpo_source_product = 1) -> exists ff_p_bpo_source_product ff_r_bpo_source_product ff_s_bpo_source_product. ((((exists ff_h_bpo_source_product_factor. ff_h_bpo_source_product_factor + S (ff_p_bpo_source_product) = S ((S (ff_i_bpo_source_product)) * bpr_scale_bpo_source)) /\ exists ff_q_bpo_source_product_factor. bpr_code_bpo_source = ff_q_bpo_source_product_factor * S ((S (ff_i_bpo_source_product)) * bpr_scale_bpo_source) + (ff_p_bpo_source_product))) /\ ((((exists ff_h_bpo_source_product_partial. ff_h_bpo_source_product_partial + S (ff_r_bpo_source_product) = S ((S (ff_i_bpo_source_product)) * ff_v_bpo_source_product)) /\ exists ff_q_bpo_source_product_partial. ff_u_bpo_source_product = ff_q_bpo_source_product_partial * S ((S (ff_i_bpo_source_product)) * ff_v_bpo_source_product) + (ff_r_bpo_source_product))) /\ ((((exists ff_h_bpo_source_product_successor. ff_h_bpo_source_product_successor + S (ff_s_bpo_source_product) = S ((S (S ff_i_bpo_source_product)) * ff_v_bpo_source_product)) /\ exists ff_q_bpo_source_product_successor. ff_u_bpo_source_product = ff_q_bpo_source_product_successor * S ((S (S ff_i_bpo_source_product)) * ff_v_bpo_source_product) + (ff_s_bpo_source_product))) /\ ff_s_bpo_source_product = ff_r_bpo_source_product * ff_p_bpo_source_product)))))))) -> z = 1

Proof neighborhood

Direct theorem prerequisites

BT00UC primorial_zero BT00UD primorial_succ_decompose

Direct theorem dependents

BT00VV primorial_le_four_pow_bounded

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

27 script commands · 12 reading checkpoints · 2 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)
primorial zeroprimorial succ decompose
01Fix variables and assumptionsL1–2

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

  1. L1
    intro z
  2. L2
    intro hprimorial
02Establish hdecompositionL3–7

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

  1. L3
    have hdecomposition : ∃ p. ∃ r. (Prime(1) ∧ p = 1 ∨ ¬Prime(1) ∧ p = 1) ∧ (Primorial(0,r) ∧ z = r · p)Definitions: Prime(1)Primorial(0,r)Original native command in the exact edition
  2. L4
    specialize primorial_succ_decompose 0
  3. L5
    specialize primorial_succ_decompose z
  4. L6
    apply primorial_succ_decompose
  5. L7
    exact hprimorial
03Separate the logical casesL8–11

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

  1. L8
    cases hdecomposition
  2. L9
    cases hdecomposition_witness
  3. L10
    cases hdecomposition_witness_witness
  4. L11
    cases hdecomposition_witness_witness_right
04Establish hrL12–14

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

  1. L12
    have hr : x1 = 1
  2. L13
    apply primorial_zero
  3. L14
    exact hdecomposition_witness_witness_right_left
05Separate the logical casesL15–16

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

  1. L15
    cases hdecomposition_witness_witness_left
  2. L16
    cases hdecomposition_witness_witness_left_left
06Calculate and transport equalitiesL17–19

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

  1. L17
    rewrite hr at hdecomposition_witness_witness_right_right
  2. L18
    rewrite hdecomposition_witness_witness_left_left_right at hdecomposition_witness_witness_right_right
  3. L19
    trans 1 * 1
07Use earlier factsL20–20

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

  1. L20
    exact hdecomposition_witness_witness_right_right
08Calculate and transport equalitiesL21–21

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

  1. L21
    norm_num
09Separate the logical casesL22–22

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

  1. L22
    cases hdecomposition_witness_witness_left_right
10Calculate and transport equalitiesL23–25

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

  1. L23
    rewrite hr at hdecomposition_witness_witness_right_right
  2. L24
    rewrite hdecomposition_witness_witness_left_right_right at hdecomposition_witness_witness_right_right
  3. L25
    trans 1 * 1
11Use earlier factsL26–26

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

  1. L26
    exact hdecomposition_witness_witness_right_right
12Calculate and transport equalitiesL27–27

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

  1. L27
    norm_num

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro z
  2. 0002intro hprimorial
  3. 0003have hdecomposition : ∃ p. ∃ r. (Prime(1) ∧ p = 1 ∨ ¬Prime(1) ∧ p = 1) ∧ (Primorial(0,r) ∧ z = r · p)
    Exact native replay linehave hdecomposition : exists p r. (((((~(S (0) = 1) /\ forall bpr_left_bpo_factor_prime bpr_right_bpo_factor_prime. S (0) = bpr_left_bpo_factor_prime * bpr_right_bpo_factor_prime -> bpr_left_bpo_factor_prime = 1 \/ bpr_right_bpo_factor_prime = 1)) /\ p = S (0)) \/ (~((~(S (0) = 1) /\ forall bpr_left_bpo_factor_prime bpr_right_bpo_factor_prime. S (0) = bpr_left_bpo_factor_prime * bpr_right_bpo_factor_prime -> bpr_left_bpo_factor_prime = 1 \/ bpr_right_bpo_factor_prime = 1)) /\ p = 1))) /\ ((exists bpr_code_bpo_previous bpr_scale_bpo_previous. ((forall bpr_index_bpo_previous_mask. (exists bpr_gap_bpo_previous_mask_bound. bpr_gap_bpo_previous_mask_bound + S (bpr_index_bpo_previous_mask) = 0) -> exists bpr_value_bpo_previous_mask. ((((exists bpr_height_bpo_previous_mask_decoded. bpr_height_bpo_previous_mask_decoded + S (bpr_value_bpo_previous_mask) = S ((S (bpr_index_bpo_previous_mask)) * bpr_scale_bpo_previous)) /\ exists bpr_quotient_bpo_previous_mask_decoded. bpr_code_bpo_previous = bpr_quotient_bpo_previous_mask_decoded * S ((S (bpr_index_bpo_previous_mask)) * bpr_scale_bpo_previous) + (bpr_value_bpo_previous_mask))) /\ (((((~(S (bpr_index_bpo_previous_mask) = 1) /\ forall bpr_left_bpo_previous_mask_choice_prime bpr_right_bpo_previous_mask_choice_prime. S (bpr_index_bpo_previous_mask) = bpr_left_bpo_previous_mask_choice_prime * bpr_right_bpo_previous_mask_choice_prime -> bpr_left_bpo_previous_mask_choice_prime = 1 \/ bpr_right_bpo_previous_mask_choice_prime = 1)) /\ bpr_value_bpo_previous_mask = S (bpr_index_bpo_previous_mask)) \/ (~((~(S (bpr_index_bpo_previous_mask) = 1) /\ forall bpr_left_bpo_previous_mask_choice_prime bpr_right_bpo_previous_mask_choice_prime. S (bpr_index_bpo_previous_mask) = bpr_left_bpo_previous_mask_choice_prime * bpr_right_bpo_previous_mask_choice_prime -> bpr_left_bpo_previous_mask_choice_prime = 1 \/ bpr_right_bpo_previous_mask_choice_prime = 1)) /\ bpr_value_bpo_previous_mask = 1))))) /\ (exists ff_u_bpo_previous_product ff_v_bpo_previous_product. ((((exists ff_h_bpo_previous_product_start. ff_h_bpo_previous_product_start + S (1) = S ((S (0)) * ff_v_bpo_previous_product)) /\ exists ff_q_bpo_previous_product_start. ff_u_bpo_previous_product = ff_q_bpo_previous_product_start * S ((S (0)) * ff_v_bpo_previous_product) + (1))) /\ ((((exists ff_h_bpo_previous_product_terminal. ff_h_bpo_previous_product_terminal + S (r) = S ((S (0)) * ff_v_bpo_previous_product)) /\ exists ff_q_bpo_previous_product_terminal. ff_u_bpo_previous_product = ff_q_bpo_previous_product_terminal * S ((S (0)) * ff_v_bpo_previous_product) + (r))) /\ forall ff_i_bpo_previous_product. (exists ff_lt_bpo_previous_product_bound. ff_lt_bpo_previous_product_bound + S ff_i_bpo_previous_product = 0) -> exists ff_p_bpo_previous_product ff_r_bpo_previous_product ff_s_bpo_previous_product. ((((exists ff_h_bpo_previous_product_factor. ff_h_bpo_previous_product_factor + S (ff_p_bpo_previous_product) = S ((S (ff_i_bpo_previous_product)) * bpr_scale_bpo_previous)) /\ exists ff_q_bpo_previous_product_factor. bpr_code_bpo_previous = ff_q_bpo_previous_product_factor * S ((S (ff_i_bpo_previous_product)) * bpr_scale_bpo_previous) + (ff_p_bpo_previous_product))) /\ ((((exists ff_h_bpo_previous_product_partial. ff_h_bpo_previous_product_partial + S (ff_r_bpo_previous_product) = S ((S (ff_i_bpo_previous_product)) * ff_v_bpo_previous_product)) /\ exists ff_q_bpo_previous_product_partial. ff_u_bpo_previous_product = ff_q_bpo_previous_product_partial * S ((S (ff_i_bpo_previous_product)) * ff_v_bpo_previous_product) + (ff_r_bpo_previous_product))) /\ ((((exists ff_h_bpo_previous_product_successor. ff_h_bpo_previous_product_successor + S (ff_s_bpo_previous_product) = S ((S (S ff_i_bpo_previous_product)) * ff_v_bpo_previous_product)) /\ exists ff_q_bpo_previous_product_successor. ff_u_bpo_previous_product = ff_q_bpo_previous_product_successor * S ((S (S ff_i_bpo_previous_product)) * ff_v_bpo_previous_product) + (ff_s_bpo_previous_product))) /\ ff_s_bpo_previous_product = ff_r_bpo_previous_product * ff_p_bpo_previous_product)))))))) /\ z = r * p)
  4. 0004specialize primorial_succ_decompose 0
  5. 0005specialize primorial_succ_decompose z
  6. 0006apply primorial_succ_decompose
  7. 0007exact hprimorial
  8. 0008cases hdecomposition
  9. 0009cases hdecomposition_witness
  10. 0010cases hdecomposition_witness_witness
  11. 0011cases hdecomposition_witness_witness_right
  12. 0012have hr : x1 = 1
  13. 0013apply primorial_zero
  14. 0014exact hdecomposition_witness_witness_right_left
  15. 0015cases hdecomposition_witness_witness_left
  16. 0016cases hdecomposition_witness_witness_left_left
  17. 0017rewrite hr at hdecomposition_witness_witness_right_right
  18. 0018rewrite hdecomposition_witness_witness_left_left_right at hdecomposition_witness_witness_right_right
  19. 0019trans 1 * 1
  20. 0020exact hdecomposition_witness_witness_right_right
  21. 0021norm_num
  22. 0022cases hdecomposition_witness_witness_left_right
  23. 0023rewrite hr at hdecomposition_witness_witness_right_right
  24. 0024rewrite hdecomposition_witness_witness_left_right_right at hdecomposition_witness_witness_right_right
  25. 0025trans 1 * 1
  26. 0026exact hdecomposition_witness_witness_right_right
  27. 0027norm_num