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 → Dvd(a,n)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
5 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall n i a. (((((~(S (i) = 1) /\ forall bpr_left_bpcfd_choice_prime bpr_right_bpcfd_choice_prime. S (i) = bpr_left_bpcfd_choice_prime * bpr_right_bpcfd_choice_prime -> bpr_left_bpcfd_choice_prime = 1 \/ bpr_right_bpcfd_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcfd_choice. ((((exists bpr_le_gap_bpcfd_choice_valuation_selected_bound. bpr_le_gap_bpcfd_choice_valuation_selected_bound + (bpr_choice_exponent_bpcfd_choice) = (n)) /\ (exists bpr_power_value_bpcfd_choice_valuation_selected. ((exists bpr_power_code_bpcfd_choice_valuation_selected_power bpr_power_scale_bpcfd_choice_valuation_selected_power. ((forall bpr_power_index_bpcfd_choice_valuation_selected_power. (exists bpr_gap_bpcfd_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcfd_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcfd_choice_valuation_selected_power) = bpr_choice_exponent_bpcfd_choice) -> (((exists bpr_height_bpcfd_choice_valuation_selected_power_repeat_entry. bpr_height_bpcfd_choice_valuation_selected_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcfd_choice_valuation_selected_power)) * bpr_power_scale_bpcfd_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcfd_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcfd_choice_valuation_selected_power = bpr_quotient_bpcfd_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcfd_choice_valuation_selected_power)) * bpr_power_scale_bpcfd_choice_valuation_selected_power) + (S (i))))) /\ (exists ff_u_bpcfd_choice_valuation_selected_power_product ff_v_bpcfd_choice_valuation_selected_power_product. ((((exists ff_h_bpcfd_choice_valuation_selected_power_product_start. ff_h_bpcfd_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcfd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcfd_choice_valuation_selected_power_product_start. ff_u_bpcfd_choice_valuation_selected_power_product = ff_q_bpcfd_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcfd_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcfd_choice_valuation_selected_power_product_terminal. ff_h_bpcfd_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcfd_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcfd_choice)) * ff_v_bpcfd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcfd_choice_valuation_selected_power_product_terminal. ff_u_bpcfd_choice_valuation_selected_power_product = ff_q_bpcfd_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcfd_choice)) * ff_v_bpcfd_choice_valuation_selected_power_product) + (bpr_power_value_bpcfd_choice_valuation_selected))) /\ forall ff_i_bpcfd_choice_valuation_selected_power_product. (exists ff_lt_bpcfd_choice_valuation_selected_power_product_bound. ff_lt_bpcfd_choice_valuation_selected_power_product_bound + S ff_i_bpcfd_choice_valuation_selected_power_product = bpr_choice_exponent_bpcfd_choice) -> exists ff_p_bpcfd_choice_valuation_selected_power_product ff_r_bpcfd_choice_valuation_selected_power_product ff_s_bpcfd_choice_valuation_selected_power_product. ((((exists ff_h_bpcfd_choice_valuation_selected_power_product_factor. ff_h_bpcfd_choice_valuation_selected_power_product_factor + S (ff_p_bpcfd_choice_valuation_selected_power_product) = S ((S (ff_i_bpcfd_choice_valuation_selected_power_product)) * bpr_power_scale_bpcfd_choice_valuation_selected_power)) /\ exists ff_q_bpcfd_choice_valuation_selected_power_product_factor. bpr_power_code_bpcfd_choice_valuation_selected_power = ff_q_bpcfd_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcfd_choice_valuation_selected_power_product)) * bpr_power_scale_bpcfd_choice_valuation_selected_power) + (ff_p_bpcfd_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcfd_choice_valuation_selected_power_product_partial. ff_h_bpcfd_choice_valuation_selected_power_product_partial + S (ff_r_bpcfd_choice_valuation_selected_power_product) = S ((S (ff_i_bpcfd_choice_valuation_selected_power_product)) * ff_v_bpcfd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcfd_choice_valuation_selected_power_product_partial. ff_u_bpcfd_choice_valuation_selected_power_product = ff_q_bpcfd_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcfd_choice_valuation_selected_power_product)) * ff_v_bpcfd_choice_valuation_selected_power_product) + (ff_r_bpcfd_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcfd_choice_valuation_selected_power_product_successor. ff_h_bpcfd_choice_valuation_selected_power_product_successor + S (ff_s_bpcfd_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcfd_choice_valuation_selected_power_product)) * ff_v_bpcfd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcfd_choice_valuation_selected_power_product_successor. ff_u_bpcfd_choice_valuation_selected_power_product = ff_q_bpcfd_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcfd_choice_valuation_selected_power_product)) * ff_v_bpcfd_choice_valuation_selected_power_product) + (ff_s_bpcfd_choice_valuation_selected_power_product))) /\ ff_s_bpcfd_choice_valuation_selected_power_product = ff_r_bpcfd_choice_valuation_selected_power_product * ff_p_bpcfd_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcfd_choice_valuation_selected_divides. n = (bpr_power_value_bpcfd_choice_valuation_selected) * bpr_divides_quotient_bpcfd_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcfd_choice_valuation. (exists bpr_le_gap_bpcfd_choice_valuation_candidate_bound. bpr_le_gap_bpcfd_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcfd_choice_valuation) = (n)) -> (exists bpr_power_value_bpcfd_choice_valuation_candidate. ((exists bpr_power_code_bpcfd_choice_valuation_candidate_power bpr_power_scale_bpcfd_choice_valuation_candidate_power. ((forall bpr_power_index_bpcfd_choice_valuation_candidate_power. (exists bpr_gap_bpcfd_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcfd_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcfd_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcfd_choice_valuation) -> (((exists bpr_height_bpcfd_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcfd_choice_valuation_candidate_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcfd_choice_valuation_candidate_power)) * bpr_power_scale_bpcfd_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcfd_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcfd_choice_valuation_candidate_power = bpr_quotient_bpcfd_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcfd_choice_valuation_candidate_power)) * bpr_power_scale_bpcfd_choice_valuation_candidate_power) + (S (i))))) /\ (exists ff_u_bpcfd_choice_valuation_candidate_power_product ff_v_bpcfd_choice_valuation_candidate_power_product. ((((exists ff_h_bpcfd_choice_valuation_candidate_power_product_start. ff_h_bpcfd_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcfd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcfd_choice_valuation_candidate_power_product_start. ff_u_bpcfd_choice_valuation_candidate_power_product = ff_q_bpcfd_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcfd_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcfd_choice_valuation_candidate_power_product_terminal. ff_h_bpcfd_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcfd_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcfd_choice_valuation)) * ff_v_bpcfd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcfd_choice_valuation_candidate_power_product_terminal. ff_u_bpcfd_choice_valuation_candidate_power_product = ff_q_bpcfd_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcfd_choice_valuation)) * ff_v_bpcfd_choice_valuation_candidate_power_product) + (bpr_power_value_bpcfd_choice_valuation_candidate))) /\ forall ff_i_bpcfd_choice_valuation_candidate_power_product. (exists ff_lt_bpcfd_choice_valuation_candidate_power_product_bound. ff_lt_bpcfd_choice_valuation_candidate_power_product_bound + S ff_i_bpcfd_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcfd_choice_valuation) -> exists ff_p_bpcfd_choice_valuation_candidate_power_product ff_r_bpcfd_choice_valuation_candidate_power_product ff_s_bpcfd_choice_valuation_candidate_power_product. ((((exists ff_h_bpcfd_choice_valuation_candidate_power_product_factor. ff_h_bpcfd_choice_valuation_candidate_power_product_factor + S (ff_p_bpcfd_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcfd_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcfd_choice_valuation_candidate_power)) /\ exists ff_q_bpcfd_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcfd_choice_valuation_candidate_power = ff_q_bpcfd_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcfd_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcfd_choice_valuation_candidate_power) + (ff_p_bpcfd_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcfd_choice_valuation_candidate_power_product_partial. ff_h_bpcfd_choice_valuation_candidate_power_product_partial + S (ff_r_bpcfd_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcfd_choice_valuation_candidate_power_product)) * ff_v_bpcfd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcfd_choice_valuation_candidate_power_product_partial. ff_u_bpcfd_choice_valuation_candidate_power_product = ff_q_bpcfd_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcfd_choice_valuation_candidate_power_product)) * ff_v_bpcfd_choice_valuation_candidate_power_product) + (ff_r_bpcfd_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcfd_choice_valuation_candidate_power_product_successor. ff_h_bpcfd_choice_valuation_candidate_power_product_successor + S (ff_s_bpcfd_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcfd_choice_valuation_candidate_power_product)) * ff_v_bpcfd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcfd_choice_valuation_candidate_power_product_successor. ff_u_bpcfd_choice_valuation_candidate_power_product = ff_q_bpcfd_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcfd_choice_valuation_candidate_power_product)) * ff_v_bpcfd_choice_valuation_candidate_power_product) + (ff_s_bpcfd_choice_valuation_candidate_power_product))) /\ ff_s_bpcfd_choice_valuation_candidate_power_product = ff_r_bpcfd_choice_valuation_candidate_power_product * ff_p_bpcfd_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcfd_choice_valuation_candidate_divides. n = (bpr_power_value_bpcfd_choice_valuation_candidate) * bpr_divides_quotient_bpcfd_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcfd_choice_valuation_candidate_below. bpr_le_gap_bpcfd_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcfd_choice_valuation) = (bpr_choice_exponent_bpcfd_choice))) /\ (exists bpr_power_code_bpcfd_choice_power bpr_power_scale_bpcfd_choice_power. ((forall bpr_power_index_bpcfd_choice_power. (exists bpr_gap_bpcfd_choice_power_repeat_bound. bpr_gap_bpcfd_choice_power_repeat_bound + S (bpr_power_index_bpcfd_choice_power) = bpr_choice_exponent_bpcfd_choice) -> (((exists bpr_height_bpcfd_choice_power_repeat_entry. bpr_height_bpcfd_choice_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcfd_choice_power)) * bpr_power_scale_bpcfd_choice_power)) /\ exists bpr_quotient_bpcfd_choice_power_repeat_entry. bpr_power_code_bpcfd_choice_power = bpr_quotient_bpcfd_choice_power_repeat_entry * S ((S (bpr_power_index_bpcfd_choice_power)) * bpr_power_scale_bpcfd_choice_power) + (S (i))))) /\ (exists ff_u_bpcfd_choice_power_product ff_v_bpcfd_choice_power_product. ((((exists ff_h_bpcfd_choice_power_product_start. ff_h_bpcfd_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcfd_choice_power_product)) /\ exists ff_q_bpcfd_choice_power_product_start. ff_u_bpcfd_choice_power_product = ff_q_bpcfd_choice_power_product_start * S ((S (0)) * ff_v_bpcfd_choice_power_product) + (1))) /\ ((((exists ff_h_bpcfd_choice_power_product_terminal. ff_h_bpcfd_choice_power_product_terminal + S (a) = S ((S (bpr_choice_exponent_bpcfd_choice)) * ff_v_bpcfd_choice_power_product)) /\ exists ff_q_bpcfd_choice_power_product_terminal. ff_u_bpcfd_choice_power_product = ff_q_bpcfd_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcfd_choice)) * ff_v_bpcfd_choice_power_product) + (a))) /\ forall ff_i_bpcfd_choice_power_product. (exists ff_lt_bpcfd_choice_power_product_bound. ff_lt_bpcfd_choice_power_product_bound + S ff_i_bpcfd_choice_power_product = bpr_choice_exponent_bpcfd_choice) -> exists ff_p_bpcfd_choice_power_product ff_r_bpcfd_choice_power_product ff_s_bpcfd_choice_power_product. ((((exists ff_h_bpcfd_choice_power_product_factor. ff_h_bpcfd_choice_power_product_factor + S (ff_p_bpcfd_choice_power_product) = S ((S (ff_i_bpcfd_choice_power_product)) * bpr_power_scale_bpcfd_choice_power)) /\ exists ff_q_bpcfd_choice_power_product_factor. bpr_power_code_bpcfd_choice_power = ff_q_bpcfd_choice_power_product_factor * S ((S (ff_i_bpcfd_choice_power_product)) * bpr_power_scale_bpcfd_choice_power) + (ff_p_bpcfd_choice_power_product))) /\ ((((exists ff_h_bpcfd_choice_power_product_partial. ff_h_bpcfd_choice_power_product_partial + S (ff_r_bpcfd_choice_power_product) = S ((S (ff_i_bpcfd_choice_power_product)) * ff_v_bpcfd_choice_power_product)) /\ exists ff_q_bpcfd_choice_power_product_partial. ff_u_bpcfd_choice_power_product = ff_q_bpcfd_choice_power_product_partial * S ((S (ff_i_bpcfd_choice_power_product)) * ff_v_bpcfd_choice_power_product) + (ff_r_bpcfd_choice_power_product))) /\ ((((exists ff_h_bpcfd_choice_power_product_successor. ff_h_bpcfd_choice_power_product_successor + S (ff_s_bpcfd_choice_power_product) = S ((S (S ff_i_bpcfd_choice_power_product)) * ff_v_bpcfd_choice_power_product)) /\ exists ff_q_bpcfd_choice_power_product_successor. ff_u_bpcfd_choice_power_product = ff_q_bpcfd_choice_power_product_successor * S ((S (S ff_i_bpcfd_choice_power_product)) * ff_v_bpcfd_choice_power_product) + (ff_s_bpcfd_choice_power_product))) /\ ff_s_bpcfd_choice_power_product = ff_r_bpcfd_choice_power_product * ff_p_bpcfd_choice_power_product)))))))))) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpcfd_choice_prime bpr_right_bpcfd_choice_prime. S (i) = bpr_left_bpcfd_choice_prime * bpr_right_bpcfd_choice_prime -> bpr_left_bpcfd_choice_prime = 1 \/ bpr_right_bpcfd_choice_prime = 1)) /\ a = 1))) -> (exists bpr_divides_quotient_bpcfd_result. n = (a) * bpr_divides_quotient_bpcfd_result)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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.
Named ingredients (3)
01Fix variables and assumptionsL1–4
02Separate the logical casesL5–8
03Establish hselectedL9–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation power divides.
- L9
have hselected : PowerDivides(S i,x,n)Definitions: PowerDivides(S i,x,n)Original native command in the exact edition - L10
specialize power_valuation_power_divides (S i) - L11
specialize power_valuation_power_divides n - L12
specialize power_valuation_power_divides x - L13
apply power_valuation_power_divides - L14
exact hchoice_left_right_witness_left
04Separate the logical casesL15–17
05Establish hvalueL18–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow functional.
06Construct an explicit witnessL26–26
Supply the displayed value, then prove that it has the required property.
- L26
exists x2
07Calculate and transport equalitiesL27–27
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L27
rewrite <- hvalue
08Use earlier factsL28–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
exact hselected_witness_right_witness
09Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
cases hchoice_right
10Calculate and transport equalitiesL30–30
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L30
rewrite hchoice_right_right
11Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
apply one_multiple
Original defined command ledger · 31 lines
- 0001
intro n - 0002
intro i - 0003
intro a - 0004
intro hchoice - 0005
cases hchoice - 0006
cases hchoice_left - 0007
cases hchoice_left_right - 0008
cases hchoice_left_right_witness - 0009
have hselected : PowerDivides(S i,x,n)Exact native replay line
have hselected : exists bpr_power_value_bpcfd_selected. ((exists bpr_power_code_bpcfd_selected_power bpr_power_scale_bpcfd_selected_power. ((forall bpr_power_index_bpcfd_selected_power. (exists bpr_gap_bpcfd_selected_power_repeat_bound. bpr_gap_bpcfd_selected_power_repeat_bound + S (bpr_power_index_bpcfd_selected_power) = x) -> (((exists bpr_height_bpcfd_selected_power_repeat_entry. bpr_height_bpcfd_selected_power_repeat_entry + S (S i) = S ((S (bpr_power_index_bpcfd_selected_power)) * bpr_power_scale_bpcfd_selected_power)) /\ exists bpr_quotient_bpcfd_selected_power_repeat_entry. bpr_power_code_bpcfd_selected_power = bpr_quotient_bpcfd_selected_power_repeat_entry * S ((S (bpr_power_index_bpcfd_selected_power)) * bpr_power_scale_bpcfd_selected_power) + (S i)))) /\ (exists ff_u_bpcfd_selected_power_product ff_v_bpcfd_selected_power_product. ((((exists ff_h_bpcfd_selected_power_product_start. ff_h_bpcfd_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcfd_selected_power_product)) /\ exists ff_q_bpcfd_selected_power_product_start. ff_u_bpcfd_selected_power_product = ff_q_bpcfd_selected_power_product_start * S ((S (0)) * ff_v_bpcfd_selected_power_product) + (1))) /\ ((((exists ff_h_bpcfd_selected_power_product_terminal. ff_h_bpcfd_selected_power_product_terminal + S (bpr_power_value_bpcfd_selected) = S ((S (x)) * ff_v_bpcfd_selected_power_product)) /\ exists ff_q_bpcfd_selected_power_product_terminal. ff_u_bpcfd_selected_power_product = ff_q_bpcfd_selected_power_product_terminal * S ((S (x)) * ff_v_bpcfd_selected_power_product) + (bpr_power_value_bpcfd_selected))) /\ forall ff_i_bpcfd_selected_power_product. (exists ff_lt_bpcfd_selected_power_product_bound. ff_lt_bpcfd_selected_power_product_bound + S ff_i_bpcfd_selected_power_product = x) -> exists ff_p_bpcfd_selected_power_product ff_r_bpcfd_selected_power_product ff_s_bpcfd_selected_power_product. ((((exists ff_h_bpcfd_selected_power_product_factor. ff_h_bpcfd_selected_power_product_factor + S (ff_p_bpcfd_selected_power_product) = S ((S (ff_i_bpcfd_selected_power_product)) * bpr_power_scale_bpcfd_selected_power)) /\ exists ff_q_bpcfd_selected_power_product_factor. bpr_power_code_bpcfd_selected_power = ff_q_bpcfd_selected_power_product_factor * S ((S (ff_i_bpcfd_selected_power_product)) * bpr_power_scale_bpcfd_selected_power) + (ff_p_bpcfd_selected_power_product))) /\ ((((exists ff_h_bpcfd_selected_power_product_partial. ff_h_bpcfd_selected_power_product_partial + S (ff_r_bpcfd_selected_power_product) = S ((S (ff_i_bpcfd_selected_power_product)) * ff_v_bpcfd_selected_power_product)) /\ exists ff_q_bpcfd_selected_power_product_partial. ff_u_bpcfd_selected_power_product = ff_q_bpcfd_selected_power_product_partial * S ((S (ff_i_bpcfd_selected_power_product)) * ff_v_bpcfd_selected_power_product) + (ff_r_bpcfd_selected_power_product))) /\ ((((exists ff_h_bpcfd_selected_power_product_successor. ff_h_bpcfd_selected_power_product_successor + S (ff_s_bpcfd_selected_power_product) = S ((S (S ff_i_bpcfd_selected_power_product)) * ff_v_bpcfd_selected_power_product)) /\ exists ff_q_bpcfd_selected_power_product_successor. ff_u_bpcfd_selected_power_product = ff_q_bpcfd_selected_power_product_successor * S ((S (S ff_i_bpcfd_selected_power_product)) * ff_v_bpcfd_selected_power_product) + (ff_s_bpcfd_selected_power_product))) /\ ff_s_bpcfd_selected_power_product = ff_r_bpcfd_selected_power_product * ff_p_bpcfd_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcfd_selected_divides. n = (bpr_power_value_bpcfd_selected) * bpr_divides_quotient_bpcfd_selected_divides)) - 0010
specialize power_valuation_power_divides (S i) - 0011
specialize power_valuation_power_divides n - 0012
specialize power_valuation_power_divides x - 0013
apply power_valuation_power_divides - 0014
exact hchoice_left_right_witness_left - 0015
cases hselected - 0016
cases hselected_witness - 0017
cases hselected_witness_right - 0018
have hvalue : x1 = a - 0019
specialize pow_functional (S i) - 0020
specialize pow_functional x - 0021
specialize pow_functional x1 - 0022
specialize pow_functional a - 0023
apply pow_functional - 0024
exact hselected_witness_left - 0025
exact hchoice_left_right_witness_right - 0026
exists x2 - 0027
rewrite <- hvalue - 0028
exact hselected_witness_right_witness - 0029
cases hchoice_right - 0030
rewrite hchoice_right_right - 0031
apply one_multiple