BT00Y5

central_binom_prime_power_contribution_le_double

Alpha body-checked · checked-use disabled

Every complete prime-power contribution is bounded by twice n.

Exact expanded PA statement

forall p n C v D. ((~(p = 1) /\ forall frm_prime_left_b5ccppcld_prime frm_prime_right_b5ccppcld_prime. p = frm_prime_left_b5ccppcld_prime * frm_prime_right_b5ccppcld_prime -> frm_prime_left_b5ccppcld_prime = 1 \/ frm_prime_right_b5ccppcld_prime = 1)) -> (exists bcf_le_gap_b5ccppcld_positive. bcf_le_gap_b5ccppcld_positive + (1) = n) -> (((exists bcf_lt_gap_b5ccppcld_central_out_of_range. bcf_lt_gap_b5ccppcld_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_b5ccppcld_central_in_range. bcf_le_gap_b5ccppcld_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_b5ccppcld_central bcf_row_code_scale_b5ccppcld_central bcf_row_scale_code_b5ccppcld_central bcf_row_scale_scale_b5ccppcld_central bcf_row_code_b5ccppcld_central bcf_row_scale_b5ccppcld_central. ((forall bcf_row_index_b5ccppcld_central_table. (exists bcf_lt_gap_b5ccppcld_central_table_row_bound. bcf_lt_gap_b5ccppcld_central_table_row_bound + S (bcf_row_index_b5ccppcld_central_table) = S (n + n)) -> exists bcf_row_code_b5ccppcld_central_table bcf_row_scale_b5ccppcld_central_table. ((((exists bcf_height_b5ccppcld_central_table_decoded_row_code. bcf_height_b5ccppcld_central_table_decoded_row_code + S (bcf_row_code_b5ccppcld_central_table) = S ((S (bcf_row_index_b5ccppcld_central_table)) * bcf_row_code_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_table_decoded_row_code. bcf_row_code_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_table_decoded_row_code * S ((S (bcf_row_index_b5ccppcld_central_table)) * bcf_row_code_scale_b5ccppcld_central) + (bcf_row_code_b5ccppcld_central_table))) /\ ((((exists bcf_height_b5ccppcld_central_table_decoded_row_scale. bcf_height_b5ccppcld_central_table_decoded_row_scale + S (bcf_row_scale_b5ccppcld_central_table) = S ((S (bcf_row_index_b5ccppcld_central_table)) * bcf_row_scale_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_table_decoded_row_scale. bcf_row_scale_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_table_decoded_row_scale * S ((S (bcf_row_index_b5ccppcld_central_table)) * bcf_row_scale_scale_b5ccppcld_central) + (bcf_row_scale_b5ccppcld_central_table))) /\ ((bcf_row_index_b5ccppcld_central_table = 0 /\ (forall bcf_index_b5ccppcld_central_table_zero_row. (exists bcf_lt_gap_b5ccppcld_central_table_zero_row_bound. bcf_lt_gap_b5ccppcld_central_table_zero_row_bound + S (bcf_index_b5ccppcld_central_table_zero_row) = S (n + n)) -> exists bcf_value_b5ccppcld_central_table_zero_row. ((((exists bcf_height_b5ccppcld_central_table_zero_row_entry. bcf_height_b5ccppcld_central_table_zero_row_entry + S (bcf_value_b5ccppcld_central_table_zero_row) = S ((S (bcf_index_b5ccppcld_central_table_zero_row)) * bcf_row_scale_b5ccppcld_central_table)) /\ exists bcf_quotient_b5ccppcld_central_table_zero_row_entry. bcf_row_code_b5ccppcld_central_table = bcf_quotient_b5ccppcld_central_table_zero_row_entry * S ((S (bcf_index_b5ccppcld_central_table_zero_row)) * bcf_row_scale_b5ccppcld_central_table) + (bcf_value_b5ccppcld_central_table_zero_row))) /\ ((bcf_index_b5ccppcld_central_table_zero_row = 0 /\ bcf_value_b5ccppcld_central_table_zero_row = 1) \/ exists bcf_predecessor_b5ccppcld_central_table_zero_row. bcf_index_b5ccppcld_central_table_zero_row = S bcf_predecessor_b5ccppcld_central_table_zero_row /\ bcf_value_b5ccppcld_central_table_zero_row = 0)))) \/ exists bcf_predecessor_b5ccppcld_central_table bcf_previous_code_b5ccppcld_central_table bcf_previous_scale_b5ccppcld_central_table. bcf_row_index_b5ccppcld_central_table = S bcf_predecessor_b5ccppcld_central_table /\ ((((exists bcf_height_b5ccppcld_central_table_decoded_previous_code. bcf_height_b5ccppcld_central_table_decoded_previous_code + S (bcf_previous_code_b5ccppcld_central_table) = S ((S (bcf_predecessor_b5ccppcld_central_table)) * bcf_row_code_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_table_decoded_previous_code. bcf_row_code_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_table_decoded_previous_code * S ((S (bcf_predecessor_b5ccppcld_central_table)) * bcf_row_code_scale_b5ccppcld_central) + (bcf_previous_code_b5ccppcld_central_table))) /\ ((((exists bcf_height_b5ccppcld_central_table_decoded_previous_scale. bcf_height_b5ccppcld_central_table_decoded_previous_scale + S (bcf_previous_scale_b5ccppcld_central_table) = S ((S (bcf_predecessor_b5ccppcld_central_table)) * bcf_row_scale_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_table_decoded_previous_scale. bcf_row_scale_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_table_decoded_previous_scale * S ((S (bcf_predecessor_b5ccppcld_central_table)) * bcf_row_scale_scale_b5ccppcld_central) + (bcf_previous_scale_b5ccppcld_central_table))) /\ (forall bcf_index_b5ccppcld_central_table_row_step. (exists bcf_lt_gap_b5ccppcld_central_table_row_step_bound. bcf_lt_gap_b5ccppcld_central_table_row_step_bound + S (bcf_index_b5ccppcld_central_table_row_step) = S (n + n)) -> exists bcf_value_b5ccppcld_central_table_row_step. ((((exists bcf_height_b5ccppcld_central_table_row_step_entry. bcf_height_b5ccppcld_central_table_row_step_entry + S (bcf_value_b5ccppcld_central_table_row_step) = S ((S (bcf_index_b5ccppcld_central_table_row_step)) * bcf_row_scale_b5ccppcld_central_table)) /\ exists bcf_quotient_b5ccppcld_central_table_row_step_entry. bcf_row_code_b5ccppcld_central_table = bcf_quotient_b5ccppcld_central_table_row_step_entry * S ((S (bcf_index_b5ccppcld_central_table_row_step)) * bcf_row_scale_b5ccppcld_central_table) + (bcf_value_b5ccppcld_central_table_row_step))) /\ ((bcf_index_b5ccppcld_central_table_row_step = 0 /\ bcf_value_b5ccppcld_central_table_row_step = 1) \/ exists bcf_predecessor_b5ccppcld_central_table_row_step bcf_left_b5ccppcld_central_table_row_step bcf_right_b5ccppcld_central_table_row_step. bcf_index_b5ccppcld_central_table_row_step = S bcf_predecessor_b5ccppcld_central_table_row_step /\ ((((exists bcf_height_b5ccppcld_central_table_row_step_previous_left. bcf_height_b5ccppcld_central_table_row_step_previous_left + S (bcf_left_b5ccppcld_central_table_row_step) = S ((S (bcf_predecessor_b5ccppcld_central_table_row_step)) * bcf_previous_scale_b5ccppcld_central_table)) /\ exists bcf_quotient_b5ccppcld_central_table_row_step_previous_left. bcf_previous_code_b5ccppcld_central_table = bcf_quotient_b5ccppcld_central_table_row_step_previous_left * S ((S (bcf_predecessor_b5ccppcld_central_table_row_step)) * bcf_previous_scale_b5ccppcld_central_table) + (bcf_left_b5ccppcld_central_table_row_step))) /\ ((((exists bcf_height_b5ccppcld_central_table_row_step_previous_right. bcf_height_b5ccppcld_central_table_row_step_previous_right + S (bcf_right_b5ccppcld_central_table_row_step) = S ((S (S (bcf_predecessor_b5ccppcld_central_table_row_step))) * bcf_previous_scale_b5ccppcld_central_table)) /\ exists bcf_quotient_b5ccppcld_central_table_row_step_previous_right. bcf_previous_code_b5ccppcld_central_table = bcf_quotient_b5ccppcld_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_b5ccppcld_central_table_row_step))) * bcf_previous_scale_b5ccppcld_central_table) + (bcf_right_b5ccppcld_central_table_row_step))) /\ bcf_value_b5ccppcld_central_table_row_step = bcf_left_b5ccppcld_central_table_row_step + bcf_right_b5ccppcld_central_table_row_step))))))))))) /\ ((((exists bcf_height_b5ccppcld_central_decoded_row_code. bcf_height_b5ccppcld_central_decoded_row_code + S (bcf_row_code_b5ccppcld_central) = S ((S (n + n)) * bcf_row_code_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_decoded_row_code. bcf_row_code_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_b5ccppcld_central) + (bcf_row_code_b5ccppcld_central))) /\ ((((exists bcf_height_b5ccppcld_central_decoded_row_scale. bcf_height_b5ccppcld_central_decoded_row_scale + S (bcf_row_scale_b5ccppcld_central) = S ((S (n + n)) * bcf_row_scale_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_decoded_row_scale. bcf_row_scale_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_b5ccppcld_central) + (bcf_row_scale_b5ccppcld_central))) /\ (((exists bcf_height_b5ccppcld_central_decoded_value. bcf_height_b5ccppcld_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_b5ccppcld_central)) /\ exists bcf_quotient_b5ccppcld_central_decoded_value. bcf_row_code_b5ccppcld_central = bcf_quotient_b5ccppcld_central_decoded_value * S ((S (n)) * bcf_row_scale_b5ccppcld_central) + (C))))))))) -> (((exists bpv_gap_b5ccppcld_valuation_exponent_bound. bpv_gap_b5ccppcld_valuation_exponent_bound + v = C) /\ (exists bpv_result_b5ccppcld_valuation_selected. ((exists ff_b_b5ccppcld_valuation_selected_power ff_c_b5ccppcld_valuation_selected_power. ((forall ff_i_b5ccppcld_valuation_selected_power_repeat. (exists ff_lt_b5ccppcld_valuation_selected_power_repeat_bound. ff_lt_b5ccppcld_valuation_selected_power_repeat_bound + S ff_i_b5ccppcld_valuation_selected_power_repeat = v) -> (((exists ff_h_b5ccppcld_valuation_selected_power_repeat_decoded. ff_h_b5ccppcld_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_b5ccppcld_valuation_selected_power_repeat)) * ff_c_b5ccppcld_valuation_selected_power)) /\ exists ff_q_b5ccppcld_valuation_selected_power_repeat_decoded. ff_b_b5ccppcld_valuation_selected_power = ff_q_b5ccppcld_valuation_selected_power_repeat_decoded * S ((S (ff_i_b5ccppcld_valuation_selected_power_repeat)) * ff_c_b5ccppcld_valuation_selected_power) + (p)))) /\ (exists ff_u_b5ccppcld_valuation_selected_power_product ff_v_b5ccppcld_valuation_selected_power_product. ((((exists ff_h_b5ccppcld_valuation_selected_power_product_start. ff_h_b5ccppcld_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5ccppcld_valuation_selected_power_product)) /\ exists ff_q_b5ccppcld_valuation_selected_power_product_start. ff_u_b5ccppcld_valuation_selected_power_product = ff_q_b5ccppcld_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5ccppcld_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5ccppcld_valuation_selected_power_product_terminal. ff_h_b5ccppcld_valuation_selected_power_product_terminal + S (bpv_result_b5ccppcld_valuation_selected) = S ((S (v)) * ff_v_b5ccppcld_valuation_selected_power_product)) /\ exists ff_q_b5ccppcld_valuation_selected_power_product_terminal. ff_u_b5ccppcld_valuation_selected_power_product = ff_q_b5ccppcld_valuation_selected_power_product_terminal * S ((S (v)) * ff_v_b5ccppcld_valuation_selected_power_product) + (bpv_result_b5ccppcld_valuation_selected))) /\ forall ff_i_b5ccppcld_valuation_selected_power_product. (exists ff_lt_b5ccppcld_valuation_selected_power_product_bound. ff_lt_b5ccppcld_valuation_selected_power_product_bound + S ff_i_b5ccppcld_valuation_selected_power_product = v) -> exists ff_p_b5ccppcld_valuation_selected_power_product ff_r_b5ccppcld_valuation_selected_power_product ff_s_b5ccppcld_valuation_selected_power_product. ((((exists ff_h_b5ccppcld_valuation_selected_power_product_factor. ff_h_b5ccppcld_valuation_selected_power_product_factor + S (ff_p_b5ccppcld_valuation_selected_power_product) = S ((S (ff_i_b5ccppcld_valuation_selected_power_product)) * ff_c_b5ccppcld_valuation_selected_power)) /\ exists ff_q_b5ccppcld_valuation_selected_power_product_factor. ff_b_b5ccppcld_valuation_selected_power = ff_q_b5ccppcld_valuation_selected_power_product_factor * S ((S (ff_i_b5ccppcld_valuation_selected_power_product)) * ff_c_b5ccppcld_valuation_selected_power) + (ff_p_b5ccppcld_valuation_selected_power_product))) /\ ((((exists ff_h_b5ccppcld_valuation_selected_power_product_partial. ff_h_b5ccppcld_valuation_selected_power_product_partial + S (ff_r_b5ccppcld_valuation_selected_power_product) = S ((S (ff_i_b5ccppcld_valuation_selected_power_product)) * ff_v_b5ccppcld_valuation_selected_power_product)) /\ exists ff_q_b5ccppcld_valuation_selected_power_product_partial. ff_u_b5ccppcld_valuation_selected_power_product = ff_q_b5ccppcld_valuation_selected_power_product_partial * S ((S (ff_i_b5ccppcld_valuation_selected_power_product)) * ff_v_b5ccppcld_valuation_selected_power_product) + (ff_r_b5ccppcld_valuation_selected_power_product))) /\ ((((exists ff_h_b5ccppcld_valuation_selected_power_product_successor. ff_h_b5ccppcld_valuation_selected_power_product_successor + S (ff_s_b5ccppcld_valuation_selected_power_product) = S ((S (S ff_i_b5ccppcld_valuation_selected_power_product)) * ff_v_b5ccppcld_valuation_selected_power_product)) /\ exists ff_q_b5ccppcld_valuation_selected_power_product_successor. ff_u_b5ccppcld_valuation_selected_power_product = ff_q_b5ccppcld_valuation_selected_power_product_successor * S ((S (S ff_i_b5ccppcld_valuation_selected_power_product)) * ff_v_b5ccppcld_valuation_selected_power_product) + (ff_s_b5ccppcld_valuation_selected_power_product))) /\ ff_s_b5ccppcld_valuation_selected_power_product = ff_r_b5ccppcld_valuation_selected_power_product * ff_p_b5ccppcld_valuation_selected_power_product)))))))) /\ (exists bpv_factor_b5ccppcld_valuation_selected_divides. C = bpv_result_b5ccppcld_valuation_selected * bpv_factor_b5ccppcld_valuation_selected_divides)))) /\ forall bpv_candidate_b5ccppcld_valuation. (exists bpv_gap_b5ccppcld_valuation_candidate_bound. bpv_gap_b5ccppcld_valuation_candidate_bound + bpv_candidate_b5ccppcld_valuation = C) -> (exists bpv_result_b5ccppcld_valuation_candidate. ((exists ff_b_b5ccppcld_valuation_candidate_power ff_c_b5ccppcld_valuation_candidate_power. ((forall ff_i_b5ccppcld_valuation_candidate_power_repeat. (exists ff_lt_b5ccppcld_valuation_candidate_power_repeat_bound. ff_lt_b5ccppcld_valuation_candidate_power_repeat_bound + S ff_i_b5ccppcld_valuation_candidate_power_repeat = bpv_candidate_b5ccppcld_valuation) -> (((exists ff_h_b5ccppcld_valuation_candidate_power_repeat_decoded. ff_h_b5ccppcld_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_b5ccppcld_valuation_candidate_power_repeat)) * ff_c_b5ccppcld_valuation_candidate_power)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_repeat_decoded. ff_b_b5ccppcld_valuation_candidate_power = ff_q_b5ccppcld_valuation_candidate_power_repeat_decoded * S ((S (ff_i_b5ccppcld_valuation_candidate_power_repeat)) * ff_c_b5ccppcld_valuation_candidate_power) + (p)))) /\ (exists ff_u_b5ccppcld_valuation_candidate_power_product ff_v_b5ccppcld_valuation_candidate_power_product. ((((exists ff_h_b5ccppcld_valuation_candidate_power_product_start. ff_h_b5ccppcld_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5ccppcld_valuation_candidate_power_product)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_product_start. ff_u_b5ccppcld_valuation_candidate_power_product = ff_q_b5ccppcld_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5ccppcld_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5ccppcld_valuation_candidate_power_product_terminal. ff_h_b5ccppcld_valuation_candidate_power_product_terminal + S (bpv_result_b5ccppcld_valuation_candidate) = S ((S (bpv_candidate_b5ccppcld_valuation)) * ff_v_b5ccppcld_valuation_candidate_power_product)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_product_terminal. ff_u_b5ccppcld_valuation_candidate_power_product = ff_q_b5ccppcld_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_b5ccppcld_valuation)) * ff_v_b5ccppcld_valuation_candidate_power_product) + (bpv_result_b5ccppcld_valuation_candidate))) /\ forall ff_i_b5ccppcld_valuation_candidate_power_product. (exists ff_lt_b5ccppcld_valuation_candidate_power_product_bound. ff_lt_b5ccppcld_valuation_candidate_power_product_bound + S ff_i_b5ccppcld_valuation_candidate_power_product = bpv_candidate_b5ccppcld_valuation) -> exists ff_p_b5ccppcld_valuation_candidate_power_product ff_r_b5ccppcld_valuation_candidate_power_product ff_s_b5ccppcld_valuation_candidate_power_product. ((((exists ff_h_b5ccppcld_valuation_candidate_power_product_factor. ff_h_b5ccppcld_valuation_candidate_power_product_factor + S (ff_p_b5ccppcld_valuation_candidate_power_product) = S ((S (ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_c_b5ccppcld_valuation_candidate_power)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_product_factor. ff_b_b5ccppcld_valuation_candidate_power = ff_q_b5ccppcld_valuation_candidate_power_product_factor * S ((S (ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_c_b5ccppcld_valuation_candidate_power) + (ff_p_b5ccppcld_valuation_candidate_power_product))) /\ ((((exists ff_h_b5ccppcld_valuation_candidate_power_product_partial. ff_h_b5ccppcld_valuation_candidate_power_product_partial + S (ff_r_b5ccppcld_valuation_candidate_power_product) = S ((S (ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_v_b5ccppcld_valuation_candidate_power_product)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_product_partial. ff_u_b5ccppcld_valuation_candidate_power_product = ff_q_b5ccppcld_valuation_candidate_power_product_partial * S ((S (ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_v_b5ccppcld_valuation_candidate_power_product) + (ff_r_b5ccppcld_valuation_candidate_power_product))) /\ ((((exists ff_h_b5ccppcld_valuation_candidate_power_product_successor. ff_h_b5ccppcld_valuation_candidate_power_product_successor + S (ff_s_b5ccppcld_valuation_candidate_power_product) = S ((S (S ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_v_b5ccppcld_valuation_candidate_power_product)) /\ exists ff_q_b5ccppcld_valuation_candidate_power_product_successor. ff_u_b5ccppcld_valuation_candidate_power_product = ff_q_b5ccppcld_valuation_candidate_power_product_successor * S ((S (S ff_i_b5ccppcld_valuation_candidate_power_product)) * ff_v_b5ccppcld_valuation_candidate_power_product) + (ff_s_b5ccppcld_valuation_candidate_power_product))) /\ ff_s_b5ccppcld_valuation_candidate_power_product = ff_r_b5ccppcld_valuation_candidate_power_product * ff_p_b5ccppcld_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_b5ccppcld_valuation_candidate_divides. C = bpv_result_b5ccppcld_valuation_candidate * bpv_factor_b5ccppcld_valuation_candidate_divides))) -> (exists bpv_gap_b5ccppcld_valuation_maximal. bpv_gap_b5ccppcld_valuation_maximal + bpv_candidate_b5ccppcld_valuation = v)) -> (exists bpvi_b_b5ccppcld_power bpvi_c_b5ccppcld_power. ((forall bpvi_i_b5ccppcld_power. (exists bpvi_repeat_gap_b5ccppcld_power. bpvi_repeat_gap_b5ccppcld_power + S bpvi_i_b5ccppcld_power = v) -> (((exists bpvi_h_b5ccppcld_power_repeat. bpvi_h_b5ccppcld_power_repeat + S (p) = S ((S (bpvi_i_b5ccppcld_power)) * bpvi_c_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_repeat. bpvi_b_b5ccppcld_power = bpvi_q_b5ccppcld_power_repeat * S ((S (bpvi_i_b5ccppcld_power)) * bpvi_c_b5ccppcld_power) + (p)))) /\ (exists bpvi_u_b5ccppcld_power bpvi_v_b5ccppcld_power. ((((exists bpvi_h_b5ccppcld_power_start. bpvi_h_b5ccppcld_power_start + S (1) = S ((S (0)) * bpvi_v_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_start. bpvi_u_b5ccppcld_power = bpvi_q_b5ccppcld_power_start * S ((S (0)) * bpvi_v_b5ccppcld_power) + (1))) /\ ((((exists bpvi_h_b5ccppcld_power_terminal. bpvi_h_b5ccppcld_power_terminal + S (D) = S ((S (v)) * bpvi_v_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_terminal. bpvi_u_b5ccppcld_power = bpvi_q_b5ccppcld_power_terminal * S ((S (v)) * bpvi_v_b5ccppcld_power) + (D))) /\ forall bpvi_j_b5ccppcld_power. (exists bpvi_product_gap_b5ccppcld_power. bpvi_product_gap_b5ccppcld_power + S bpvi_j_b5ccppcld_power = v) -> exists bpvi_factor_b5ccppcld_power bpvi_partial_b5ccppcld_power bpvi_successor_b5ccppcld_power. ((((exists bpvi_h_b5ccppcld_power_factor. bpvi_h_b5ccppcld_power_factor + S (bpvi_factor_b5ccppcld_power) = S ((S (bpvi_j_b5ccppcld_power)) * bpvi_c_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_factor. bpvi_b_b5ccppcld_power = bpvi_q_b5ccppcld_power_factor * S ((S (bpvi_j_b5ccppcld_power)) * bpvi_c_b5ccppcld_power) + (bpvi_factor_b5ccppcld_power))) /\ ((((exists bpvi_h_b5ccppcld_power_partial. bpvi_h_b5ccppcld_power_partial + S (bpvi_partial_b5ccppcld_power) = S ((S (bpvi_j_b5ccppcld_power)) * bpvi_v_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_partial. bpvi_u_b5ccppcld_power = bpvi_q_b5ccppcld_power_partial * S ((S (bpvi_j_b5ccppcld_power)) * bpvi_v_b5ccppcld_power) + (bpvi_partial_b5ccppcld_power))) /\ ((((exists bpvi_h_b5ccppcld_power_successor. bpvi_h_b5ccppcld_power_successor + S (bpvi_successor_b5ccppcld_power) = S ((S (S bpvi_j_b5ccppcld_power)) * bpvi_v_b5ccppcld_power)) /\ exists bpvi_q_b5ccppcld_power_successor. bpvi_u_b5ccppcld_power = bpvi_q_b5ccppcld_power_successor * S ((S (S bpvi_j_b5ccppcld_power)) * bpvi_v_b5ccppcld_power) + (bpvi_successor_b5ccppcld_power))) /\ bpvi_successor_b5ccppcld_power = bpvi_partial_b5ccppcld_power * bpvi_factor_b5ccppcld_power)))))))) -> (exists bcf_le_gap_b5ccppcld_result. bcf_le_gap_b5ccppcld_result + (D) = n + n)

Structural proof guide

Every complete prime-power contribution is bounded by twice n.

Direct prerequisites: pow_zero, le_add_right, le_trans, prime_nonzero, one_le_of_ne_zero, beta_at_unique, pow_le_pow_of_exponent_le, bit_count_positive_last_one, division_successor_quotient_divisor_le, central_binom_carry_bit_count. The authored body proceeds by structural induction (1), case analysis (26), intermediate claims (14), equality transport (4).

Proof neighborhood

Direct dependencies

BT0081 pow_zero BT0013 le_add_right BT000F le_trans BT003G prime_nonzero BT0010 one_le_of_ne_zero BT0042 beta_at_unique BT00XJ pow_le_pow_of_exponent_le BT00Y1 bit_count_positive_last_one BT00Y2 division_successor_quotient_divisor_le BT00Y4 central_binom_carry_bit_count

Direct dependents

BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YL no_bertrand_central_nonzero_contribution_factor_ranges

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro C
  4. 0004induction v
  5. 0005intro D
  6. 0006intro hp
  7. 0007intro hpositive
  8. 0008intro hcentral
  9. 0009intro hvaluation
  10. 0010intro hpower
  11. 0011have hD : D = 1
  12. 0012specialize pow_zero p
  13. 0013specialize pow_zero 0
  14. 0014specialize pow_zero D
  15. 0015apply pow_zero
  16. 0016refl
  17. 0017exact hpower
  18. 0018have hn_double : exists h. h + n = n + n
  19. 0019specialize le_add_right n
  20. 0020specialize le_add_right n
  21. 0021exact le_add_right
  22. 0022have hone_double : exists h. h + 1 = n + n
  23. 0023specialize le_trans 1
  24. 0024specialize le_trans n
  25. 0025specialize le_trans (n + n)
  26. 0026apply le_trans
  27. 0027exact hpositive
  28. 0028exact hn_double
  29. 0029rewrite hD
  30. 0030exact hone_double
  31. 0031intro D
  32. 0032intro hp
  33. 0033intro hpositive
  34. 0034intro hcentral
  35. 0035intro hvaluation
  36. 0036intro hpower
  37. 0037have hpackage : exists b s d t f g. (forall bls_index_b5ccppcld_left. (exists bls_gap_b5ccppcld_left_bound. bls_gap_b5ccppcld_left_bound + S (bls_index_b5ccppcld_left) = (n + n)) -> exists bls_power_b5ccppcld_left bls_quotient_b5ccppcld_left bls_remainder_b5ccppcld_left. ((exists bpvi_b_bls_b5ccppcld_left_power bpvi_c_bls_b5ccppcld_left_power. ((forall bpvi_i_bls_b5ccppcld_left_power. (exists bpvi_repeat_gap_bls_b5ccppcld_left_power. bpvi_repeat_gap_bls_b5ccppcld_left_power + S bpvi_i_bls_b5ccppcld_left_power = S bls_index_b5ccppcld_left) -> (((exists bpvi_h_bls_b5ccppcld_left_power_repeat. bpvi_h_bls_b5ccppcld_left_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccppcld_left_power)) * bpvi_c_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_repeat. bpvi_b_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_repeat * S ((S (bpvi_i_bls_b5ccppcld_left_power)) * bpvi_c_bls_b5ccppcld_left_power) + (p)))) /\ (exists bpvi_u_bls_b5ccppcld_left_power bpvi_v_bls_b5ccppcld_left_power. ((((exists bpvi_h_bls_b5ccppcld_left_power_start. bpvi_h_bls_b5ccppcld_left_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_start. bpvi_u_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_start * S ((S (0)) * bpvi_v_bls_b5ccppcld_left_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccppcld_left_power_terminal. bpvi_h_bls_b5ccppcld_left_power_terminal + S (bls_power_b5ccppcld_left) = S ((S (S bls_index_b5ccppcld_left)) * bpvi_v_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_terminal. bpvi_u_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_terminal * S ((S (S bls_index_b5ccppcld_left)) * bpvi_v_bls_b5ccppcld_left_power) + (bls_power_b5ccppcld_left))) /\ forall bpvi_j_bls_b5ccppcld_left_power. (exists bpvi_product_gap_bls_b5ccppcld_left_power. bpvi_product_gap_bls_b5ccppcld_left_power + S bpvi_j_bls_b5ccppcld_left_power = S bls_index_b5ccppcld_left) -> exists bpvi_factor_bls_b5ccppcld_left_power bpvi_partial_bls_b5ccppcld_left_power bpvi_successor_bls_b5ccppcld_left_power. ((((exists bpvi_h_bls_b5ccppcld_left_power_factor. bpvi_h_bls_b5ccppcld_left_power_factor + S (bpvi_factor_bls_b5ccppcld_left_power) = S ((S (bpvi_j_bls_b5ccppcld_left_power)) * bpvi_c_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_factor. bpvi_b_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_factor * S ((S (bpvi_j_bls_b5ccppcld_left_power)) * bpvi_c_bls_b5ccppcld_left_power) + (bpvi_factor_bls_b5ccppcld_left_power))) /\ ((((exists bpvi_h_bls_b5ccppcld_left_power_partial. bpvi_h_bls_b5ccppcld_left_power_partial + S (bpvi_partial_bls_b5ccppcld_left_power) = S ((S (bpvi_j_bls_b5ccppcld_left_power)) * bpvi_v_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_partial. bpvi_u_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_partial * S ((S (bpvi_j_bls_b5ccppcld_left_power)) * bpvi_v_bls_b5ccppcld_left_power) + (bpvi_partial_bls_b5ccppcld_left_power))) /\ ((((exists bpvi_h_bls_b5ccppcld_left_power_successor. bpvi_h_bls_b5ccppcld_left_power_successor + S (bpvi_successor_bls_b5ccppcld_left_power) = S ((S (S bpvi_j_bls_b5ccppcld_left_power)) * bpvi_v_bls_b5ccppcld_left_power)) /\ exists bpvi_q_bls_b5ccppcld_left_power_successor. bpvi_u_bls_b5ccppcld_left_power = bpvi_q_bls_b5ccppcld_left_power_successor * S ((S (S bpvi_j_bls_b5ccppcld_left_power)) * bpvi_v_bls_b5ccppcld_left_power) + (bpvi_successor_bls_b5ccppcld_left_power))) /\ bpvi_successor_bls_b5ccppcld_left_power = bpvi_partial_bls_b5ccppcld_left_power * bpvi_factor_bls_b5ccppcld_left_power)))))))) /\ ((((exists ff_h_bls_b5ccppcld_left_quotient_entry. ff_h_bls_b5ccppcld_left_quotient_entry + S (bls_quotient_b5ccppcld_left) = S ((S (bls_index_b5ccppcld_left)) * s)) /\ exists ff_q_bls_b5ccppcld_left_quotient_entry. b = ff_q_bls_b5ccppcld_left_quotient_entry * S ((S (bls_index_b5ccppcld_left)) * s) + (bls_quotient_b5ccppcld_left))) /\ ((n = bls_power_b5ccppcld_left * bls_quotient_b5ccppcld_left + bls_remainder_b5ccppcld_left /\ exists bls_remainder_gap_b5ccppcld_left_division. bls_remainder_gap_b5ccppcld_left_division + S (bls_remainder_b5ccppcld_left) = bls_power_b5ccppcld_left))))) /\ ((forall bls_index_b5ccppcld_right. (exists bls_gap_b5ccppcld_right_bound. bls_gap_b5ccppcld_right_bound + S (bls_index_b5ccppcld_right) = (n + n)) -> exists bls_power_b5ccppcld_right bls_quotient_b5ccppcld_right bls_remainder_b5ccppcld_right. ((exists bpvi_b_bls_b5ccppcld_right_power bpvi_c_bls_b5ccppcld_right_power. ((forall bpvi_i_bls_b5ccppcld_right_power. (exists bpvi_repeat_gap_bls_b5ccppcld_right_power. bpvi_repeat_gap_bls_b5ccppcld_right_power + S bpvi_i_bls_b5ccppcld_right_power = S bls_index_b5ccppcld_right) -> (((exists bpvi_h_bls_b5ccppcld_right_power_repeat. bpvi_h_bls_b5ccppcld_right_power_repeat + S (p) = S ((S (bpvi_i_bls_b5ccppcld_right_power)) * bpvi_c_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_repeat. bpvi_b_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_repeat * S ((S (bpvi_i_bls_b5ccppcld_right_power)) * bpvi_c_bls_b5ccppcld_right_power) + (p)))) /\ (exists bpvi_u_bls_b5ccppcld_right_power bpvi_v_bls_b5ccppcld_right_power. ((((exists bpvi_h_bls_b5ccppcld_right_power_start. bpvi_h_bls_b5ccppcld_right_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_start. bpvi_u_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_start * S ((S (0)) * bpvi_v_bls_b5ccppcld_right_power) + (1))) /\ ((((exists bpvi_h_bls_b5ccppcld_right_power_terminal. bpvi_h_bls_b5ccppcld_right_power_terminal + S (bls_power_b5ccppcld_right) = S ((S (S bls_index_b5ccppcld_right)) * bpvi_v_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_terminal. bpvi_u_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_terminal * S ((S (S bls_index_b5ccppcld_right)) * bpvi_v_bls_b5ccppcld_right_power) + (bls_power_b5ccppcld_right))) /\ forall bpvi_j_bls_b5ccppcld_right_power. (exists bpvi_product_gap_bls_b5ccppcld_right_power. bpvi_product_gap_bls_b5ccppcld_right_power + S bpvi_j_bls_b5ccppcld_right_power = S bls_index_b5ccppcld_right) -> exists bpvi_factor_bls_b5ccppcld_right_power bpvi_partial_bls_b5ccppcld_right_power bpvi_successor_bls_b5ccppcld_right_power. ((((exists bpvi_h_bls_b5ccppcld_right_power_factor. bpvi_h_bls_b5ccppcld_right_power_factor + S (bpvi_factor_bls_b5ccppcld_right_power) = S ((S (bpvi_j_bls_b5ccppcld_right_power)) * bpvi_c_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_factor. bpvi_b_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_factor * S ((S (bpvi_j_bls_b5ccppcld_right_power)) * bpvi_c_bls_b5ccppcld_right_power) + (bpvi_factor_bls_b5ccppcld_right_power))) /\ ((((exists bpvi_h_bls_b5ccppcld_right_power_partial. bpvi_h_bls_b5ccppcld_right_power_partial + S (bpvi_partial_bls_b5ccppcld_right_power) = S ((S (bpvi_j_bls_b5ccppcld_right_power)) * bpvi_v_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_partial. bpvi_u_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_partial * S ((S (bpvi_j_bls_b5ccppcld_right_power)) * bpvi_v_bls_b5ccppcld_right_power) + (bpvi_partial_bls_b5ccppcld_right_power))) /\ ((((exists bpvi_h_bls_b5ccppcld_right_power_successor. bpvi_h_bls_b5ccppcld_right_power_successor + S (bpvi_successor_bls_b5ccppcld_right_power) = S ((S (S bpvi_j_bls_b5ccppcld_right_power)) * bpvi_v_bls_b5ccppcld_right_power)) /\ exists bpvi_q_bls_b5ccppcld_right_power_successor. bpvi_u_bls_b5ccppcld_right_power = bpvi_q_bls_b5ccppcld_right_power_successor * S ((S (S bpvi_j_bls_b5ccppcld_right_power)) * bpvi_v_bls_b5ccppcld_right_power) + (bpvi_successor_bls_b5ccppcld_right_power))) /\ bpvi_successor_bls_b5ccppcld_right_power = bpvi_partial_bls_b5ccppcld_right_power * bpvi_factor_bls_b5ccppcld_right_power)))))))) /\ ((((exists ff_h_bls_b5ccppcld_right_quotient_entry. ff_h_bls_b5ccppcld_right_quotient_entry + S (bls_quotient_b5ccppcld_right) = S ((S (bls_index_b5ccppcld_right)) * t)) /\ exists ff_q_bls_b5ccppcld_right_quotient_entry. d = ff_q_bls_b5ccppcld_right_quotient_entry * S ((S (bls_index_b5ccppcld_right)) * t) + (bls_quotient_b5ccppcld_right))) /\ ((n + n = bls_power_b5ccppcld_right * bls_quotient_b5ccppcld_right + bls_remainder_b5ccppcld_right /\ exists bls_remainder_gap_b5ccppcld_right_division. bls_remainder_gap_b5ccppcld_right_division + S (bls_remainder_b5ccppcld_right) = bls_power_b5ccppcld_right))))) /\ ((forall b5cc_index_b5ccppcld_carries. (exists bcf_lt_gap_b5ccppcld_carries_bound. bcf_lt_gap_b5ccppcld_carries_bound + S (b5cc_index_b5ccppcld_carries) = n + n) -> exists b5cc_left_b5ccppcld_carries b5cc_right_b5ccppcld_carries b5cc_bit_b5ccppcld_carries. (((exists fs_h_b5cc_b5ccppcld_carries_left. fs_h_b5cc_b5ccppcld_carries_left + S (b5cc_left_b5ccppcld_carries) = S ((S (b5cc_index_b5ccppcld_carries)) * s)) /\ exists fs_q_b5cc_b5ccppcld_carries_left. b = fs_q_b5cc_b5ccppcld_carries_left * S ((S (b5cc_index_b5ccppcld_carries)) * s) + (b5cc_left_b5ccppcld_carries))) /\ ((((exists fs_h_b5cc_b5ccppcld_carries_right. fs_h_b5cc_b5ccppcld_carries_right + S (b5cc_right_b5ccppcld_carries) = S ((S (b5cc_index_b5ccppcld_carries)) * t)) /\ exists fs_q_b5cc_b5ccppcld_carries_right. d = fs_q_b5cc_b5ccppcld_carries_right * S ((S (b5cc_index_b5ccppcld_carries)) * t) + (b5cc_right_b5ccppcld_carries))) /\ ((((exists fs_h_b5cc_b5ccppcld_carries_bit. fs_h_b5cc_b5ccppcld_carries_bit + S (b5cc_bit_b5ccppcld_carries) = S ((S (b5cc_index_b5ccppcld_carries)) * g)) /\ exists fs_q_b5cc_b5ccppcld_carries_bit. f = fs_q_b5cc_b5ccppcld_carries_bit * S ((S (b5cc_index_b5ccppcld_carries)) * g) + (b5cc_bit_b5ccppcld_carries))) /\ (((b5cc_bit_b5ccppcld_carries = 0 /\ b5cc_right_b5ccppcld_carries = b5cc_left_b5ccppcld_carries + b5cc_left_b5ccppcld_carries) \/ (b5cc_bit_b5ccppcld_carries = 1 /\ b5cc_right_b5ccppcld_carries = S (b5cc_left_b5ccppcld_carries + b5cc_left_b5ccppcld_carries))))))) /\ (((exists ff_u_b5ccppcld_count_sum ff_v_b5ccppcld_count_sum. ((((exists ff_h_b5ccppcld_count_sum_start. ff_h_b5ccppcld_count_sum_start + S (0) = S ((S (0)) * ff_v_b5ccppcld_count_sum)) /\ exists ff_q_b5ccppcld_count_sum_start. ff_u_b5ccppcld_count_sum = ff_q_b5ccppcld_count_sum_start * S ((S (0)) * ff_v_b5ccppcld_count_sum) + (0))) /\ ((((exists ff_h_b5ccppcld_count_sum_terminal. ff_h_b5ccppcld_count_sum_terminal + S ((S v)) = S ((S ((n + n))) * ff_v_b5ccppcld_count_sum)) /\ exists ff_q_b5ccppcld_count_sum_terminal. ff_u_b5ccppcld_count_sum = ff_q_b5ccppcld_count_sum_terminal * S ((S ((n + n))) * ff_v_b5ccppcld_count_sum) + ((S v)))) /\ forall ff_i_b5ccppcld_count_sum. (exists ff_lt_b5ccppcld_count_sum_bound. ff_lt_b5ccppcld_count_sum_bound + S ff_i_b5ccppcld_count_sum = (n + n)) -> exists ff_a_b5ccppcld_count_sum ff_r_b5ccppcld_count_sum ff_s_b5ccppcld_count_sum. ((((exists ff_h_b5ccppcld_count_sum_summand. ff_h_b5ccppcld_count_sum_summand + S (ff_a_b5ccppcld_count_sum) = S ((S (ff_i_b5ccppcld_count_sum)) * g)) /\ exists ff_q_b5ccppcld_count_sum_summand. f = ff_q_b5ccppcld_count_sum_summand * S ((S (ff_i_b5ccppcld_count_sum)) * g) + (ff_a_b5ccppcld_count_sum))) /\ ((((exists ff_h_b5ccppcld_count_sum_partial. ff_h_b5ccppcld_count_sum_partial + S (ff_r_b5ccppcld_count_sum) = S ((S (ff_i_b5ccppcld_count_sum)) * ff_v_b5ccppcld_count_sum)) /\ exists ff_q_b5ccppcld_count_sum_partial. ff_u_b5ccppcld_count_sum = ff_q_b5ccppcld_count_sum_partial * S ((S (ff_i_b5ccppcld_count_sum)) * ff_v_b5ccppcld_count_sum) + (ff_r_b5ccppcld_count_sum))) /\ ((((exists ff_h_b5ccppcld_count_sum_successor. ff_h_b5ccppcld_count_sum_successor + S (ff_s_b5ccppcld_count_sum) = S ((S (S ff_i_b5ccppcld_count_sum)) * ff_v_b5ccppcld_count_sum)) /\ exists ff_q_b5ccppcld_count_sum_successor. ff_u_b5ccppcld_count_sum = ff_q_b5ccppcld_count_sum_successor * S ((S (S ff_i_b5ccppcld_count_sum)) * ff_v_b5ccppcld_count_sum) + (ff_s_b5ccppcld_count_sum))) /\ ff_s_b5ccppcld_count_sum = ff_r_b5ccppcld_count_sum + ff_a_b5ccppcld_count_sum)))))) /\ (forall ff_i_b5ccppcld_count_bits. (exists ff_lt_b5ccppcld_count_bits_bound. ff_lt_b5ccppcld_count_bits_bound + S ff_i_b5ccppcld_count_bits = (n + n)) -> exists ff_bit_b5ccppcld_count_bits. ((((exists ff_h_b5ccppcld_count_bits_decoded. ff_h_b5ccppcld_count_bits_decoded + S (ff_bit_b5ccppcld_count_bits) = S ((S (ff_i_b5ccppcld_count_bits)) * g)) /\ exists ff_q_b5ccppcld_count_bits_decoded. f = ff_q_b5ccppcld_count_bits_decoded * S ((S (ff_i_b5ccppcld_count_bits)) * g) + (ff_bit_b5ccppcld_count_bits))) /\ (ff_bit_b5ccppcld_count_bits = 0 \/ ff_bit_b5ccppcld_count_bits = 1)))))))
  38. 0038specialize central_binom_carry_bit_count p
  39. 0039specialize central_binom_carry_bit_count n
  40. 0040specialize central_binom_carry_bit_count C
  41. 0041specialize central_binom_carry_bit_count (S v)
  42. 0042apply central_binom_carry_bit_count
  43. 0043exact hp
  44. 0044exact hcentral
  45. 0045exact hvaluation
  46. 0046cases hpackage
  47. 0047cases hpackage_witness
  48. 0048cases hpackage_witness_witness
  49. 0049cases hpackage_witness_witness_witness
  50. 0050cases hpackage_witness_witness_witness_witness
  51. 0051cases hpackage_witness_witness_witness_witness_witness
  52. 0052cases hpackage_witness_witness_witness_witness_witness_witness
  53. 0053cases hpackage_witness_witness_witness_witness_witness_witness_right
  54. 0054cases hpackage_witness_witness_witness_witness_witness_witness_right_right
  55. 0055have hlast : exists i. (exists bcf_lt_gap_b5ccppcld_last_bound. bcf_lt_gap_b5ccppcld_last_bound + S (i) = n + n) /\ ((((exists fs_h_b5ccppcld_last_entry. fs_h_b5ccppcld_last_entry + S (1) = S ((S (i)) * x5)) /\ exists fs_q_b5ccppcld_last_entry. x4 = fs_q_b5ccppcld_last_entry * S ((S (i)) * x5) + (1))) /\ (exists bcf_le_gap_b5ccppcld_last_result. bcf_le_gap_b5ccppcld_last_result + (S v) = S i))
  56. 0056specialize bit_count_positive_last_one x4
  57. 0057specialize bit_count_positive_last_one x5
  58. 0058specialize bit_count_positive_last_one (n + n)
  59. 0059specialize bit_count_positive_last_one v
  60. 0060apply bit_count_positive_last_one
  61. 0061exact hpackage_witness_witness_witness_witness_witness_witness_right_right_right
  62. 0062cases hlast
  63. 0063cases hlast_witness
  64. 0064cases hlast_witness_right
  65. 0065have hsemantic : exists q Q bit. (((exists fs_h_b5ccppcld_semantic_left. fs_h_b5ccppcld_semantic_left + S (q) = S ((S (x6)) * x1)) /\ exists fs_q_b5ccppcld_semantic_left. x = fs_q_b5ccppcld_semantic_left * S ((S (x6)) * x1) + (q))) /\ ((((exists fs_h_b5ccppcld_semantic_right. fs_h_b5ccppcld_semantic_right + S (Q) = S ((S (x6)) * x3)) /\ exists fs_q_b5ccppcld_semantic_right. x2 = fs_q_b5ccppcld_semantic_right * S ((S (x6)) * x3) + (Q))) /\ ((((exists fs_h_b5ccppcld_semantic_bit. fs_h_b5ccppcld_semantic_bit + S (bit) = S ((S (x6)) * x5)) /\ exists fs_q_b5ccppcld_semantic_bit. x4 = fs_q_b5ccppcld_semantic_bit * S ((S (x6)) * x5) + (bit))) /\ (((bit = 0 /\ Q = q + q) \/ (bit = 1 /\ Q = S (q + q))))))
  66. 0066specialize hpackage_witness_witness_witness_witness_witness_witness_right_right_left x6
  67. 0067apply hpackage_witness_witness_witness_witness_witness_witness_right_right_left
  68. 0068exact hlast_witness_left
  69. 0069cases hsemantic
  70. 0070cases hsemantic_witness
  71. 0071cases hsemantic_witness_witness
  72. 0072cases hsemantic_witness_witness_witness
  73. 0073cases hsemantic_witness_witness_witness_right
  74. 0074cases hsemantic_witness_witness_witness_right_right
  75. 0075have hbit : x9 = 1
  76. 0076specialize beta_at_unique x4
  77. 0077specialize beta_at_unique x5
  78. 0078specialize beta_at_unique x6
  79. 0079specialize beta_at_unique x9
  80. 0080specialize beta_at_unique 1
  81. 0081apply beta_at_unique
  82. 0082exact hsemantic_witness_witness_witness_right_right_left
  83. 0083exact hlast_witness_right_left
  84. 0084rewrite hbit at hsemantic_witness_witness_witness_right_right_right
  85. 0085rewrite hbit at hsemantic_witness_witness_witness_right_right_right
  86. 0086cases hsemantic_witness_witness_witness_right_right_right
  87. 0087cases hsemantic_witness_witness_witness_right_right_right_left
  88. 0088exfalso
  89. 0089apply PA1
  90. 0090exact hsemantic_witness_witness_witness_right_right_right_left_left
  91. 0091cases hsemantic_witness_witness_witness_right_right_right_right
  92. 0092have hright_data : exists P Q R. (exists bpvi_b_b5ccppcld_right_power bpvi_c_b5ccppcld_right_power. ((forall bpvi_i_b5ccppcld_right_power. (exists bpvi_repeat_gap_b5ccppcld_right_power. bpvi_repeat_gap_b5ccppcld_right_power + S bpvi_i_b5ccppcld_right_power = S x6) -> (((exists bpvi_h_b5ccppcld_right_power_repeat. bpvi_h_b5ccppcld_right_power_repeat + S (p) = S ((S (bpvi_i_b5ccppcld_right_power)) * bpvi_c_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_repeat. bpvi_b_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_repeat * S ((S (bpvi_i_b5ccppcld_right_power)) * bpvi_c_b5ccppcld_right_power) + (p)))) /\ (exists bpvi_u_b5ccppcld_right_power bpvi_v_b5ccppcld_right_power. ((((exists bpvi_h_b5ccppcld_right_power_start. bpvi_h_b5ccppcld_right_power_start + S (1) = S ((S (0)) * bpvi_v_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_start. bpvi_u_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_start * S ((S (0)) * bpvi_v_b5ccppcld_right_power) + (1))) /\ ((((exists bpvi_h_b5ccppcld_right_power_terminal. bpvi_h_b5ccppcld_right_power_terminal + S (P) = S ((S (S x6)) * bpvi_v_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_terminal. bpvi_u_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_terminal * S ((S (S x6)) * bpvi_v_b5ccppcld_right_power) + (P))) /\ forall bpvi_j_b5ccppcld_right_power. (exists bpvi_product_gap_b5ccppcld_right_power. bpvi_product_gap_b5ccppcld_right_power + S bpvi_j_b5ccppcld_right_power = S x6) -> exists bpvi_factor_b5ccppcld_right_power bpvi_partial_b5ccppcld_right_power bpvi_successor_b5ccppcld_right_power. ((((exists bpvi_h_b5ccppcld_right_power_factor. bpvi_h_b5ccppcld_right_power_factor + S (bpvi_factor_b5ccppcld_right_power) = S ((S (bpvi_j_b5ccppcld_right_power)) * bpvi_c_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_factor. bpvi_b_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_factor * S ((S (bpvi_j_b5ccppcld_right_power)) * bpvi_c_b5ccppcld_right_power) + (bpvi_factor_b5ccppcld_right_power))) /\ ((((exists bpvi_h_b5ccppcld_right_power_partial. bpvi_h_b5ccppcld_right_power_partial + S (bpvi_partial_b5ccppcld_right_power) = S ((S (bpvi_j_b5ccppcld_right_power)) * bpvi_v_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_partial. bpvi_u_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_partial * S ((S (bpvi_j_b5ccppcld_right_power)) * bpvi_v_b5ccppcld_right_power) + (bpvi_partial_b5ccppcld_right_power))) /\ ((((exists bpvi_h_b5ccppcld_right_power_successor. bpvi_h_b5ccppcld_right_power_successor + S (bpvi_successor_b5ccppcld_right_power) = S ((S (S bpvi_j_b5ccppcld_right_power)) * bpvi_v_b5ccppcld_right_power)) /\ exists bpvi_q_b5ccppcld_right_power_successor. bpvi_u_b5ccppcld_right_power = bpvi_q_b5ccppcld_right_power_successor * S ((S (S bpvi_j_b5ccppcld_right_power)) * bpvi_v_b5ccppcld_right_power) + (bpvi_successor_b5ccppcld_right_power))) /\ bpvi_successor_b5ccppcld_right_power = bpvi_partial_b5ccppcld_right_power * bpvi_factor_b5ccppcld_right_power)))))))) /\ ((((exists fs_h_b5ccppcld_right_entry. fs_h_b5ccppcld_right_entry + S (Q) = S ((S (x6)) * x3)) /\ exists fs_q_b5ccppcld_right_entry. x2 = fs_q_b5ccppcld_right_entry * S ((S (x6)) * x3) + (Q))) /\ (((n + n) = (P) * (Q) + (R) /\ (exists bcf_lt_gap_b5ccppcld_right_division_bound. bcf_lt_gap_b5ccppcld_right_division_bound + S (R) = P))))
  93. 0093specialize hpackage_witness_witness_witness_witness_witness_witness_right_left x6
  94. 0094apply hpackage_witness_witness_witness_witness_witness_witness_right_left
  95. 0095exact hlast_witness_left
  96. 0096cases hright_data
  97. 0097cases hright_data_witness
  98. 0098cases hright_data_witness_witness
  99. 0099cases hright_data_witness_witness_witness
  100. 0100cases hright_data_witness_witness_witness_right
  101. 0101have hQ : x8 = x11
  102. 0102specialize beta_at_unique x2
  103. 0103specialize beta_at_unique x3
  104. 0104specialize beta_at_unique x6
  105. 0105specialize beta_at_unique x8
  106. 0106specialize beta_at_unique x11
  107. 0107apply beta_at_unique
  108. 0108exact hsemantic_witness_witness_witness_right_left
  109. 0109exact hright_data_witness_witness_witness_right_left
  110. 0110have hquotient : x11 = S (x7 + x7)
  111. 0111trans x8
  112. 0112symm
  113. 0113exact hQ
  114. 0114exact hsemantic_witness_witness_witness_right_right_right_right_right
  115. 0115rewrite hquotient at hright_data_witness_witness_witness_right_right
  116. 0116have hdivisor_bound : exists bcf_le_gap_b5ccppcld_divisor_bound. bcf_le_gap_b5ccppcld_divisor_bound + (x10) = n + n
  117. 0117specialize division_successor_quotient_divisor_le x10
  118. 0118specialize division_successor_quotient_divisor_le (n + n)
  119. 0119specialize division_successor_quotient_divisor_le (x7 + x7)
  120. 0120specialize division_successor_quotient_divisor_le x12
  121. 0121apply division_successor_quotient_divisor_le
  122. 0122exact hright_data_witness_witness_witness_right_right
  123. 0123have hp0 : ~(p = 0)
  124. 0124intro hpzero
  125. 0125specialize prime_nonzero p
  126. 0126apply prime_nonzero
  127. 0127exact hp
  128. 0128exact hpzero
  129. 0129have hp1 : exists k. k + 1 = p
  130. 0130specialize one_le_of_ne_zero p
  131. 0131apply one_le_of_ne_zero
  132. 0132exact hp0
  133. 0133have hpower_bound : exists bcf_le_gap_b5ccppcld_power_bound. bcf_le_gap_b5ccppcld_power_bound + (D) = x10
  134. 0134specialize pow_le_pow_of_exponent_le p
  135. 0135specialize pow_le_pow_of_exponent_le (S v)
  136. 0136specialize pow_le_pow_of_exponent_le (S x6)
  137. 0137specialize pow_le_pow_of_exponent_le D
  138. 0138specialize pow_le_pow_of_exponent_le x10
  139. 0139apply pow_le_pow_of_exponent_le
  140. 0140exact hp1
  141. 0141exact hlast_witness_right_right
  142. 0142exact hpower
  143. 0143exact hright_data_witness_witness_witness_left
  144. 0144specialize le_trans D
  145. 0145specialize le_trans x10
  146. 0146specialize le_trans (n + n)
  147. 0147apply le_trans
  148. 0148exact hpower_bound
  149. 0149exact hdivisor_bound