BT00UY · Bertrand theorem

primorial_prefix_interval_split

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

Split Primorial(a+l) into its prefix and offset interval product.

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

∀ a. ∀ l. ∀ z. Primorial(a + l,z) → ∃ x. ∃ y. Primorial(a,x) ∧ ((∃ n. ∃ m. (∀ k. Lt(k,l) → ∃ i. BetaAt(n,m,k,i) ∧ (Prime(S (a + k)) ∧ i = S (a + k) ∨ ¬Prime(S (a + k)) ∧ i = 1)) ∧ Product(n,m,l,y)) ∧ z = x · y)

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

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0014 Product PD0043 Primorial

7 occurrences

In local proof propositions

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0014 Product

13 occurrences

Exact expanded native-PA statement
forall a l z. (exists bpr_code_bppis_source bpr_scale_bppis_source. ((forall bpr_index_bppis_source_mask. (exists bpr_gap_bppis_source_mask_bound. bpr_gap_bppis_source_mask_bound + S (bpr_index_bppis_source_mask) = a + l) -> exists bpr_value_bppis_source_mask. ((((exists bpr_height_bppis_source_mask_decoded. bpr_height_bppis_source_mask_decoded + S (bpr_value_bppis_source_mask) = S ((S (bpr_index_bppis_source_mask)) * bpr_scale_bppis_source)) /\ exists bpr_quotient_bppis_source_mask_decoded. bpr_code_bppis_source = bpr_quotient_bppis_source_mask_decoded * S ((S (bpr_index_bppis_source_mask)) * bpr_scale_bppis_source) + (bpr_value_bppis_source_mask))) /\ (((((~(S (bpr_index_bppis_source_mask) = 1) /\ forall bpr_left_bppis_source_mask_choice_prime bpr_right_bppis_source_mask_choice_prime. S (bpr_index_bppis_source_mask) = bpr_left_bppis_source_mask_choice_prime * bpr_right_bppis_source_mask_choice_prime -> bpr_left_bppis_source_mask_choice_prime = 1 \/ bpr_right_bppis_source_mask_choice_prime = 1)) /\ bpr_value_bppis_source_mask = S (bpr_index_bppis_source_mask)) \/ (~((~(S (bpr_index_bppis_source_mask) = 1) /\ forall bpr_left_bppis_source_mask_choice_prime bpr_right_bppis_source_mask_choice_prime. S (bpr_index_bppis_source_mask) = bpr_left_bppis_source_mask_choice_prime * bpr_right_bppis_source_mask_choice_prime -> bpr_left_bppis_source_mask_choice_prime = 1 \/ bpr_right_bppis_source_mask_choice_prime = 1)) /\ bpr_value_bppis_source_mask = 1))))) /\ (exists ff_u_bppis_source_product ff_v_bppis_source_product. ((((exists ff_h_bppis_source_product_start. ff_h_bppis_source_product_start + S (1) = S ((S (0)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_start. ff_u_bppis_source_product = ff_q_bppis_source_product_start * S ((S (0)) * ff_v_bppis_source_product) + (1))) /\ ((((exists ff_h_bppis_source_product_terminal. ff_h_bppis_source_product_terminal + S (z) = S ((S (a + l)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_terminal. ff_u_bppis_source_product = ff_q_bppis_source_product_terminal * S ((S (a + l)) * ff_v_bppis_source_product) + (z))) /\ forall ff_i_bppis_source_product. (exists ff_lt_bppis_source_product_bound. ff_lt_bppis_source_product_bound + S ff_i_bppis_source_product = a + l) -> exists ff_p_bppis_source_product ff_r_bppis_source_product ff_s_bppis_source_product. ((((exists ff_h_bppis_source_product_factor. ff_h_bppis_source_product_factor + S (ff_p_bppis_source_product) = S ((S (ff_i_bppis_source_product)) * bpr_scale_bppis_source)) /\ exists ff_q_bppis_source_product_factor. bpr_code_bppis_source = ff_q_bppis_source_product_factor * S ((S (ff_i_bppis_source_product)) * bpr_scale_bppis_source) + (ff_p_bppis_source_product))) /\ ((((exists ff_h_bppis_source_product_partial. ff_h_bppis_source_product_partial + S (ff_r_bppis_source_product) = S ((S (ff_i_bppis_source_product)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_partial. ff_u_bppis_source_product = ff_q_bppis_source_product_partial * S ((S (ff_i_bppis_source_product)) * ff_v_bppis_source_product) + (ff_r_bppis_source_product))) /\ ((((exists ff_h_bppis_source_product_successor. ff_h_bppis_source_product_successor + S (ff_s_bppis_source_product) = S ((S (S ff_i_bppis_source_product)) * ff_v_bppis_source_product)) /\ exists ff_q_bppis_source_product_successor. ff_u_bppis_source_product = ff_q_bppis_source_product_successor * S ((S (S ff_i_bppis_source_product)) * ff_v_bppis_source_product) + (ff_s_bppis_source_product))) /\ ff_s_bppis_source_product = ff_r_bppis_source_product * ff_p_bppis_source_product)))))))) -> (exists x y. (exists bpr_code_bppis_prefix bpr_scale_bppis_prefix. ((forall bpr_index_bppis_prefix_mask. (exists bpr_gap_bppis_prefix_mask_bound. bpr_gap_bppis_prefix_mask_bound + S (bpr_index_bppis_prefix_mask) = a) -> exists bpr_value_bppis_prefix_mask. ((((exists bpr_height_bppis_prefix_mask_decoded. bpr_height_bppis_prefix_mask_decoded + S (bpr_value_bppis_prefix_mask) = S ((S (bpr_index_bppis_prefix_mask)) * bpr_scale_bppis_prefix)) /\ exists bpr_quotient_bppis_prefix_mask_decoded. bpr_code_bppis_prefix = bpr_quotient_bppis_prefix_mask_decoded * S ((S (bpr_index_bppis_prefix_mask)) * bpr_scale_bppis_prefix) + (bpr_value_bppis_prefix_mask))) /\ (((((~(S (bpr_index_bppis_prefix_mask) = 1) /\ forall bpr_left_bppis_prefix_mask_choice_prime bpr_right_bppis_prefix_mask_choice_prime. S (bpr_index_bppis_prefix_mask) = bpr_left_bppis_prefix_mask_choice_prime * bpr_right_bppis_prefix_mask_choice_prime -> bpr_left_bppis_prefix_mask_choice_prime = 1 \/ bpr_right_bppis_prefix_mask_choice_prime = 1)) /\ bpr_value_bppis_prefix_mask = S (bpr_index_bppis_prefix_mask)) \/ (~((~(S (bpr_index_bppis_prefix_mask) = 1) /\ forall bpr_left_bppis_prefix_mask_choice_prime bpr_right_bppis_prefix_mask_choice_prime. S (bpr_index_bppis_prefix_mask) = bpr_left_bppis_prefix_mask_choice_prime * bpr_right_bppis_prefix_mask_choice_prime -> bpr_left_bppis_prefix_mask_choice_prime = 1 \/ bpr_right_bppis_prefix_mask_choice_prime = 1)) /\ bpr_value_bppis_prefix_mask = 1))))) /\ (exists ff_u_bppis_prefix_product ff_v_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_start. ff_h_bppis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_start. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_start * S ((S (0)) * ff_v_bppis_prefix_product) + (1))) /\ ((((exists ff_h_bppis_prefix_product_terminal. ff_h_bppis_prefix_product_terminal + S (x) = S ((S (a)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_terminal. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_terminal * S ((S (a)) * ff_v_bppis_prefix_product) + (x))) /\ forall ff_i_bppis_prefix_product. (exists ff_lt_bppis_prefix_product_bound. ff_lt_bppis_prefix_product_bound + S ff_i_bppis_prefix_product = a) -> exists ff_p_bppis_prefix_product ff_r_bppis_prefix_product ff_s_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_factor. ff_h_bppis_prefix_product_factor + S (ff_p_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * bpr_scale_bppis_prefix)) /\ exists ff_q_bppis_prefix_product_factor. bpr_code_bppis_prefix = ff_q_bppis_prefix_product_factor * S ((S (ff_i_bppis_prefix_product)) * bpr_scale_bppis_prefix) + (ff_p_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_partial. ff_h_bppis_prefix_product_partial + S (ff_r_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_partial. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_partial * S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_r_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_successor. ff_h_bppis_prefix_product_successor + S (ff_s_bppis_prefix_product) = S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_successor. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_successor * S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_s_bppis_prefix_product))) /\ ff_s_bppis_prefix_product = ff_r_bppis_prefix_product * ff_p_bppis_prefix_product)))))))) /\ ((exists bpr_code_bppis_interval bpr_scale_bppis_interval. ((forall bpr_index_bppis_interval_mask. (exists bpr_gap_bppis_interval_mask_bound. bpr_gap_bppis_interval_mask_bound + S (bpr_index_bppis_interval_mask) = l) -> exists bpr_value_bppis_interval_mask. ((((exists bpr_height_bppis_interval_mask_decoded. bpr_height_bppis_interval_mask_decoded + S (bpr_value_bppis_interval_mask) = S ((S (bpr_index_bppis_interval_mask)) * bpr_scale_bppis_interval)) /\ exists bpr_quotient_bppis_interval_mask_decoded. bpr_code_bppis_interval = bpr_quotient_bppis_interval_mask_decoded * S ((S (bpr_index_bppis_interval_mask)) * bpr_scale_bppis_interval) + (bpr_value_bppis_interval_mask))) /\ (((((~(S (a + bpr_index_bppis_interval_mask) = 1) /\ forall bpr_left_bppis_interval_mask_choice_prime bpr_right_bppis_interval_mask_choice_prime. S (a + bpr_index_bppis_interval_mask) = bpr_left_bppis_interval_mask_choice_prime * bpr_right_bppis_interval_mask_choice_prime -> bpr_left_bppis_interval_mask_choice_prime = 1 \/ bpr_right_bppis_interval_mask_choice_prime = 1)) /\ bpr_value_bppis_interval_mask = S (a + bpr_index_bppis_interval_mask)) \/ (~((~(S (a + bpr_index_bppis_interval_mask) = 1) /\ forall bpr_left_bppis_interval_mask_choice_prime bpr_right_bppis_interval_mask_choice_prime. S (a + bpr_index_bppis_interval_mask) = bpr_left_bppis_interval_mask_choice_prime * bpr_right_bppis_interval_mask_choice_prime -> bpr_left_bppis_interval_mask_choice_prime = 1 \/ bpr_right_bppis_interval_mask_choice_prime = 1)) /\ bpr_value_bppis_interval_mask = 1))))) /\ (exists ff_u_bppis_interval_product ff_v_bppis_interval_product. ((((exists ff_h_bppis_interval_product_start. ff_h_bppis_interval_product_start + S (1) = S ((S (0)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_start. ff_u_bppis_interval_product = ff_q_bppis_interval_product_start * S ((S (0)) * ff_v_bppis_interval_product) + (1))) /\ ((((exists ff_h_bppis_interval_product_terminal. ff_h_bppis_interval_product_terminal + S (y) = S ((S (l)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_terminal. ff_u_bppis_interval_product = ff_q_bppis_interval_product_terminal * S ((S (l)) * ff_v_bppis_interval_product) + (y))) /\ forall ff_i_bppis_interval_product. (exists ff_lt_bppis_interval_product_bound. ff_lt_bppis_interval_product_bound + S ff_i_bppis_interval_product = l) -> exists ff_p_bppis_interval_product ff_r_bppis_interval_product ff_s_bppis_interval_product. ((((exists ff_h_bppis_interval_product_factor. ff_h_bppis_interval_product_factor + S (ff_p_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * bpr_scale_bppis_interval)) /\ exists ff_q_bppis_interval_product_factor. bpr_code_bppis_interval = ff_q_bppis_interval_product_factor * S ((S (ff_i_bppis_interval_product)) * bpr_scale_bppis_interval) + (ff_p_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_partial. ff_h_bppis_interval_product_partial + S (ff_r_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_partial. ff_u_bppis_interval_product = ff_q_bppis_interval_product_partial * S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_r_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_successor. ff_h_bppis_interval_product_successor + S (ff_s_bppis_interval_product) = S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_successor. ff_u_bppis_interval_product = ff_q_bppis_interval_product_successor * S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_s_bppis_interval_product))) /\ ff_s_bppis_interval_product = ff_r_bppis_interval_product * ff_p_bppis_interval_product)))))))) /\ z = x * y))

Proof neighborhood

Direct theorem prerequisites

BT00UQ beta_product_prefix_suffix_split BT00US primorial_interval_factor_prefix_exists BT00UW primorial_interval_factor_prefix_shift BT00UX primorial_factor_prefix_restrict_add

Direct theorem dependents

BT00VU primorial_four_power_support_package 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

54 script commands · 18 reading checkpoints · 4 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 prefix suffix splitprimorial interval factor prefix existsprimorial interval factor prefix shiftprimorial factor prefix restrict add
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro l
  3. L3
    intro z
  4. L4
    intro hprimorial
02Separate the logical casesL5–7

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

  1. L5
    cases hprimorial
  2. L6
    cases hprimorial_witness
  3. L7
    cases hprimorial_witness_witness
03Establish hrestrictedL8–10

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

  1. L8
    have hrestricted : ∀ bpr_index_bppis_restricted. Lt(bpr_index_bppis_restricted,a) → ∃ y. BetaAt(x,x1,bpr_index_bppis_restricted,y) ∧ (Prime(S bpr_index_bppis_restricted) ∧ y = S bpr_index_bppis_restricted ∨ ¬Prime(S bpr_index_bppis_restricted) ∧ y = 1)Definitions: Lt(bpr_index_bppis_restricted,a)BetaAt(x,x1,bpr_index_bppis_restricted,y)Prime(S bpr_index_bppis_restricted)Original native command in the exact edition
  2. L9
    apply primorial_factor_prefix_restrict_add
  3. L10
    exact hprimorial_witness_witness_left
04Establish hintervalL11–12

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

  1. L11
    have hinterval : ∃ d. ∃ e. ∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ y = S (a + x) ∨ ¬Prime(S (a + x)) ∧ y = 1)Definitions: Lt(x,l)BetaAt(d,e,x,y)Prime(S (a + x))Original native command in the exact edition
  2. L12
    apply primorial_interval_factor_prefix_exists
05Separate the logical casesL13–14

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

  1. L13
    cases hinterval
  2. L14
    cases hinterval_witness
06Establish hshiftL15–24

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

  1. L15
    have hshift : ∀ i. ∀ p. Lt(i,l) → BetaAt(x,x1,a + i,p) → BetaAt(x2,x3,i,p)Definitions: Lt(i,l)BetaAt(x,x1,a + i,p)BetaAt(x2,x3,i,p)Original native command in the exact edition
  2. L16
    specialize primorial_interval_factor_prefix_shift a
  3. L17
    specialize primorial_interval_factor_prefix_shift x
  4. L18
    specialize primorial_interval_factor_prefix_shift x1
  5. L19
    specialize primorial_interval_factor_prefix_shift x2
  6. L20
    specialize primorial_interval_factor_prefix_shift x3
  7. L21
    specialize primorial_interval_factor_prefix_shift l
  8. L22
    apply primorial_interval_factor_prefix_shift
  9. L23
    exact hprimorial_witness_witness_left
  10. L24
    exact hinterval_witness_witness
07Establish hsplitL25–34

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

  1. L25
    have hsplit : ∃ p. ∃ q. Product(x,x1,a,p) ∧ (Product(x2,x3,l,q) ∧ z = p · q)Definitions: Product(x,x1,a,p)Product(x2,x3,l,q)Original native command in the exact edition
  2. L26
    specialize beta_product_prefix_suffix_split x
  3. L27
    specialize beta_product_prefix_suffix_split x1
  4. L28
    specialize beta_product_prefix_suffix_split x2
  5. L29
    specialize beta_product_prefix_suffix_split x3
  6. L30
    specialize beta_product_prefix_suffix_split a
  7. L31
    specialize beta_product_prefix_suffix_split l
  8. L32
    specialize beta_product_prefix_suffix_split z
  9. L33
    apply beta_product_prefix_suffix_split
  10. L34
    exact hshift
08Use earlier factsL35–35

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

  1. L35
    exact hprimorial_witness_witness_right
09Separate the logical casesL36–39

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

  1. L36
    cases hsplit
  2. L37
    cases hsplit_witness
  3. L38
    cases hsplit_witness_witness
  4. L39
    cases hsplit_witness_witness_right
10Construct an explicit witnessL40–41

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

  1. L40
    exists x4
  2. L41
    exists x5
11Separate the logical casesL42–42

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

  1. L42
    split
12Construct an explicit witnessL43–44

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

  1. L43
    exists x
  2. L44
    exists x1
13Separate the logical casesL45–45

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

  1. L45
    split
14Use earlier factsL46–47

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

  1. L46
    exact hrestricted
  2. L47
    exact hsplit_witness_witness_left
15Separate the logical casesL48–48

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

  1. L48
    split
16Construct an explicit witnessL49–50

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

  1. L49
    exists x2
  2. L50
    exists x3
17Separate the logical casesL51–51

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

  1. L51
    split
18Use earlier factsL52–54

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

  1. L52
    exact hinterval_witness_witness
  2. L53
    exact hsplit_witness_witness_right_left
  3. L54
    exact hsplit_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro a
  2. 0002intro l
  3. 0003intro z
  4. 0004intro hprimorial
  5. 0005cases hprimorial
  6. 0006cases hprimorial_witness
  7. 0007cases hprimorial_witness_witness
  8. 0008have hrestricted : ∀ bpr_index_bppis_restricted. Lt(bpr_index_bppis_restricted,a) → ∃ y. BetaAt(x,x1,bpr_index_bppis_restricted,y) ∧ (Prime(S bpr_index_bppis_restricted) ∧ y = S bpr_index_bppis_restricted ∨ ¬Prime(S bpr_index_bppis_restricted) ∧ y = 1)
    Exact native replay linehave hrestricted : forall bpr_index_bppis_restricted. (exists bpr_gap_bppis_restricted_bound. bpr_gap_bppis_restricted_bound + S (bpr_index_bppis_restricted) = a) -> exists bpr_value_bppis_restricted. ((((exists bpr_height_bppis_restricted_decoded. bpr_height_bppis_restricted_decoded + S (bpr_value_bppis_restricted) = S ((S (bpr_index_bppis_restricted)) * x1)) /\ exists bpr_quotient_bppis_restricted_decoded. x = bpr_quotient_bppis_restricted_decoded * S ((S (bpr_index_bppis_restricted)) * x1) + (bpr_value_bppis_restricted))) /\ (((((~(S (bpr_index_bppis_restricted) = 1) /\ forall bpr_left_bppis_restricted_choice_prime bpr_right_bppis_restricted_choice_prime. S (bpr_index_bppis_restricted) = bpr_left_bppis_restricted_choice_prime * bpr_right_bppis_restricted_choice_prime -> bpr_left_bppis_restricted_choice_prime = 1 \/ bpr_right_bppis_restricted_choice_prime = 1)) /\ bpr_value_bppis_restricted = S (bpr_index_bppis_restricted)) \/ (~((~(S (bpr_index_bppis_restricted) = 1) /\ forall bpr_left_bppis_restricted_choice_prime bpr_right_bppis_restricted_choice_prime. S (bpr_index_bppis_restricted) = bpr_left_bppis_restricted_choice_prime * bpr_right_bppis_restricted_choice_prime -> bpr_left_bppis_restricted_choice_prime = 1 \/ bpr_right_bppis_restricted_choice_prime = 1)) /\ bpr_value_bppis_restricted = 1))))
  9. 0009apply primorial_factor_prefix_restrict_add
  10. 0010exact hprimorial_witness_witness_left
  11. 0011have hinterval : ∃ d. ∃ e. ∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ y = S (a + x) ∨ ¬Prime(S (a + x)) ∧ y = 1)
    Exact native replay linehave hinterval : exists d e. (forall bpr_index_bppis_interval_prefix. (exists bpr_gap_bppis_interval_prefix_bound. bpr_gap_bppis_interval_prefix_bound + S (bpr_index_bppis_interval_prefix) = l) -> exists bpr_value_bppis_interval_prefix. ((((exists bpr_height_bppis_interval_prefix_decoded. bpr_height_bppis_interval_prefix_decoded + S (bpr_value_bppis_interval_prefix) = S ((S (bpr_index_bppis_interval_prefix)) * e)) /\ exists bpr_quotient_bppis_interval_prefix_decoded. d = bpr_quotient_bppis_interval_prefix_decoded * S ((S (bpr_index_bppis_interval_prefix)) * e) + (bpr_value_bppis_interval_prefix))) /\ (((((~(S (a + bpr_index_bppis_interval_prefix) = 1) /\ forall bpr_left_bppis_interval_prefix_choice_prime bpr_right_bppis_interval_prefix_choice_prime. S (a + bpr_index_bppis_interval_prefix) = bpr_left_bppis_interval_prefix_choice_prime * bpr_right_bppis_interval_prefix_choice_prime -> bpr_left_bppis_interval_prefix_choice_prime = 1 \/ bpr_right_bppis_interval_prefix_choice_prime = 1)) /\ bpr_value_bppis_interval_prefix = S (a + bpr_index_bppis_interval_prefix)) \/ (~((~(S (a + bpr_index_bppis_interval_prefix) = 1) /\ forall bpr_left_bppis_interval_prefix_choice_prime bpr_right_bppis_interval_prefix_choice_prime. S (a + bpr_index_bppis_interval_prefix) = bpr_left_bppis_interval_prefix_choice_prime * bpr_right_bppis_interval_prefix_choice_prime -> bpr_left_bppis_interval_prefix_choice_prime = 1 \/ bpr_right_bppis_interval_prefix_choice_prime = 1)) /\ bpr_value_bppis_interval_prefix = 1)))))
  12. 0012apply primorial_interval_factor_prefix_exists
  13. 0013cases hinterval
  14. 0014cases hinterval_witness
  15. 0015have hshift : ∀ i. ∀ p. Lt(i,l) → BetaAt(x,x1,a + i,p) → BetaAt(x2,x3,i,p)
    Exact native replay linehave hshift : forall i p. (exists bpr_gap_bppis_shift_bound. bpr_gap_bppis_shift_bound + S (i) = l) -> (((exists bpr_height_bppis_shift_source. bpr_height_bppis_shift_source + S (p) = S ((S (a + i)) * x1)) /\ exists bpr_quotient_bppis_shift_source. x = bpr_quotient_bppis_shift_source * S ((S (a + i)) * x1) + (p))) -> (((exists bpr_height_bppis_shift_target. bpr_height_bppis_shift_target + S (p) = S ((S (i)) * x3)) /\ exists bpr_quotient_bppis_shift_target. x2 = bpr_quotient_bppis_shift_target * S ((S (i)) * x3) + (p)))
  16. 0016specialize primorial_interval_factor_prefix_shift a
  17. 0017specialize primorial_interval_factor_prefix_shift x
  18. 0018specialize primorial_interval_factor_prefix_shift x1
  19. 0019specialize primorial_interval_factor_prefix_shift x2
  20. 0020specialize primorial_interval_factor_prefix_shift x3
  21. 0021specialize primorial_interval_factor_prefix_shift l
  22. 0022apply primorial_interval_factor_prefix_shift
  23. 0023exact hprimorial_witness_witness_left
  24. 0024exact hinterval_witness_witness
  25. 0025have hsplit : ∃ p. ∃ q. Product(x,x1,a,p) ∧ (Product(x2,x3,l,q) ∧ z = p · q)
    Exact native replay linehave hsplit : exists p q. (exists ff_u_bppis_prefix_product ff_v_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_start. ff_h_bppis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_start. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_start * S ((S (0)) * ff_v_bppis_prefix_product) + (1))) /\ ((((exists ff_h_bppis_prefix_product_terminal. ff_h_bppis_prefix_product_terminal + S (p) = S ((S (a)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_terminal. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_terminal * S ((S (a)) * ff_v_bppis_prefix_product) + (p))) /\ forall ff_i_bppis_prefix_product. (exists ff_lt_bppis_prefix_product_bound. ff_lt_bppis_prefix_product_bound + S ff_i_bppis_prefix_product = a) -> exists ff_p_bppis_prefix_product ff_r_bppis_prefix_product ff_s_bppis_prefix_product. ((((exists ff_h_bppis_prefix_product_factor. ff_h_bppis_prefix_product_factor + S (ff_p_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * x1)) /\ exists ff_q_bppis_prefix_product_factor. x = ff_q_bppis_prefix_product_factor * S ((S (ff_i_bppis_prefix_product)) * x1) + (ff_p_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_partial. ff_h_bppis_prefix_product_partial + S (ff_r_bppis_prefix_product) = S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_partial. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_partial * S ((S (ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_r_bppis_prefix_product))) /\ ((((exists ff_h_bppis_prefix_product_successor. ff_h_bppis_prefix_product_successor + S (ff_s_bppis_prefix_product) = S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product)) /\ exists ff_q_bppis_prefix_product_successor. ff_u_bppis_prefix_product = ff_q_bppis_prefix_product_successor * S ((S (S ff_i_bppis_prefix_product)) * ff_v_bppis_prefix_product) + (ff_s_bppis_prefix_product))) /\ ff_s_bppis_prefix_product = ff_r_bppis_prefix_product * ff_p_bppis_prefix_product)))))) /\ ((exists ff_u_bppis_interval_product ff_v_bppis_interval_product. ((((exists ff_h_bppis_interval_product_start. ff_h_bppis_interval_product_start + S (1) = S ((S (0)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_start. ff_u_bppis_interval_product = ff_q_bppis_interval_product_start * S ((S (0)) * ff_v_bppis_interval_product) + (1))) /\ ((((exists ff_h_bppis_interval_product_terminal. ff_h_bppis_interval_product_terminal + S (q) = S ((S (l)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_terminal. ff_u_bppis_interval_product = ff_q_bppis_interval_product_terminal * S ((S (l)) * ff_v_bppis_interval_product) + (q))) /\ forall ff_i_bppis_interval_product. (exists ff_lt_bppis_interval_product_bound. ff_lt_bppis_interval_product_bound + S ff_i_bppis_interval_product = l) -> exists ff_p_bppis_interval_product ff_r_bppis_interval_product ff_s_bppis_interval_product. ((((exists ff_h_bppis_interval_product_factor. ff_h_bppis_interval_product_factor + S (ff_p_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * x3)) /\ exists ff_q_bppis_interval_product_factor. x2 = ff_q_bppis_interval_product_factor * S ((S (ff_i_bppis_interval_product)) * x3) + (ff_p_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_partial. ff_h_bppis_interval_product_partial + S (ff_r_bppis_interval_product) = S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_partial. ff_u_bppis_interval_product = ff_q_bppis_interval_product_partial * S ((S (ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_r_bppis_interval_product))) /\ ((((exists ff_h_bppis_interval_product_successor. ff_h_bppis_interval_product_successor + S (ff_s_bppis_interval_product) = S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product)) /\ exists ff_q_bppis_interval_product_successor. ff_u_bppis_interval_product = ff_q_bppis_interval_product_successor * S ((S (S ff_i_bppis_interval_product)) * ff_v_bppis_interval_product) + (ff_s_bppis_interval_product))) /\ ff_s_bppis_interval_product = ff_r_bppis_interval_product * ff_p_bppis_interval_product)))))) /\ z = p * q)
  26. 0026specialize beta_product_prefix_suffix_split x
  27. 0027specialize beta_product_prefix_suffix_split x1
  28. 0028specialize beta_product_prefix_suffix_split x2
  29. 0029specialize beta_product_prefix_suffix_split x3
  30. 0030specialize beta_product_prefix_suffix_split a
  31. 0031specialize beta_product_prefix_suffix_split l
  32. 0032specialize beta_product_prefix_suffix_split z
  33. 0033apply beta_product_prefix_suffix_split
  34. 0034exact hshift
  35. 0035exact hprimorial_witness_witness_right
  36. 0036cases hsplit
  37. 0037cases hsplit_witness
  38. 0038cases hsplit_witness_witness
  39. 0039cases hsplit_witness_witness_right
  40. 0040exists x4
  41. 0041exists x5
  42. 0042split
  43. 0043exists x
  44. 0044exists x1
  45. 0045split
  46. 0046exact hrestricted
  47. 0047exact hsplit_witness_witness_left
  48. 0048split
  49. 0049exists x2
  50. 0050exists x3
  51. 0051split
  52. 0052exact hinterval_witness_witness
  53. 0053exact hsplit_witness_witness_right_left
  54. 0054exact hsplit_witness_witness_right_right