BT0114

central_binom_le_of_no_bertrand_prime

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

No Bertrand prime forces the reviewed central-binomial upper bound.

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.

Exact expanded PA statement

forall n s q r C A B. (forall bpr_prime_candidate_b5cblonbp_exclusion. ((exists bpr_gap_b5cblonbp_exclusion_lower. bpr_gap_b5cblonbp_exclusion_lower + S (n) = bpr_prime_candidate_b5cblonbp_exclusion) /\ (exists bpr_le_gap_b5cblonbp_exclusion_upper. bpr_le_gap_b5cblonbp_exclusion_upper + (bpr_prime_candidate_b5cblonbp_exclusion) = (n + n))) -> ~((~(bpr_prime_candidate_b5cblonbp_exclusion = 1) /\ forall bpr_left_b5cblonbp_exclusion_prime bpr_right_b5cblonbp_exclusion_prime. bpr_prime_candidate_b5cblonbp_exclusion = bpr_left_b5cblonbp_exclusion_prime * bpr_right_b5cblonbp_exclusion_prime -> bpr_left_b5cblonbp_exclusion_prime = 1 \/ bpr_right_b5cblonbp_exclusion_prime = 1))) -> (exists bcf_lt_gap_b5cblonbp_positive. bcf_lt_gap_b5cblonbp_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5cblonbp_floor. bcs_sqrt_lower_gap_b5cblonbp_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5cblonbp_floor. bcs_sqrt_upper_gap_b5cblonbp_floor + S (n + n) = S (s) * S (s))) -> (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5cblonbp_division_bound. bcf_lt_gap_b5cblonbp_division_bound + S (r) = 3))) -> (((exists bcf_lt_gap_b5cblonbp_central_out_of_range. bcf_lt_gap_b5cblonbp_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_b5cblonbp_central_in_range. bcf_le_gap_b5cblonbp_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_b5cblonbp_central bcf_row_code_scale_b5cblonbp_central bcf_row_scale_code_b5cblonbp_central bcf_row_scale_scale_b5cblonbp_central bcf_row_code_b5cblonbp_central bcf_row_scale_b5cblonbp_central. ((forall bcf_row_index_b5cblonbp_central_table. (exists bcf_lt_gap_b5cblonbp_central_table_row_bound. bcf_lt_gap_b5cblonbp_central_table_row_bound + S (bcf_row_index_b5cblonbp_central_table) = S (n + n)) -> exists bcf_row_code_b5cblonbp_central_table bcf_row_scale_b5cblonbp_central_table. ((((exists bcf_height_b5cblonbp_central_table_decoded_row_code. bcf_height_b5cblonbp_central_table_decoded_row_code + S (bcf_row_code_b5cblonbp_central_table) = S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_row_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_row_code * S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_row_code_b5cblonbp_central_table))) /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_row_scale. bcf_height_b5cblonbp_central_table_decoded_row_scale + S (bcf_row_scale_b5cblonbp_central_table) = S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_row_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_row_scale * S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_row_scale_b5cblonbp_central_table))) /\ ((bcf_row_index_b5cblonbp_central_table = 0 /\ (forall bcf_index_b5cblonbp_central_table_zero_row. (exists bcf_lt_gap_b5cblonbp_central_table_zero_row_bound. bcf_lt_gap_b5cblonbp_central_table_zero_row_bound + S (bcf_index_b5cblonbp_central_table_zero_row) = S (n + n)) -> exists bcf_value_b5cblonbp_central_table_zero_row. ((((exists bcf_height_b5cblonbp_central_table_zero_row_entry. bcf_height_b5cblonbp_central_table_zero_row_entry + S (bcf_value_b5cblonbp_central_table_zero_row) = S ((S (bcf_index_b5cblonbp_central_table_zero_row)) * bcf_row_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_zero_row_entry. bcf_row_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_zero_row_entry * S ((S (bcf_index_b5cblonbp_central_table_zero_row)) * bcf_row_scale_b5cblonbp_central_table) + (bcf_value_b5cblonbp_central_table_zero_row))) /\ ((bcf_index_b5cblonbp_central_table_zero_row = 0 /\ bcf_value_b5cblonbp_central_table_zero_row = 1) \/ exists bcf_predecessor_b5cblonbp_central_table_zero_row. bcf_index_b5cblonbp_central_table_zero_row = S bcf_predecessor_b5cblonbp_central_table_zero_row /\ bcf_value_b5cblonbp_central_table_zero_row = 0)))) \/ exists bcf_predecessor_b5cblonbp_central_table bcf_previous_code_b5cblonbp_central_table bcf_previous_scale_b5cblonbp_central_table. bcf_row_index_b5cblonbp_central_table = S bcf_predecessor_b5cblonbp_central_table /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_previous_code. bcf_height_b5cblonbp_central_table_decoded_previous_code + S (bcf_previous_code_b5cblonbp_central_table) = S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_previous_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_previous_code * S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_previous_code_b5cblonbp_central_table))) /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_previous_scale. bcf_height_b5cblonbp_central_table_decoded_previous_scale + S (bcf_previous_scale_b5cblonbp_central_table) = S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_previous_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_previous_scale * S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_previous_scale_b5cblonbp_central_table))) /\ (forall bcf_index_b5cblonbp_central_table_row_step. (exists bcf_lt_gap_b5cblonbp_central_table_row_step_bound. bcf_lt_gap_b5cblonbp_central_table_row_step_bound + S (bcf_index_b5cblonbp_central_table_row_step) = S (n + n)) -> exists bcf_value_b5cblonbp_central_table_row_step. ((((exists bcf_height_b5cblonbp_central_table_row_step_entry. bcf_height_b5cblonbp_central_table_row_step_entry + S (bcf_value_b5cblonbp_central_table_row_step) = S ((S (bcf_index_b5cblonbp_central_table_row_step)) * bcf_row_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_entry. bcf_row_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_entry * S ((S (bcf_index_b5cblonbp_central_table_row_step)) * bcf_row_scale_b5cblonbp_central_table) + (bcf_value_b5cblonbp_central_table_row_step))) /\ ((bcf_index_b5cblonbp_central_table_row_step = 0 /\ bcf_value_b5cblonbp_central_table_row_step = 1) \/ exists bcf_predecessor_b5cblonbp_central_table_row_step bcf_left_b5cblonbp_central_table_row_step bcf_right_b5cblonbp_central_table_row_step. bcf_index_b5cblonbp_central_table_row_step = S bcf_predecessor_b5cblonbp_central_table_row_step /\ ((((exists bcf_height_b5cblonbp_central_table_row_step_previous_left. bcf_height_b5cblonbp_central_table_row_step_previous_left + S (bcf_left_b5cblonbp_central_table_row_step) = S ((S (bcf_predecessor_b5cblonbp_central_table_row_step)) * bcf_previous_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_previous_left. bcf_previous_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_previous_left * S ((S (bcf_predecessor_b5cblonbp_central_table_row_step)) * bcf_previous_scale_b5cblonbp_central_table) + (bcf_left_b5cblonbp_central_table_row_step))) /\ ((((exists bcf_height_b5cblonbp_central_table_row_step_previous_right. bcf_height_b5cblonbp_central_table_row_step_previous_right + S (bcf_right_b5cblonbp_central_table_row_step) = S ((S (S (bcf_predecessor_b5cblonbp_central_table_row_step))) * bcf_previous_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_previous_right. bcf_previous_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_b5cblonbp_central_table_row_step))) * bcf_previous_scale_b5cblonbp_central_table) + (bcf_right_b5cblonbp_central_table_row_step))) /\ bcf_value_b5cblonbp_central_table_row_step = bcf_left_b5cblonbp_central_table_row_step + bcf_right_b5cblonbp_central_table_row_step))))))))))) /\ ((((exists bcf_height_b5cblonbp_central_decoded_row_code. bcf_height_b5cblonbp_central_decoded_row_code + S (bcf_row_code_b5cblonbp_central) = S ((S (n + n)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_row_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_row_code_b5cblonbp_central))) /\ ((((exists bcf_height_b5cblonbp_central_decoded_row_scale. bcf_height_b5cblonbp_central_decoded_row_scale + S (bcf_row_scale_b5cblonbp_central) = S ((S (n + n)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_row_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_row_scale_b5cblonbp_central))) /\ (((exists bcf_height_b5cblonbp_central_decoded_value. bcf_height_b5cblonbp_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_value. bcf_row_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_value * S ((S (n)) * bcf_row_scale_b5cblonbp_central) + (C))))))))) -> (exists bpvi_b_b5cblonbp_power_a bpvi_c_b5cblonbp_power_a. ((forall bpvi_i_b5cblonbp_power_a. (exists bpvi_repeat_gap_b5cblonbp_power_a. bpvi_repeat_gap_b5cblonbp_power_a + S bpvi_i_b5cblonbp_power_a = s) -> (((exists bpvi_h_b5cblonbp_power_a_repeat. bpvi_h_b5cblonbp_power_a_repeat + S (n + n) = S ((S (bpvi_i_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_repeat. bpvi_b_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_repeat * S ((S (bpvi_i_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a) + (n + n)))) /\ (exists bpvi_u_b5cblonbp_power_a bpvi_v_b5cblonbp_power_a. ((((exists bpvi_h_b5cblonbp_power_a_start. bpvi_h_b5cblonbp_power_a_start + S (1) = S ((S (0)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_start. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_start * S ((S (0)) * bpvi_v_b5cblonbp_power_a) + (1))) /\ ((((exists bpvi_h_b5cblonbp_power_a_terminal. bpvi_h_b5cblonbp_power_a_terminal + S (A) = S ((S (s)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_terminal. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_terminal * S ((S (s)) * bpvi_v_b5cblonbp_power_a) + (A))) /\ forall bpvi_j_b5cblonbp_power_a. (exists bpvi_product_gap_b5cblonbp_power_a. bpvi_product_gap_b5cblonbp_power_a + S bpvi_j_b5cblonbp_power_a = s) -> exists bpvi_factor_b5cblonbp_power_a bpvi_partial_b5cblonbp_power_a bpvi_successor_b5cblonbp_power_a. ((((exists bpvi_h_b5cblonbp_power_a_factor. bpvi_h_b5cblonbp_power_a_factor + S (bpvi_factor_b5cblonbp_power_a) = S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_factor. bpvi_b_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_factor * S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a) + (bpvi_factor_b5cblonbp_power_a))) /\ ((((exists bpvi_h_b5cblonbp_power_a_partial. bpvi_h_b5cblonbp_power_a_partial + S (bpvi_partial_b5cblonbp_power_a) = S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_partial. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_partial * S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a) + (bpvi_partial_b5cblonbp_power_a))) /\ ((((exists bpvi_h_b5cblonbp_power_a_successor. bpvi_h_b5cblonbp_power_a_successor + S (bpvi_successor_b5cblonbp_power_a) = S ((S (S bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_successor. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_successor * S ((S (S bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a) + (bpvi_successor_b5cblonbp_power_a))) /\ bpvi_successor_b5cblonbp_power_a = bpvi_partial_b5cblonbp_power_a * bpvi_factor_b5cblonbp_power_a)))))))) -> (exists bpvi_b_b5cblonbp_power_b bpvi_c_b5cblonbp_power_b. ((forall bpvi_i_b5cblonbp_power_b. (exists bpvi_repeat_gap_b5cblonbp_power_b. bpvi_repeat_gap_b5cblonbp_power_b + S bpvi_i_b5cblonbp_power_b = q) -> (((exists bpvi_h_b5cblonbp_power_b_repeat. bpvi_h_b5cblonbp_power_b_repeat + S (4) = S ((S (bpvi_i_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_repeat. bpvi_b_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_repeat * S ((S (bpvi_i_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b) + (4)))) /\ (exists bpvi_u_b5cblonbp_power_b bpvi_v_b5cblonbp_power_b. ((((exists bpvi_h_b5cblonbp_power_b_start. bpvi_h_b5cblonbp_power_b_start + S (1) = S ((S (0)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_start. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_start * S ((S (0)) * bpvi_v_b5cblonbp_power_b) + (1))) /\ ((((exists bpvi_h_b5cblonbp_power_b_terminal. bpvi_h_b5cblonbp_power_b_terminal + S (B) = S ((S (q)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_terminal. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_terminal * S ((S (q)) * bpvi_v_b5cblonbp_power_b) + (B))) /\ forall bpvi_j_b5cblonbp_power_b. (exists bpvi_product_gap_b5cblonbp_power_b. bpvi_product_gap_b5cblonbp_power_b + S bpvi_j_b5cblonbp_power_b = q) -> exists bpvi_factor_b5cblonbp_power_b bpvi_partial_b5cblonbp_power_b bpvi_successor_b5cblonbp_power_b. ((((exists bpvi_h_b5cblonbp_power_b_factor. bpvi_h_b5cblonbp_power_b_factor + S (bpvi_factor_b5cblonbp_power_b) = S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_factor. bpvi_b_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_factor * S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b) + (bpvi_factor_b5cblonbp_power_b))) /\ ((((exists bpvi_h_b5cblonbp_power_b_partial. bpvi_h_b5cblonbp_power_b_partial + S (bpvi_partial_b5cblonbp_power_b) = S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_partial. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_partial * S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b) + (bpvi_partial_b5cblonbp_power_b))) /\ ((((exists bpvi_h_b5cblonbp_power_b_successor. bpvi_h_b5cblonbp_power_b_successor + S (bpvi_successor_b5cblonbp_power_b) = S ((S (S bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_successor. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_successor * S ((S (S bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b) + (bpvi_successor_b5cblonbp_power_b))) /\ bpvi_successor_b5cblonbp_power_b = bpvi_partial_b5cblonbp_power_b * bpvi_factor_b5cblonbp_power_b)))))))) -> (exists bcf_le_gap_b5cblonbp_result. bcf_le_gap_b5cblonbp_result + (C) = A * B)

Structural proof guide

No Bertrand prime forces the reviewed central-binomial upper bound.

Direct prerequisites: mul_le_mul, floor_third_double_gap_package, central_binom_prime_contribution_product_exists, no_bertrand_small_contribution_product_le_power, no_bertrand_middle_contribution_interval_le_four_pow, central_binom_factorization_small. The authored body proceeds by case analysis (9), intermediate claims (6), equality transport (2).

Proof neighborhood

Direct dependencies

BT00PV mul_le_mul BT010J floor_third_double_gap_package BT0107 central_binom_prime_contribution_product_exists BT010Y no_bertrand_small_contribution_product_le_power BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0113 central_binom_factorization_small

Direct dependents

BT0115 bertrand_eventually_closed_upper

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

100 script commands · 15 reading checkpoints · 6 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.

Named ingredients (6)
mul le mulfloor third double gap packagecentral binom prime contribution product existsno bertrand small contribution product le powerno bertrand middle contribution interval le four powcentral binom factorization small

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro C
  6. L6
    intro A
  7. L7
    intro B
  8. L8
    intro hexclusion
  9. L9
    intro hpositive
  10. L10
    intro hfloor
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hdivision
  2. L12
    intro hcentral
  3. L13
    intro hpower_a
  4. L14
    intro hpower_b
03Establish hgapsL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor third double gap package.

  1. L15
    have hgaps : exists g h. s + g = q /\ q + h = n + n
  2. L16
    specialize floor_third_double_gap_package n
  3. L17
    specialize floor_third_double_gap_package s
  4. L18
    specialize floor_third_double_gap_package q
  5. L19
    specialize floor_third_double_gap_package r
  6. L20
    apply floor_third_double_gap_package
  7. L21
    exact hpositive
  8. L22
    exact hfloor
  9. L23
    exact hdivision
04Separate the logical casesL24–26

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

  1. L24
    cases hgaps
  2. L25
    cases hgaps_witness
  3. L26
    cases hgaps_witness_witness
05Establish hproductL27–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom prime contribution product exists.

  1. L27
    have hproduct : ∃ z. (∃ x. ∃ y. (∀ m. Lt(m,n + n) → ∃ k. BetaAt(x,y,m,k) ∧ (Prime(S m) ∧ (∃ i. BoundedPowerValuation(S m,C,C,i) ∧ Pow(S m,i,k)) ∨ ¬Prime(S m) ∧ k = 1)) ∧ Product(x,y,n + n,z)) ∧ C = zDefinitions: LtPrimeBetaAtProductPowBoundedPowerValuation
  2. L28
    specialize central_binom_prime_contribution_product_exists n
  3. L29
    specialize central_binom_prime_contribution_product_exists C
  4. L30
    apply central_binom_prime_contribution_product_exists
  5. L31
    exact hcentral
06Separate the logical casesL32–33

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

  1. L32
    cases hproduct
  2. L33
    cases hproduct_witness
07Establish hfactorizationL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom factorization small.

  1. L34
    have hfactorization : ∃ u. ∃ v. (∃ y. ∃ z. (∀ n. Lt(n,s) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S n) ∧ (∃ k. BoundedPowerValuation(S n,C,C,k) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(y,z,s,u)) ∧ ((∃ y. ∃ z. (∀ n. Lt(n,x) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S (s + n)) ∧ (∃ k. BoundedPowerValuation(S (s + n),C,C,k) ∧ Pow(S (s + n),k,m)) ∨ ¬Prime(S (s + n)) ∧ m = 1)) ∧ Product(y,z,x,v)) ∧ x2 = u · v)Definitions: LtPrimeBetaAtProductPowBoundedPowerValuation
  2. L35
    specialize central_binom_factorization_small n
  3. L36
    specialize central_binom_factorization_small s
  4. L37
    specialize central_binom_factorization_small q
  5. L38
    specialize central_binom_factorization_small r
  6. L39
    specialize central_binom_factorization_small C
  7. L40
    specialize central_binom_factorization_small x
  8. L41
    specialize central_binom_factorization_small x1
  9. L42
    specialize central_binom_factorization_small x2
  10. L43
    apply central_binom_factorization_small
08Use earlier factsL44–51

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

  1. L44
    exact hexclusion
  2. L45
    exact hpositive
  3. L46
    exact hfloor
  4. L47
    exact hdivision
  5. L48
    exact hcentral
  6. L49
    exact hgaps_witness_witness_left
  7. L50
    exact hgaps_witness_witness_right
  8. L51
    exact hproduct_witness_left
09Separate the logical casesL52–55

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

  1. L52
    cases hfactorization
  2. L53
    cases hfactorization_witness
  3. L54
    cases hfactorization_witness_witness
  4. L55
    cases hfactorization_witness_witness_right
10Establish hsmallL56–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply no bertrand small contribution product le power.

  1. L56
    have hsmall : exists bcf_le_gap_b5cblonbp_x_a. bcf_le_gap_b5cblonbp_x_a + (x3) = A
  2. L57
    specialize no_bertrand_small_contribution_product_le_power n
  3. L58
    specialize no_bertrand_small_contribution_product_le_power s
  4. L59
    specialize no_bertrand_small_contribution_product_le_power q
  5. L60
    specialize no_bertrand_small_contribution_product_le_power r
  6. L61
    specialize no_bertrand_small_contribution_product_le_power C
  7. L62
    specialize no_bertrand_small_contribution_product_le_power x3
  8. L63
    specialize no_bertrand_small_contribution_product_le_power A
  9. L64
    apply no_bertrand_small_contribution_product_le_power
  10. L65
    exact hexclusion
11Use earlier factsL66–71

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

  1. L66
    exact hpositive
  2. L67
    exact hfloor
  3. L68
    exact hdivision
  4. L69
    exact hcentral
  5. L70
    exact hfactorization_witness_witness_left
  6. L71
    exact hpower_a
12Establish hmiddleL72–81

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply no bertrand middle contribution interval le four pow.

  1. L72
    have hmiddle : exists bcf_le_gap_b5cblonbp_y_b. bcf_le_gap_b5cblonbp_y_b + (x4) = B
  2. L73
    specialize no_bertrand_middle_contribution_interval_le_four_pow n
  3. L74
    specialize no_bertrand_middle_contribution_interval_le_four_pow s
  4. L75
    specialize no_bertrand_middle_contribution_interval_le_four_pow q
  5. L76
    specialize no_bertrand_middle_contribution_interval_le_four_pow r
  6. L77
    specialize no_bertrand_middle_contribution_interval_le_four_pow C
  7. L78
    specialize no_bertrand_middle_contribution_interval_le_four_pow x
  8. L79
    specialize no_bertrand_middle_contribution_interval_le_four_pow x4
  9. L80
    specialize no_bertrand_middle_contribution_interval_le_four_pow B
  10. L81
    apply no_bertrand_middle_contribution_interval_le_four_pow
13Use earlier factsL82–89

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

  1. L82
    exact hexclusion
  2. L83
    exact hpositive
  3. L84
    exact hfloor
  4. L85
    exact hdivision
  5. L86
    exact hcentral
  6. L87
    exact hgaps_witness_witness_left
  7. L88
    exact hfactorization_witness_witness_right_left
  8. L89
    exact hpower_b
14Establish hproduct_boundL90–99

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

  1. L90
    have hproduct_bound : exists bcf_le_gap_b5cblonbp_product_bound. bcf_le_gap_b5cblonbp_product_bound + (x3 * x4) = A * B
  2. L91
    specialize mul_le_mul x3
  3. L92
    specialize mul_le_mul A
  4. L93
    specialize mul_le_mul x4
  5. L94
    specialize mul_le_mul B
  6. L95
    apply mul_le_mul
  7. L96
    exact hsmall
  8. L97
    exact hmiddle
  9. L98
    rewrite hproduct_witness_right
  10. L99
    rewrite hfactorization_witness_witness_right_right
15Use earlier factsL100–100

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

  1. L100
    exact hproduct_bound

Library-wide reading audit

Original exact command ledger · 100 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro C
  6. 0006intro A
  7. 0007intro B
  8. 0008intro hexclusion
  9. 0009intro hpositive
  10. 0010intro hfloor
  11. 0011intro hdivision
  12. 0012intro hcentral
  13. 0013intro hpower_a
  14. 0014intro hpower_b
  15. 0015have hgaps : exists g h. s + g = q /\ q + h = n + n
  16. 0016specialize floor_third_double_gap_package n
  17. 0017specialize floor_third_double_gap_package s
  18. 0018specialize floor_third_double_gap_package q
  19. 0019specialize floor_third_double_gap_package r
  20. 0020apply floor_third_double_gap_package
  21. 0021exact hpositive
  22. 0022exact hfloor
  23. 0023exact hdivision
  24. 0024cases hgaps
  25. 0025cases hgaps_witness
  26. 0026cases hgaps_witness_witness
  27. 0027have hproduct : exists z. (exists bpr_product_code_b5cblonbp_product bpr_product_scale_b5cblonbp_product. ((forall bpr_prefix_index_b5cblonbp_product_prefix. (exists bpr_gap_b5cblonbp_product_prefix_bound. bpr_gap_b5cblonbp_product_prefix_bound + S (bpr_prefix_index_b5cblonbp_product_prefix) = n + n) -> exists bpr_prefix_value_b5cblonbp_product_prefix. ((((exists bpr_height_b5cblonbp_product_prefix_decoded. bpr_height_b5cblonbp_product_prefix_decoded + S (bpr_prefix_value_b5cblonbp_product_prefix) = S ((S (bpr_prefix_index_b5cblonbp_product_prefix)) * bpr_product_scale_b5cblonbp_product)) /\ exists bpr_quotient_b5cblonbp_product_prefix_decoded. bpr_product_code_b5cblonbp_product = bpr_quotient_b5cblonbp_product_prefix_decoded * S ((S (bpr_prefix_index_b5cblonbp_product_prefix)) * bpr_product_scale_b5cblonbp_product) + (bpr_prefix_value_b5cblonbp_product_prefix))) /\ (((((~(S (bpr_prefix_index_b5cblonbp_product_prefix) = 1) /\ forall bpr_left_b5cblonbp_product_prefix_choice_prime bpr_right_b5cblonbp_product_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_product_prefix) = bpr_left_b5cblonbp_product_prefix_choice_prime * bpr_right_b5cblonbp_product_prefix_choice_prime -> bpr_left_b5cblonbp_product_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_product_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_product_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> exists ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) -> exists ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_product_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_product_prefix_choice_power bpr_power_scale_b5cblonbp_product_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_power = bpr_quotient_b5cblonbp_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_power_product ff_v_b5cblonbp_product_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_start. ff_h_b5cblonbp_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_start. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_b5cblonbp_product_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (bpr_prefix_value_b5cblonbp_product_prefix))) /\ forall ff_i_b5cblonbp_product_prefix_choice_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> exists ff_p_b5cblonbp_product_prefix_choice_power_product ff_r_b5cblonbp_product_prefix_choice_power_product ff_s_b5cblonbp_product_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_power = ff_q_b5cblonbp_product_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power) + (ff_p_b5cblonbp_product_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (ff_r_b5cblonbp_product_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (ff_s_b5cblonbp_product_prefix_choice_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_power_product = ff_r_b5cblonbp_product_prefix_choice_power_product * ff_p_b5cblonbp_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_b5cblonbp_product_prefix) = 1) /\ forall bpr_left_b5cblonbp_product_prefix_choice_prime bpr_right_b5cblonbp_product_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_product_prefix) = bpr_left_b5cblonbp_product_prefix_choice_prime * bpr_right_b5cblonbp_product_prefix_choice_prime -> bpr_left_b5cblonbp_product_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_b5cblonbp_product_prefix = 1))))) /\ (exists ff_u_b5cblonbp_product_product ff_v_b5cblonbp_product_product. ((((exists ff_h_b5cblonbp_product_product_start. ff_h_b5cblonbp_product_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_start. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_start * S ((S (0)) * ff_v_b5cblonbp_product_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_product_terminal. ff_h_b5cblonbp_product_product_terminal + S (z) = S ((S (n + n)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_terminal. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_terminal * S ((S (n + n)) * ff_v_b5cblonbp_product_product) + (z))) /\ forall ff_i_b5cblonbp_product_product. (exists ff_lt_b5cblonbp_product_product_bound. ff_lt_b5cblonbp_product_product_bound + S ff_i_b5cblonbp_product_product = n + n) -> exists ff_p_b5cblonbp_product_product ff_r_b5cblonbp_product_product ff_s_b5cblonbp_product_product. ((((exists ff_h_b5cblonbp_product_product_factor. ff_h_b5cblonbp_product_product_factor + S (ff_p_b5cblonbp_product_product) = S ((S (ff_i_b5cblonbp_product_product)) * bpr_product_scale_b5cblonbp_product)) /\ exists ff_q_b5cblonbp_product_product_factor. bpr_product_code_b5cblonbp_product = ff_q_b5cblonbp_product_product_factor * S ((S (ff_i_b5cblonbp_product_product)) * bpr_product_scale_b5cblonbp_product) + (ff_p_b5cblonbp_product_product))) /\ ((((exists ff_h_b5cblonbp_product_product_partial. ff_h_b5cblonbp_product_product_partial + S (ff_r_b5cblonbp_product_product) = S ((S (ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_partial. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_partial * S ((S (ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product) + (ff_r_b5cblonbp_product_product))) /\ ((((exists ff_h_b5cblonbp_product_product_successor. ff_h_b5cblonbp_product_product_successor + S (ff_s_b5cblonbp_product_product) = S ((S (S ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_successor. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_successor * S ((S (S ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product) + (ff_s_b5cblonbp_product_product))) /\ ff_s_b5cblonbp_product_product = ff_r_b5cblonbp_product_product * ff_p_b5cblonbp_product_product)))))))) /\ C = z
  28. 0028specialize central_binom_prime_contribution_product_exists n
  29. 0029specialize central_binom_prime_contribution_product_exists C
  30. 0030apply central_binom_prime_contribution_product_exists
  31. 0031exact hcentral
  32. 0032cases hproduct
  33. 0033cases hproduct_witness
  34. 0034have hfactorization : exists u v. (exists bpr_product_code_b5cblonbp_small bpr_product_scale_b5cblonbp_small. ((forall bpr_prefix_index_b5cblonbp_small_prefix. (exists bpr_gap_b5cblonbp_small_prefix_bound. bpr_gap_b5cblonbp_small_prefix_bound + S (bpr_prefix_index_b5cblonbp_small_prefix) = s) -> exists bpr_prefix_value_b5cblonbp_small_prefix. ((((exists bpr_height_b5cblonbp_small_prefix_decoded. bpr_height_b5cblonbp_small_prefix_decoded + S (bpr_prefix_value_b5cblonbp_small_prefix) = S ((S (bpr_prefix_index_b5cblonbp_small_prefix)) * bpr_product_scale_b5cblonbp_small)) /\ exists bpr_quotient_b5cblonbp_small_prefix_decoded. bpr_product_code_b5cblonbp_small = bpr_quotient_b5cblonbp_small_prefix_decoded * S ((S (bpr_prefix_index_b5cblonbp_small_prefix)) * bpr_product_scale_b5cblonbp_small) + (bpr_prefix_value_b5cblonbp_small_prefix))) /\ (((((~(S (bpr_prefix_index_b5cblonbp_small_prefix) = 1) /\ forall bpr_left_b5cblonbp_small_prefix_choice_prime bpr_right_b5cblonbp_small_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_small_prefix) = bpr_left_b5cblonbp_small_prefix_choice_prime * bpr_right_b5cblonbp_small_prefix_choice_prime -> bpr_left_b5cblonbp_small_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_small_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_small_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_small_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> exists ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) -> exists ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_small_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_small_prefix_choice_power bpr_power_scale_b5cblonbp_small_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_power = bpr_quotient_b5cblonbp_small_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_power_product ff_v_b5cblonbp_small_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_start. ff_h_b5cblonbp_small_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_start. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_power_product_terminal + S (bpr_prefix_value_b5cblonbp_small_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (bpr_prefix_value_b5cblonbp_small_prefix))) /\ forall ff_i_b5cblonbp_small_prefix_choice_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> exists ff_p_b5cblonbp_small_prefix_choice_power_product ff_r_b5cblonbp_small_prefix_choice_power_product ff_s_b5cblonbp_small_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_power = ff_q_b5cblonbp_small_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power) + (ff_p_b5cblonbp_small_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (ff_r_b5cblonbp_small_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (ff_s_b5cblonbp_small_prefix_choice_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_power_product = ff_r_b5cblonbp_small_prefix_choice_power_product * ff_p_b5cblonbp_small_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_b5cblonbp_small_prefix) = 1) /\ forall bpr_left_b5cblonbp_small_prefix_choice_prime bpr_right_b5cblonbp_small_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_small_prefix) = bpr_left_b5cblonbp_small_prefix_choice_prime * bpr_right_b5cblonbp_small_prefix_choice_prime -> bpr_left_b5cblonbp_small_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_small_prefix_choice_prime = 1)) /\ bpr_prefix_value_b5cblonbp_small_prefix = 1))))) /\ (exists ff_u_b5cblonbp_small_product ff_v_b5cblonbp_small_product. ((((exists ff_h_b5cblonbp_small_product_start. ff_h_b5cblonbp_small_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_start. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_start * S ((S (0)) * ff_v_b5cblonbp_small_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_product_terminal. ff_h_b5cblonbp_small_product_terminal + S (u) = S ((S (s)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_terminal. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_terminal * S ((S (s)) * ff_v_b5cblonbp_small_product) + (u))) /\ forall ff_i_b5cblonbp_small_product. (exists ff_lt_b5cblonbp_small_product_bound. ff_lt_b5cblonbp_small_product_bound + S ff_i_b5cblonbp_small_product = s) -> exists ff_p_b5cblonbp_small_product ff_r_b5cblonbp_small_product ff_s_b5cblonbp_small_product. ((((exists ff_h_b5cblonbp_small_product_factor. ff_h_b5cblonbp_small_product_factor + S (ff_p_b5cblonbp_small_product) = S ((S (ff_i_b5cblonbp_small_product)) * bpr_product_scale_b5cblonbp_small)) /\ exists ff_q_b5cblonbp_small_product_factor. bpr_product_code_b5cblonbp_small = ff_q_b5cblonbp_small_product_factor * S ((S (ff_i_b5cblonbp_small_product)) * bpr_product_scale_b5cblonbp_small) + (ff_p_b5cblonbp_small_product))) /\ ((((exists ff_h_b5cblonbp_small_product_partial. ff_h_b5cblonbp_small_product_partial + S (ff_r_b5cblonbp_small_product) = S ((S (ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_partial. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_partial * S ((S (ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product) + (ff_r_b5cblonbp_small_product))) /\ ((((exists ff_h_b5cblonbp_small_product_successor. ff_h_b5cblonbp_small_product_successor + S (ff_s_b5cblonbp_small_product) = S ((S (S ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_successor. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_successor * S ((S (S ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product) + (ff_s_b5cblonbp_small_product))) /\ ff_s_b5cblonbp_small_product = ff_r_b5cblonbp_small_product * ff_p_b5cblonbp_small_product)))))))) /\ ((exists bpr_code_b5cblonbp_middle bpr_scale_b5cblonbp_middle. ((forall bpr_index_b5cblonbp_middle_prefix. (exists bpr_gap_b5cblonbp_middle_prefix_bound. bpr_gap_b5cblonbp_middle_prefix_bound + S (bpr_index_b5cblonbp_middle_prefix) = x) -> exists bpr_value_b5cblonbp_middle_prefix. ((((exists bpr_height_b5cblonbp_middle_prefix_decoded. bpr_height_b5cblonbp_middle_prefix_decoded + S (bpr_value_b5cblonbp_middle_prefix) = S ((S (bpr_index_b5cblonbp_middle_prefix)) * bpr_scale_b5cblonbp_middle)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_decoded. bpr_code_b5cblonbp_middle = bpr_quotient_b5cblonbp_middle_prefix_decoded * S ((S (bpr_index_b5cblonbp_middle_prefix)) * bpr_scale_b5cblonbp_middle) + (bpr_value_b5cblonbp_middle_prefix))) /\ (((((~(S (s + bpr_index_b5cblonbp_middle_prefix) = 1) /\ forall bpr_left_b5cblonbp_middle_prefix_choice_prime bpr_right_b5cblonbp_middle_prefix_choice_prime. S (s + bpr_index_b5cblonbp_middle_prefix) = bpr_left_b5cblonbp_middle_prefix_choice_prime * bpr_right_b5cblonbp_middle_prefix_choice_prime -> bpr_left_b5cblonbp_middle_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_middle_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_middle_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_middle_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> exists ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) -> exists ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_middle_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_middle_prefix_choice_power bpr_power_scale_b5cblonbp_middle_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_power = bpr_quotient_b5cblonbp_middle_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_power_product ff_v_b5cblonbp_middle_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_power_product_terminal + S (bpr_value_b5cblonbp_middle_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (bpr_value_b5cblonbp_middle_prefix))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> exists ff_p_b5cblonbp_middle_prefix_choice_power_product ff_r_b5cblonbp_middle_prefix_choice_power_product ff_s_b5cblonbp_middle_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_power = ff_q_b5cblonbp_middle_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power) + (ff_p_b5cblonbp_middle_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_power_product = ff_r_b5cblonbp_middle_prefix_choice_power_product * ff_p_b5cblonbp_middle_prefix_choice_power_product)))))))))) \/ (~((~(S (s + bpr_index_b5cblonbp_middle_prefix) = 1) /\ forall bpr_left_b5cblonbp_middle_prefix_choice_prime bpr_right_b5cblonbp_middle_prefix_choice_prime. S (s + bpr_index_b5cblonbp_middle_prefix) = bpr_left_b5cblonbp_middle_prefix_choice_prime * bpr_right_b5cblonbp_middle_prefix_choice_prime -> bpr_left_b5cblonbp_middle_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_middle_prefix_choice_prime = 1)) /\ bpr_value_b5cblonbp_middle_prefix = 1))))) /\ (exists ff_u_b5cblonbp_middle_product ff_v_b5cblonbp_middle_product. ((((exists ff_h_b5cblonbp_middle_product_start. ff_h_b5cblonbp_middle_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_start. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_product_terminal. ff_h_b5cblonbp_middle_product_terminal + S (v) = S ((S (x)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_terminal. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_terminal * S ((S (x)) * ff_v_b5cblonbp_middle_product) + (v))) /\ forall ff_i_b5cblonbp_middle_product. (exists ff_lt_b5cblonbp_middle_product_bound. ff_lt_b5cblonbp_middle_product_bound + S ff_i_b5cblonbp_middle_product = x) -> exists ff_p_b5cblonbp_middle_product ff_r_b5cblonbp_middle_product ff_s_b5cblonbp_middle_product. ((((exists ff_h_b5cblonbp_middle_product_factor. ff_h_b5cblonbp_middle_product_factor + S (ff_p_b5cblonbp_middle_product) = S ((S (ff_i_b5cblonbp_middle_product)) * bpr_scale_b5cblonbp_middle)) /\ exists ff_q_b5cblonbp_middle_product_factor. bpr_code_b5cblonbp_middle = ff_q_b5cblonbp_middle_product_factor * S ((S (ff_i_b5cblonbp_middle_product)) * bpr_scale_b5cblonbp_middle) + (ff_p_b5cblonbp_middle_product))) /\ ((((exists ff_h_b5cblonbp_middle_product_partial. ff_h_b5cblonbp_middle_product_partial + S (ff_r_b5cblonbp_middle_product) = S ((S (ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_partial. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_partial * S ((S (ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product) + (ff_r_b5cblonbp_middle_product))) /\ ((((exists ff_h_b5cblonbp_middle_product_successor. ff_h_b5cblonbp_middle_product_successor + S (ff_s_b5cblonbp_middle_product) = S ((S (S ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_successor. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_successor * S ((S (S ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product) + (ff_s_b5cblonbp_middle_product))) /\ ff_s_b5cblonbp_middle_product = ff_r_b5cblonbp_middle_product * ff_p_b5cblonbp_middle_product)))))))) /\ x2 = u * v)
  35. 0035specialize central_binom_factorization_small n
  36. 0036specialize central_binom_factorization_small s
  37. 0037specialize central_binom_factorization_small q
  38. 0038specialize central_binom_factorization_small r
  39. 0039specialize central_binom_factorization_small C
  40. 0040specialize central_binom_factorization_small x
  41. 0041specialize central_binom_factorization_small x1
  42. 0042specialize central_binom_factorization_small x2
  43. 0043apply central_binom_factorization_small
  44. 0044exact hexclusion
  45. 0045exact hpositive
  46. 0046exact hfloor
  47. 0047exact hdivision
  48. 0048exact hcentral
  49. 0049exact hgaps_witness_witness_left
  50. 0050exact hgaps_witness_witness_right
  51. 0051exact hproduct_witness_left
  52. 0052cases hfactorization
  53. 0053cases hfactorization_witness
  54. 0054cases hfactorization_witness_witness
  55. 0055cases hfactorization_witness_witness_right
  56. 0056have hsmall : exists bcf_le_gap_b5cblonbp_x_a. bcf_le_gap_b5cblonbp_x_a + (x3) = A
  57. 0057specialize no_bertrand_small_contribution_product_le_power n
  58. 0058specialize no_bertrand_small_contribution_product_le_power s
  59. 0059specialize no_bertrand_small_contribution_product_le_power q
  60. 0060specialize no_bertrand_small_contribution_product_le_power r
  61. 0061specialize no_bertrand_small_contribution_product_le_power C
  62. 0062specialize no_bertrand_small_contribution_product_le_power x3
  63. 0063specialize no_bertrand_small_contribution_product_le_power A
  64. 0064apply no_bertrand_small_contribution_product_le_power
  65. 0065exact hexclusion
  66. 0066exact hpositive
  67. 0067exact hfloor
  68. 0068exact hdivision
  69. 0069exact hcentral
  70. 0070exact hfactorization_witness_witness_left
  71. 0071exact hpower_a
  72. 0072have hmiddle : exists bcf_le_gap_b5cblonbp_y_b. bcf_le_gap_b5cblonbp_y_b + (x4) = B
  73. 0073specialize no_bertrand_middle_contribution_interval_le_four_pow n
  74. 0074specialize no_bertrand_middle_contribution_interval_le_four_pow s
  75. 0075specialize no_bertrand_middle_contribution_interval_le_four_pow q
  76. 0076specialize no_bertrand_middle_contribution_interval_le_four_pow r
  77. 0077specialize no_bertrand_middle_contribution_interval_le_four_pow C
  78. 0078specialize no_bertrand_middle_contribution_interval_le_four_pow x
  79. 0079specialize no_bertrand_middle_contribution_interval_le_four_pow x4
  80. 0080specialize no_bertrand_middle_contribution_interval_le_four_pow B
  81. 0081apply no_bertrand_middle_contribution_interval_le_four_pow
  82. 0082exact hexclusion
  83. 0083exact hpositive
  84. 0084exact hfloor
  85. 0085exact hdivision
  86. 0086exact hcentral
  87. 0087exact hgaps_witness_witness_left
  88. 0088exact hfactorization_witness_witness_right_left
  89. 0089exact hpower_b
  90. 0090have hproduct_bound : exists bcf_le_gap_b5cblonbp_product_bound. bcf_le_gap_b5cblonbp_product_bound + (x3 * x4) = A * B
  91. 0091specialize mul_le_mul x3
  92. 0092specialize mul_le_mul A
  93. 0093specialize mul_le_mul x4
  94. 0094specialize mul_le_mul B
  95. 0095apply mul_le_mul
  96. 0096exact hsmall
  97. 0097exact hmiddle
  98. 0098rewrite hproduct_witness_right
  99. 0099rewrite hfactorization_witness_witness_right_right
  100. 0100exact hproduct_bound