BT00YN · Bertrand theorem

prime_contribution_choice_exists

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

Every index has its complete prime-power contribution or 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

∀ n. ∀ i. ∃ a. Prime(S i) ∧ (∃ x. PowerValuation(S i,n,x) ∧ Pow(S i,x,a)) ∨ ¬Prime(S i) ∧ a = 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

PD0004 Prime PD0020 Pow PD0046 PowerValuation

4 occurrences

In local proof propositions

PD0020 Pow PD0046 PowerValuation

2 occurrences

Exact expanded native-PA statement
forall n i. exists a. (((((~(S (i) = 1) /\ forall bpr_left_bpcce_result_prime bpr_right_bpcce_result_prime. S (i) = bpr_left_bpcce_result_prime * bpr_right_bpcce_result_prime -> bpr_left_bpcce_result_prime = 1 \/ bpr_right_bpcce_result_prime = 1)) /\ exists bpr_choice_exponent_bpcce_result. ((((exists bpr_le_gap_bpcce_result_valuation_selected_bound. bpr_le_gap_bpcce_result_valuation_selected_bound + (bpr_choice_exponent_bpcce_result) = (n)) /\ (exists bpr_power_value_bpcce_result_valuation_selected. ((exists bpr_power_code_bpcce_result_valuation_selected_power bpr_power_scale_bpcce_result_valuation_selected_power. ((forall bpr_power_index_bpcce_result_valuation_selected_power. (exists bpr_gap_bpcce_result_valuation_selected_power_repeat_bound. bpr_gap_bpcce_result_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcce_result_valuation_selected_power) = bpr_choice_exponent_bpcce_result) -> (((exists bpr_height_bpcce_result_valuation_selected_power_repeat_entry. bpr_height_bpcce_result_valuation_selected_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcce_result_valuation_selected_power)) * bpr_power_scale_bpcce_result_valuation_selected_power)) /\ exists bpr_quotient_bpcce_result_valuation_selected_power_repeat_entry. bpr_power_code_bpcce_result_valuation_selected_power = bpr_quotient_bpcce_result_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcce_result_valuation_selected_power)) * bpr_power_scale_bpcce_result_valuation_selected_power) + (S (i))))) /\ (exists ff_u_bpcce_result_valuation_selected_power_product ff_v_bpcce_result_valuation_selected_power_product. ((((exists ff_h_bpcce_result_valuation_selected_power_product_start. ff_h_bpcce_result_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_result_valuation_selected_power_product)) /\ exists ff_q_bpcce_result_valuation_selected_power_product_start. ff_u_bpcce_result_valuation_selected_power_product = ff_q_bpcce_result_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcce_result_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcce_result_valuation_selected_power_product_terminal. ff_h_bpcce_result_valuation_selected_power_product_terminal + S (bpr_power_value_bpcce_result_valuation_selected) = S ((S (bpr_choice_exponent_bpcce_result)) * ff_v_bpcce_result_valuation_selected_power_product)) /\ exists ff_q_bpcce_result_valuation_selected_power_product_terminal. ff_u_bpcce_result_valuation_selected_power_product = ff_q_bpcce_result_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_result)) * ff_v_bpcce_result_valuation_selected_power_product) + (bpr_power_value_bpcce_result_valuation_selected))) /\ forall ff_i_bpcce_result_valuation_selected_power_product. (exists ff_lt_bpcce_result_valuation_selected_power_product_bound. ff_lt_bpcce_result_valuation_selected_power_product_bound + S ff_i_bpcce_result_valuation_selected_power_product = bpr_choice_exponent_bpcce_result) -> exists ff_p_bpcce_result_valuation_selected_power_product ff_r_bpcce_result_valuation_selected_power_product ff_s_bpcce_result_valuation_selected_power_product. ((((exists ff_h_bpcce_result_valuation_selected_power_product_factor. ff_h_bpcce_result_valuation_selected_power_product_factor + S (ff_p_bpcce_result_valuation_selected_power_product) = S ((S (ff_i_bpcce_result_valuation_selected_power_product)) * bpr_power_scale_bpcce_result_valuation_selected_power)) /\ exists ff_q_bpcce_result_valuation_selected_power_product_factor. bpr_power_code_bpcce_result_valuation_selected_power = ff_q_bpcce_result_valuation_selected_power_product_factor * S ((S (ff_i_bpcce_result_valuation_selected_power_product)) * bpr_power_scale_bpcce_result_valuation_selected_power) + (ff_p_bpcce_result_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_result_valuation_selected_power_product_partial. ff_h_bpcce_result_valuation_selected_power_product_partial + S (ff_r_bpcce_result_valuation_selected_power_product) = S ((S (ff_i_bpcce_result_valuation_selected_power_product)) * ff_v_bpcce_result_valuation_selected_power_product)) /\ exists ff_q_bpcce_result_valuation_selected_power_product_partial. ff_u_bpcce_result_valuation_selected_power_product = ff_q_bpcce_result_valuation_selected_power_product_partial * S ((S (ff_i_bpcce_result_valuation_selected_power_product)) * ff_v_bpcce_result_valuation_selected_power_product) + (ff_r_bpcce_result_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_result_valuation_selected_power_product_successor. ff_h_bpcce_result_valuation_selected_power_product_successor + S (ff_s_bpcce_result_valuation_selected_power_product) = S ((S (S ff_i_bpcce_result_valuation_selected_power_product)) * ff_v_bpcce_result_valuation_selected_power_product)) /\ exists ff_q_bpcce_result_valuation_selected_power_product_successor. ff_u_bpcce_result_valuation_selected_power_product = ff_q_bpcce_result_valuation_selected_power_product_successor * S ((S (S ff_i_bpcce_result_valuation_selected_power_product)) * ff_v_bpcce_result_valuation_selected_power_product) + (ff_s_bpcce_result_valuation_selected_power_product))) /\ ff_s_bpcce_result_valuation_selected_power_product = ff_r_bpcce_result_valuation_selected_power_product * ff_p_bpcce_result_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_result_valuation_selected_divides. n = (bpr_power_value_bpcce_result_valuation_selected) * bpr_divides_quotient_bpcce_result_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcce_result_valuation. (exists bpr_le_gap_bpcce_result_valuation_candidate_bound. bpr_le_gap_bpcce_result_valuation_candidate_bound + (bpr_valuation_candidate_bpcce_result_valuation) = (n)) -> (exists bpr_power_value_bpcce_result_valuation_candidate. ((exists bpr_power_code_bpcce_result_valuation_candidate_power bpr_power_scale_bpcce_result_valuation_candidate_power. ((forall bpr_power_index_bpcce_result_valuation_candidate_power. (exists bpr_gap_bpcce_result_valuation_candidate_power_repeat_bound. bpr_gap_bpcce_result_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcce_result_valuation_candidate_power) = bpr_valuation_candidate_bpcce_result_valuation) -> (((exists bpr_height_bpcce_result_valuation_candidate_power_repeat_entry. bpr_height_bpcce_result_valuation_candidate_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcce_result_valuation_candidate_power)) * bpr_power_scale_bpcce_result_valuation_candidate_power)) /\ exists bpr_quotient_bpcce_result_valuation_candidate_power_repeat_entry. bpr_power_code_bpcce_result_valuation_candidate_power = bpr_quotient_bpcce_result_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcce_result_valuation_candidate_power)) * bpr_power_scale_bpcce_result_valuation_candidate_power) + (S (i))))) /\ (exists ff_u_bpcce_result_valuation_candidate_power_product ff_v_bpcce_result_valuation_candidate_power_product. ((((exists ff_h_bpcce_result_valuation_candidate_power_product_start. ff_h_bpcce_result_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_result_valuation_candidate_power_product)) /\ exists ff_q_bpcce_result_valuation_candidate_power_product_start. ff_u_bpcce_result_valuation_candidate_power_product = ff_q_bpcce_result_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcce_result_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcce_result_valuation_candidate_power_product_terminal. ff_h_bpcce_result_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcce_result_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcce_result_valuation)) * ff_v_bpcce_result_valuation_candidate_power_product)) /\ exists ff_q_bpcce_result_valuation_candidate_power_product_terminal. ff_u_bpcce_result_valuation_candidate_power_product = ff_q_bpcce_result_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcce_result_valuation)) * ff_v_bpcce_result_valuation_candidate_power_product) + (bpr_power_value_bpcce_result_valuation_candidate))) /\ forall ff_i_bpcce_result_valuation_candidate_power_product. (exists ff_lt_bpcce_result_valuation_candidate_power_product_bound. ff_lt_bpcce_result_valuation_candidate_power_product_bound + S ff_i_bpcce_result_valuation_candidate_power_product = bpr_valuation_candidate_bpcce_result_valuation) -> exists ff_p_bpcce_result_valuation_candidate_power_product ff_r_bpcce_result_valuation_candidate_power_product ff_s_bpcce_result_valuation_candidate_power_product. ((((exists ff_h_bpcce_result_valuation_candidate_power_product_factor. ff_h_bpcce_result_valuation_candidate_power_product_factor + S (ff_p_bpcce_result_valuation_candidate_power_product) = S ((S (ff_i_bpcce_result_valuation_candidate_power_product)) * bpr_power_scale_bpcce_result_valuation_candidate_power)) /\ exists ff_q_bpcce_result_valuation_candidate_power_product_factor. bpr_power_code_bpcce_result_valuation_candidate_power = ff_q_bpcce_result_valuation_candidate_power_product_factor * S ((S (ff_i_bpcce_result_valuation_candidate_power_product)) * bpr_power_scale_bpcce_result_valuation_candidate_power) + (ff_p_bpcce_result_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_result_valuation_candidate_power_product_partial. ff_h_bpcce_result_valuation_candidate_power_product_partial + S (ff_r_bpcce_result_valuation_candidate_power_product) = S ((S (ff_i_bpcce_result_valuation_candidate_power_product)) * ff_v_bpcce_result_valuation_candidate_power_product)) /\ exists ff_q_bpcce_result_valuation_candidate_power_product_partial. ff_u_bpcce_result_valuation_candidate_power_product = ff_q_bpcce_result_valuation_candidate_power_product_partial * S ((S (ff_i_bpcce_result_valuation_candidate_power_product)) * ff_v_bpcce_result_valuation_candidate_power_product) + (ff_r_bpcce_result_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_result_valuation_candidate_power_product_successor. ff_h_bpcce_result_valuation_candidate_power_product_successor + S (ff_s_bpcce_result_valuation_candidate_power_product) = S ((S (S ff_i_bpcce_result_valuation_candidate_power_product)) * ff_v_bpcce_result_valuation_candidate_power_product)) /\ exists ff_q_bpcce_result_valuation_candidate_power_product_successor. ff_u_bpcce_result_valuation_candidate_power_product = ff_q_bpcce_result_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcce_result_valuation_candidate_power_product)) * ff_v_bpcce_result_valuation_candidate_power_product) + (ff_s_bpcce_result_valuation_candidate_power_product))) /\ ff_s_bpcce_result_valuation_candidate_power_product = ff_r_bpcce_result_valuation_candidate_power_product * ff_p_bpcce_result_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_result_valuation_candidate_divides. n = (bpr_power_value_bpcce_result_valuation_candidate) * bpr_divides_quotient_bpcce_result_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcce_result_valuation_candidate_below. bpr_le_gap_bpcce_result_valuation_candidate_below + (bpr_valuation_candidate_bpcce_result_valuation) = (bpr_choice_exponent_bpcce_result))) /\ (exists bpr_power_code_bpcce_result_power bpr_power_scale_bpcce_result_power. ((forall bpr_power_index_bpcce_result_power. (exists bpr_gap_bpcce_result_power_repeat_bound. bpr_gap_bpcce_result_power_repeat_bound + S (bpr_power_index_bpcce_result_power) = bpr_choice_exponent_bpcce_result) -> (((exists bpr_height_bpcce_result_power_repeat_entry. bpr_height_bpcce_result_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcce_result_power)) * bpr_power_scale_bpcce_result_power)) /\ exists bpr_quotient_bpcce_result_power_repeat_entry. bpr_power_code_bpcce_result_power = bpr_quotient_bpcce_result_power_repeat_entry * S ((S (bpr_power_index_bpcce_result_power)) * bpr_power_scale_bpcce_result_power) + (S (i))))) /\ (exists ff_u_bpcce_result_power_product ff_v_bpcce_result_power_product. ((((exists ff_h_bpcce_result_power_product_start. ff_h_bpcce_result_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_result_power_product)) /\ exists ff_q_bpcce_result_power_product_start. ff_u_bpcce_result_power_product = ff_q_bpcce_result_power_product_start * S ((S (0)) * ff_v_bpcce_result_power_product) + (1))) /\ ((((exists ff_h_bpcce_result_power_product_terminal. ff_h_bpcce_result_power_product_terminal + S (a) = S ((S (bpr_choice_exponent_bpcce_result)) * ff_v_bpcce_result_power_product)) /\ exists ff_q_bpcce_result_power_product_terminal. ff_u_bpcce_result_power_product = ff_q_bpcce_result_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_result)) * ff_v_bpcce_result_power_product) + (a))) /\ forall ff_i_bpcce_result_power_product. (exists ff_lt_bpcce_result_power_product_bound. ff_lt_bpcce_result_power_product_bound + S ff_i_bpcce_result_power_product = bpr_choice_exponent_bpcce_result) -> exists ff_p_bpcce_result_power_product ff_r_bpcce_result_power_product ff_s_bpcce_result_power_product. ((((exists ff_h_bpcce_result_power_product_factor. ff_h_bpcce_result_power_product_factor + S (ff_p_bpcce_result_power_product) = S ((S (ff_i_bpcce_result_power_product)) * bpr_power_scale_bpcce_result_power)) /\ exists ff_q_bpcce_result_power_product_factor. bpr_power_code_bpcce_result_power = ff_q_bpcce_result_power_product_factor * S ((S (ff_i_bpcce_result_power_product)) * bpr_power_scale_bpcce_result_power) + (ff_p_bpcce_result_power_product))) /\ ((((exists ff_h_bpcce_result_power_product_partial. ff_h_bpcce_result_power_product_partial + S (ff_r_bpcce_result_power_product) = S ((S (ff_i_bpcce_result_power_product)) * ff_v_bpcce_result_power_product)) /\ exists ff_q_bpcce_result_power_product_partial. ff_u_bpcce_result_power_product = ff_q_bpcce_result_power_product_partial * S ((S (ff_i_bpcce_result_power_product)) * ff_v_bpcce_result_power_product) + (ff_r_bpcce_result_power_product))) /\ ((((exists ff_h_bpcce_result_power_product_successor. ff_h_bpcce_result_power_product_successor + S (ff_s_bpcce_result_power_product) = S ((S (S ff_i_bpcce_result_power_product)) * ff_v_bpcce_result_power_product)) /\ exists ff_q_bpcce_result_power_product_successor. ff_u_bpcce_result_power_product = ff_q_bpcce_result_power_product_successor * S ((S (S ff_i_bpcce_result_power_product)) * ff_v_bpcce_result_power_product) + (ff_s_bpcce_result_power_product))) /\ ff_s_bpcce_result_power_product = ff_r_bpcce_result_power_product * ff_p_bpcce_result_power_product)))))))))) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpcce_result_prime bpr_right_bpcce_result_prime. S (i) = bpr_left_bpcce_result_prime * bpr_right_bpcce_result_prime -> bpr_left_bpcce_result_prime = 1 \/ bpr_right_bpcce_result_prime = 1)) /\ a = 1)))

Proof neighborhood

Direct theorem prerequisites

BT003H prime_decidable BT00Q7 power_valuation_exists BT0080 pow_exists

Direct theorem dependents

BT00YP prime_contribution_prefix_extend BT010K prime_contribution_interval_prefix_extend

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 · 17 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 (3)
prime decidablepower valuation existspow exists
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro i
02Use earlier factsL3–3

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

  1. L3
    specialize prime_decidable (S i)
03Separate the logical casesL4–4

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

  1. L4
    cases prime_decidable
04Establish hvaluationL5–8

Establish this local claim before using it. It is not an additional assumption.

  1. L5
    have hvaluation : ∃ e. PowerValuation(S i,n,e)Definitions: PowerValuation(S i,n,e)Original native command in the exact edition
  2. L6
    specialize power_valuation_exists (S i)
  3. L7
    specialize power_valuation_exists n
  4. L8
    exact power_valuation_exists
05Separate the logical casesL9–9

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

  1. L9
    cases hvaluation
06Establish hpowerL10–13

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hpower : ∃ a. Pow(S i,x,a)Definitions: Pow(S i,x,a)Original native command in the exact edition
  2. L11
    specialize pow_exists (S i)
  3. L12
    specialize pow_exists x
  4. L13
    exact pow_exists
07Separate the logical casesL14–14

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

  1. L14
    cases hpower
08Construct an explicit witnessL15–15

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

  1. L15
    exists x1
09Separate the logical casesL16–17

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

  1. L16
    left
  2. L17
    split
10Use earlier factsL18–18

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

  1. L18
    exact prime_decidable_left
11Construct an explicit witnessL19–19

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

  1. L19
    exists x
12Separate the logical casesL20–20

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

  1. L20
    split
13Use earlier factsL21–22

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

  1. L21
    exact hvaluation_witness
  2. L22
    exact hpower_witness
14Construct an explicit witnessL23–23

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

  1. L23
    exists 1
15Separate the logical casesL24–25

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

  1. L24
    right
  2. L25
    split
16Use earlier factsL26–26

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

  1. L26
    exact prime_decidable_right
17Calculate and transport equalitiesL27–27

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

  1. L27
    refl

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro n
  2. 0002intro i
  3. 0003specialize prime_decidable (S i)
  4. 0004cases prime_decidable
  5. 0005have hvaluation : ∃ e. PowerValuation(S i,n,e)
    Exact native replay linehave hvaluation : exists e. (((exists bpr_le_gap_bpcce_valuation_selected_bound. bpr_le_gap_bpcce_valuation_selected_bound + (e) = (n)) /\ (exists bpr_power_value_bpcce_valuation_selected. ((exists bpr_power_code_bpcce_valuation_selected_power bpr_power_scale_bpcce_valuation_selected_power. ((forall bpr_power_index_bpcce_valuation_selected_power. (exists bpr_gap_bpcce_valuation_selected_power_repeat_bound. bpr_gap_bpcce_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcce_valuation_selected_power) = e) -> (((exists bpr_height_bpcce_valuation_selected_power_repeat_entry. bpr_height_bpcce_valuation_selected_power_repeat_entry + S (S i) = S ((S (bpr_power_index_bpcce_valuation_selected_power)) * bpr_power_scale_bpcce_valuation_selected_power)) /\ exists bpr_quotient_bpcce_valuation_selected_power_repeat_entry. bpr_power_code_bpcce_valuation_selected_power = bpr_quotient_bpcce_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcce_valuation_selected_power)) * bpr_power_scale_bpcce_valuation_selected_power) + (S i)))) /\ (exists ff_u_bpcce_valuation_selected_power_product ff_v_bpcce_valuation_selected_power_product. ((((exists ff_h_bpcce_valuation_selected_power_product_start. ff_h_bpcce_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_valuation_selected_power_product)) /\ exists ff_q_bpcce_valuation_selected_power_product_start. ff_u_bpcce_valuation_selected_power_product = ff_q_bpcce_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcce_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcce_valuation_selected_power_product_terminal. ff_h_bpcce_valuation_selected_power_product_terminal + S (bpr_power_value_bpcce_valuation_selected) = S ((S (e)) * ff_v_bpcce_valuation_selected_power_product)) /\ exists ff_q_bpcce_valuation_selected_power_product_terminal. ff_u_bpcce_valuation_selected_power_product = ff_q_bpcce_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_bpcce_valuation_selected_power_product) + (bpr_power_value_bpcce_valuation_selected))) /\ forall ff_i_bpcce_valuation_selected_power_product. (exists ff_lt_bpcce_valuation_selected_power_product_bound. ff_lt_bpcce_valuation_selected_power_product_bound + S ff_i_bpcce_valuation_selected_power_product = e) -> exists ff_p_bpcce_valuation_selected_power_product ff_r_bpcce_valuation_selected_power_product ff_s_bpcce_valuation_selected_power_product. ((((exists ff_h_bpcce_valuation_selected_power_product_factor. ff_h_bpcce_valuation_selected_power_product_factor + S (ff_p_bpcce_valuation_selected_power_product) = S ((S (ff_i_bpcce_valuation_selected_power_product)) * bpr_power_scale_bpcce_valuation_selected_power)) /\ exists ff_q_bpcce_valuation_selected_power_product_factor. bpr_power_code_bpcce_valuation_selected_power = ff_q_bpcce_valuation_selected_power_product_factor * S ((S (ff_i_bpcce_valuation_selected_power_product)) * bpr_power_scale_bpcce_valuation_selected_power) + (ff_p_bpcce_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_valuation_selected_power_product_partial. ff_h_bpcce_valuation_selected_power_product_partial + S (ff_r_bpcce_valuation_selected_power_product) = S ((S (ff_i_bpcce_valuation_selected_power_product)) * ff_v_bpcce_valuation_selected_power_product)) /\ exists ff_q_bpcce_valuation_selected_power_product_partial. ff_u_bpcce_valuation_selected_power_product = ff_q_bpcce_valuation_selected_power_product_partial * S ((S (ff_i_bpcce_valuation_selected_power_product)) * ff_v_bpcce_valuation_selected_power_product) + (ff_r_bpcce_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_valuation_selected_power_product_successor. ff_h_bpcce_valuation_selected_power_product_successor + S (ff_s_bpcce_valuation_selected_power_product) = S ((S (S ff_i_bpcce_valuation_selected_power_product)) * ff_v_bpcce_valuation_selected_power_product)) /\ exists ff_q_bpcce_valuation_selected_power_product_successor. ff_u_bpcce_valuation_selected_power_product = ff_q_bpcce_valuation_selected_power_product_successor * S ((S (S ff_i_bpcce_valuation_selected_power_product)) * ff_v_bpcce_valuation_selected_power_product) + (ff_s_bpcce_valuation_selected_power_product))) /\ ff_s_bpcce_valuation_selected_power_product = ff_r_bpcce_valuation_selected_power_product * ff_p_bpcce_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_valuation_selected_divides. n = (bpr_power_value_bpcce_valuation_selected) * bpr_divides_quotient_bpcce_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcce_valuation. (exists bpr_le_gap_bpcce_valuation_candidate_bound. bpr_le_gap_bpcce_valuation_candidate_bound + (bpr_valuation_candidate_bpcce_valuation) = (n)) -> (exists bpr_power_value_bpcce_valuation_candidate. ((exists bpr_power_code_bpcce_valuation_candidate_power bpr_power_scale_bpcce_valuation_candidate_power. ((forall bpr_power_index_bpcce_valuation_candidate_power. (exists bpr_gap_bpcce_valuation_candidate_power_repeat_bound. bpr_gap_bpcce_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcce_valuation_candidate_power) = bpr_valuation_candidate_bpcce_valuation) -> (((exists bpr_height_bpcce_valuation_candidate_power_repeat_entry. bpr_height_bpcce_valuation_candidate_power_repeat_entry + S (S i) = S ((S (bpr_power_index_bpcce_valuation_candidate_power)) * bpr_power_scale_bpcce_valuation_candidate_power)) /\ exists bpr_quotient_bpcce_valuation_candidate_power_repeat_entry. bpr_power_code_bpcce_valuation_candidate_power = bpr_quotient_bpcce_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcce_valuation_candidate_power)) * bpr_power_scale_bpcce_valuation_candidate_power) + (S i)))) /\ (exists ff_u_bpcce_valuation_candidate_power_product ff_v_bpcce_valuation_candidate_power_product. ((((exists ff_h_bpcce_valuation_candidate_power_product_start. ff_h_bpcce_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_valuation_candidate_power_product)) /\ exists ff_q_bpcce_valuation_candidate_power_product_start. ff_u_bpcce_valuation_candidate_power_product = ff_q_bpcce_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcce_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcce_valuation_candidate_power_product_terminal. ff_h_bpcce_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcce_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcce_valuation)) * ff_v_bpcce_valuation_candidate_power_product)) /\ exists ff_q_bpcce_valuation_candidate_power_product_terminal. ff_u_bpcce_valuation_candidate_power_product = ff_q_bpcce_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcce_valuation)) * ff_v_bpcce_valuation_candidate_power_product) + (bpr_power_value_bpcce_valuation_candidate))) /\ forall ff_i_bpcce_valuation_candidate_power_product. (exists ff_lt_bpcce_valuation_candidate_power_product_bound. ff_lt_bpcce_valuation_candidate_power_product_bound + S ff_i_bpcce_valuation_candidate_power_product = bpr_valuation_candidate_bpcce_valuation) -> exists ff_p_bpcce_valuation_candidate_power_product ff_r_bpcce_valuation_candidate_power_product ff_s_bpcce_valuation_candidate_power_product. ((((exists ff_h_bpcce_valuation_candidate_power_product_factor. ff_h_bpcce_valuation_candidate_power_product_factor + S (ff_p_bpcce_valuation_candidate_power_product) = S ((S (ff_i_bpcce_valuation_candidate_power_product)) * bpr_power_scale_bpcce_valuation_candidate_power)) /\ exists ff_q_bpcce_valuation_candidate_power_product_factor. bpr_power_code_bpcce_valuation_candidate_power = ff_q_bpcce_valuation_candidate_power_product_factor * S ((S (ff_i_bpcce_valuation_candidate_power_product)) * bpr_power_scale_bpcce_valuation_candidate_power) + (ff_p_bpcce_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_valuation_candidate_power_product_partial. ff_h_bpcce_valuation_candidate_power_product_partial + S (ff_r_bpcce_valuation_candidate_power_product) = S ((S (ff_i_bpcce_valuation_candidate_power_product)) * ff_v_bpcce_valuation_candidate_power_product)) /\ exists ff_q_bpcce_valuation_candidate_power_product_partial. ff_u_bpcce_valuation_candidate_power_product = ff_q_bpcce_valuation_candidate_power_product_partial * S ((S (ff_i_bpcce_valuation_candidate_power_product)) * ff_v_bpcce_valuation_candidate_power_product) + (ff_r_bpcce_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_valuation_candidate_power_product_successor. ff_h_bpcce_valuation_candidate_power_product_successor + S (ff_s_bpcce_valuation_candidate_power_product) = S ((S (S ff_i_bpcce_valuation_candidate_power_product)) * ff_v_bpcce_valuation_candidate_power_product)) /\ exists ff_q_bpcce_valuation_candidate_power_product_successor. ff_u_bpcce_valuation_candidate_power_product = ff_q_bpcce_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcce_valuation_candidate_power_product)) * ff_v_bpcce_valuation_candidate_power_product) + (ff_s_bpcce_valuation_candidate_power_product))) /\ ff_s_bpcce_valuation_candidate_power_product = ff_r_bpcce_valuation_candidate_power_product * ff_p_bpcce_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_valuation_candidate_divides. n = (bpr_power_value_bpcce_valuation_candidate) * bpr_divides_quotient_bpcce_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcce_valuation_candidate_below. bpr_le_gap_bpcce_valuation_candidate_below + (bpr_valuation_candidate_bpcce_valuation) = (e)))
  6. 0006specialize power_valuation_exists (S i)
  7. 0007specialize power_valuation_exists n
  8. 0008exact power_valuation_exists
  9. 0009cases hvaluation
  10. 0010have hpower : ∃ a. Pow(S i,x,a)
    Exact native replay linehave hpower : exists a. (exists bpr_power_code_bpcce_power bpr_power_scale_bpcce_power. ((forall bpr_power_index_bpcce_power. (exists bpr_gap_bpcce_power_repeat_bound. bpr_gap_bpcce_power_repeat_bound + S (bpr_power_index_bpcce_power) = x) -> (((exists bpr_height_bpcce_power_repeat_entry. bpr_height_bpcce_power_repeat_entry + S (S i) = S ((S (bpr_power_index_bpcce_power)) * bpr_power_scale_bpcce_power)) /\ exists bpr_quotient_bpcce_power_repeat_entry. bpr_power_code_bpcce_power = bpr_quotient_bpcce_power_repeat_entry * S ((S (bpr_power_index_bpcce_power)) * bpr_power_scale_bpcce_power) + (S i)))) /\ (exists ff_u_bpcce_power_product ff_v_bpcce_power_product. ((((exists ff_h_bpcce_power_product_start. ff_h_bpcce_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_power_product)) /\ exists ff_q_bpcce_power_product_start. ff_u_bpcce_power_product = ff_q_bpcce_power_product_start * S ((S (0)) * ff_v_bpcce_power_product) + (1))) /\ ((((exists ff_h_bpcce_power_product_terminal. ff_h_bpcce_power_product_terminal + S (a) = S ((S (x)) * ff_v_bpcce_power_product)) /\ exists ff_q_bpcce_power_product_terminal. ff_u_bpcce_power_product = ff_q_bpcce_power_product_terminal * S ((S (x)) * ff_v_bpcce_power_product) + (a))) /\ forall ff_i_bpcce_power_product. (exists ff_lt_bpcce_power_product_bound. ff_lt_bpcce_power_product_bound + S ff_i_bpcce_power_product = x) -> exists ff_p_bpcce_power_product ff_r_bpcce_power_product ff_s_bpcce_power_product. ((((exists ff_h_bpcce_power_product_factor. ff_h_bpcce_power_product_factor + S (ff_p_bpcce_power_product) = S ((S (ff_i_bpcce_power_product)) * bpr_power_scale_bpcce_power)) /\ exists ff_q_bpcce_power_product_factor. bpr_power_code_bpcce_power = ff_q_bpcce_power_product_factor * S ((S (ff_i_bpcce_power_product)) * bpr_power_scale_bpcce_power) + (ff_p_bpcce_power_product))) /\ ((((exists ff_h_bpcce_power_product_partial. ff_h_bpcce_power_product_partial + S (ff_r_bpcce_power_product) = S ((S (ff_i_bpcce_power_product)) * ff_v_bpcce_power_product)) /\ exists ff_q_bpcce_power_product_partial. ff_u_bpcce_power_product = ff_q_bpcce_power_product_partial * S ((S (ff_i_bpcce_power_product)) * ff_v_bpcce_power_product) + (ff_r_bpcce_power_product))) /\ ((((exists ff_h_bpcce_power_product_successor. ff_h_bpcce_power_product_successor + S (ff_s_bpcce_power_product) = S ((S (S ff_i_bpcce_power_product)) * ff_v_bpcce_power_product)) /\ exists ff_q_bpcce_power_product_successor. ff_u_bpcce_power_product = ff_q_bpcce_power_product_successor * S ((S (S ff_i_bpcce_power_product)) * ff_v_bpcce_power_product) + (ff_s_bpcce_power_product))) /\ ff_s_bpcce_power_product = ff_r_bpcce_power_product * ff_p_bpcce_power_product))))))))
  11. 0011specialize pow_exists (S i)
  12. 0012specialize pow_exists x
  13. 0013exact pow_exists
  14. 0014cases hpower
  15. 0015exists x1
  16. 0016left
  17. 0017split
  18. 0018exact prime_decidable_left
  19. 0019exists x
  20. 0020split
  21. 0021exact hvaluation_witness
  22. 0022exact hpower_witness
  23. 0023exists 1
  24. 0024right
  25. 0025split
  26. 0026exact prime_decidable_right
  27. 0027refl