BT00Y5 · Bertrand theorem

central_binom_prime_power_contribution_le_double

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ C. ∀ v. ∀ D. Prime(p) → Lt(0,n) → CentralBinom(n,C) → PowerValuation(p,C,v) → Pow(p,v,D) → Le(D,n + n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0004 Prime PD0020 Pow PD0042 CentralBinom PD0046 PowerValuation

6 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0007 DivRem PD0013 BetaAt PD0017 BitCount PD0020 Pow PD0049 PowerQuotPrefix

21 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YL no_bertrand_central_nonzero_contribution_factor_ranges

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

149 script commands · 26 reading checkpoints · 14 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (10)
pow zerole add rightle transprime nonzeroone le of ne zerobeta at uniquepow le pow of exponent lebit count positive last onedivision successor quotient divisor lecentral binom carry bit count
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro C
02Induction on vL4–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction v
  2. L5
    intro D
  3. L6
    intro hp
  4. L7
    intro hpositive
  5. L8
    intro hcentral
  6. L9
    intro hvaluation
  7. L10
    intro hpower
03Establish hDL11–17

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

  1. L11
    have hD : D = 1
  2. L12
    specialize pow_zero p
  3. L13
    specialize pow_zero 0
  4. L14
    specialize pow_zero D
  5. L15
    apply pow_zero
  6. L16
    refl
  7. L17
    exact hpower
04Establish hn_doubleL18–21

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

  1. L18
    have hn_double : Le(n,n + n)Definitions: Le(n,n + n)Original native command in the exact edition
  2. L19
    specialize le_add_right n
  3. L20
    specialize le_add_right n
  4. L21
    exact le_add_right
05Establish hone_doubleL22–31

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

  1. L22
    have hone_double : Lt(0,n + n)Definitions: Lt(0,n + n)Original native command in the exact edition
  2. L23
    specialize le_trans 1
  3. L24
    specialize le_trans n
  4. L25
    specialize le_trans (n + n)
  5. L26
    apply le_trans
  6. L27
    exact hpositive
  7. L28
    exact hn_double
  8. L29
    rewrite hD
  9. L30
    exact hone_double
  10. L31
    intro D
06Fix variables and assumptionsL32–36

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

  1. L32
    intro hp
  2. L33
    intro hpositive
  3. L34
    intro hcentral
  4. L35
    intro hvaluation
  5. L36
    intro hpower
07Establish hpackageL37–45

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

  1. L37
    have hpackage : ∃ b. ∃ s. ∃ d. ∃ t. ∃ f. ∃ g. PowerQuotPrefix(p,n,b,s,n + n) ∧ (PowerQuotPrefix(p,n + n,d,t,n + n) ∧ ((∀ x. Lt(x,n + n) → ∃ y. ∃ z. ∃ m. BetaAt(b,s,x,y) ∧ (BetaAt(d,t,x,z) ∧ (BetaAt(f,g,x,m) ∧ (m = 0 ∧ z = y + y ∨ m = 1 ∧ z = S (y + y))))) ∧ BitCount(f,g,n + n,S v)))Definitions: PowerQuotPrefix(p,n,b,s,n + n)PowerQuotPrefix(p,n + n,d,t,n + n)Lt(x,n + n)BetaAt(b,s,x,y)BetaAt(d,t,x,z)BetaAt(f,g,x,m)BitCount(f,g,n + n,S v)Original native command in the exact edition
  2. L38
    specialize central_binom_carry_bit_count p
  3. L39
    specialize central_binom_carry_bit_count n
  4. L40
    specialize central_binom_carry_bit_count C
  5. L41
    specialize central_binom_carry_bit_count (S v)
  6. L42
    apply central_binom_carry_bit_count
  7. L43
    exact hp
  8. L44
    exact hcentral
  9. L45
    exact hvaluation
08Separate the logical casesL46–54

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

  1. L46
    cases hpackage
  2. L47
    cases hpackage_witness
  3. L48
    cases hpackage_witness_witness
  4. L49
    cases hpackage_witness_witness_witness
  5. L50
    cases hpackage_witness_witness_witness_witness
  6. L51
    cases hpackage_witness_witness_witness_witness_witness
  7. L52
    cases hpackage_witness_witness_witness_witness_witness_witness
  8. L53
    cases hpackage_witness_witness_witness_witness_witness_witness_right
  9. L54
    cases hpackage_witness_witness_witness_witness_witness_witness_right_right
09Establish hlastL55–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count positive last one.

  1. L55
    have hlast : ∃ i. Lt(i,n + n) ∧ (BetaAt(x4,x5,i,1) ∧ Lt(v,S i))Definitions: Lt(i,n + n)BetaAt(x4,x5,i,1)Lt(v,S i)Original native command in the exact edition
  2. L56
    specialize bit_count_positive_last_one x4
  3. L57
    specialize bit_count_positive_last_one x5
  4. L58
    specialize bit_count_positive_last_one (n + n)
  5. L59
    specialize bit_count_positive_last_one v
  6. L60
    apply bit_count_positive_last_one
  7. L61
    exact hpackage_witness_witness_witness_witness_witness_witness_right_right_right
10Separate the logical casesL62–64

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

  1. L62
    cases hlast
  2. L63
    cases hlast_witness
  3. L64
    cases hlast_witness_right
11Establish hsemanticL65–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpackage witness witness witness witness witness witness right right left.

  1. L65
    have hsemantic : ∃ q. ∃ Q. ∃ bit. BetaAt(x,x1,x6,q) ∧ (BetaAt(x2,x3,x6,Q) ∧ (BetaAt(x4,x5,x6,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))Definitions: BetaAt(x,x1,x6,q)BetaAt(x2,x3,x6,Q)BetaAt(x4,x5,x6,bit)Original native command in the exact edition
  2. L66
    specialize hpackage_witness_witness_witness_witness_witness_witness_right_right_left x6
  3. L67
    apply hpackage_witness_witness_witness_witness_witness_witness_right_right_left
  4. L68
    exact hlast_witness_left
12Separate the logical casesL69–74

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

  1. L69
    cases hsemantic
  2. L70
    cases hsemantic_witness
  3. L71
    cases hsemantic_witness_witness
  4. L72
    cases hsemantic_witness_witness_witness
  5. L73
    cases hsemantic_witness_witness_witness_right
  6. L74
    cases hsemantic_witness_witness_witness_right_right
13Establish hbitL75–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L75
    have hbit : x9 = 1
  2. L76
    specialize beta_at_unique x4
  3. L77
    specialize beta_at_unique x5
  4. L78
    specialize beta_at_unique x6
  5. L79
    specialize beta_at_unique x9
  6. L80
    specialize beta_at_unique 1
  7. L81
    apply beta_at_unique
  8. L82
    exact hsemantic_witness_witness_witness_right_right_left
  9. L83
    exact hlast_witness_right_left
  10. L84
    rewrite hbit at hsemantic_witness_witness_witness_right_right_right
14Calculate and transport equalitiesL85–85

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

  1. L85
    rewrite hbit at hsemantic_witness_witness_witness_right_right_right
15Separate the logical casesL86–88

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

  1. L86
    cases hsemantic_witness_witness_witness_right_right_right
  2. L87
    cases hsemantic_witness_witness_witness_right_right_right_left
  3. L88
    exfalso
16Use earlier factsL89–90

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

  1. L89
    apply PA1
  2. L90
    exact hsemantic_witness_witness_witness_right_right_right_left_left
17Separate the logical casesL91–91

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

  1. L91
    cases hsemantic_witness_witness_witness_right_right_right_right
18Establish hright_dataL92–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpackage witness witness witness witness witness witness right left.

  1. L92
    have hright_data : ∃ P. ∃ Q. ∃ R. Pow(p,S x6,P) ∧ (BetaAt(x2,x3,x6,Q) ∧ DivRem(n + n,P,Q,R))Definitions: Pow(p,S x6,P)BetaAt(x2,x3,x6,Q)DivRem(n + n,P,Q,R)Original native command in the exact edition
  2. L93
    specialize hpackage_witness_witness_witness_witness_witness_witness_right_left x6
  3. L94
    apply hpackage_witness_witness_witness_witness_witness_witness_right_left
  4. L95
    exact hlast_witness_left
19Separate the logical casesL96–100

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

  1. L96
    cases hright_data
  2. L97
    cases hright_data_witness
  3. L98
    cases hright_data_witness_witness
  4. L99
    cases hright_data_witness_witness_witness
  5. L100
    cases hright_data_witness_witness_witness_right
20Establish hQL101–109

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L101
    have hQ : x8 = x11
  2. L102
    specialize beta_at_unique x2
  3. L103
    specialize beta_at_unique x3
  4. L104
    specialize beta_at_unique x6
  5. L105
    specialize beta_at_unique x8
  6. L106
    specialize beta_at_unique x11
  7. L107
    apply beta_at_unique
  8. L108
    exact hsemantic_witness_witness_witness_right_left
  9. L109
    exact hright_data_witness_witness_witness_right_left
21Establish hquotientL110–115

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

  1. L110
    have hquotient : x11 = S (x7 + x7)
  2. L111
    trans x8
  3. L112
    symm
  4. L113
    exact hQ
  5. L114
    exact hsemantic_witness_witness_witness_right_right_right_right_right
  6. L115
    rewrite hquotient at hright_data_witness_witness_witness_right_right
22Establish hdivisor_boundL116–122

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

  1. L116
    have hdivisor_bound : Le(x10,n + n)Definitions: Le(x10,n + n)Original native command in the exact edition
  2. L117
    specialize division_successor_quotient_divisor_le x10
  3. L118
    specialize division_successor_quotient_divisor_le (n + n)
  4. L119
    specialize division_successor_quotient_divisor_le (x7 + x7)
  5. L120
    specialize division_successor_quotient_divisor_le x12
  6. L121
    apply division_successor_quotient_divisor_le
  7. L122
    exact hright_data_witness_witness_witness_right_right
23Establish hp0L123–128

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

  1. L123
    have hp0 : ~(p = 0)
  2. L124
    intro hpzero
  3. L125
    specialize prime_nonzero p
  4. L126
    apply prime_nonzero
  5. L127
    exact hp
  6. L128
    exact hpzero
24Establish hp1L129–132

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

  1. L129
  2. L130
    specialize one_le_of_ne_zero p
  3. L131
    apply one_le_of_ne_zero
  4. L132
    exact hp0
25Establish hpower_boundL133–142

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

  1. L133
    have hpower_bound : Le(D,x10)Definitions: Le(D,x10)Original native command in the exact edition
  2. L134
    specialize pow_le_pow_of_exponent_le p
  3. L135
    specialize pow_le_pow_of_exponent_le (S v)
  4. L136
    specialize pow_le_pow_of_exponent_le (S x6)
  5. L137
    specialize pow_le_pow_of_exponent_le D
  6. L138
    specialize pow_le_pow_of_exponent_le x10
  7. L139
    apply pow_le_pow_of_exponent_le
  8. L140
    exact hp1
  9. L141
    exact hlast_witness_right_right
  10. L142
    exact hpower
26Use earlier factsL143–149

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

  1. L143
    exact hright_data_witness_witness_witness_left
  2. L144
    specialize le_trans D
  3. L145
    specialize le_trans x10
  4. L146
    specialize le_trans (n + n)
  5. L147
    apply le_trans
  6. L148
    exact hpower_bound
  7. L149
    exact hdivisor_bound

Library-wide reading audit

Original defined command ledger · 149 lines
  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 : Le(n,n + n)
    Exact native replay linehave 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 : Lt(0,n + n)
    Exact native replay linehave 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 : ∃ b. ∃ s. ∃ d. ∃ t. ∃ f. ∃ g. PowerQuotPrefix(p,n,b,s,n + n) ∧ (PowerQuotPrefix(p,n + n,d,t,n + n) ∧ ((∀ x. Lt(x,n + n) → ∃ y. ∃ z. ∃ m. BetaAt(b,s,x,y) ∧ (BetaAt(d,t,x,z) ∧ (BetaAt(f,g,x,m) ∧ (m = 0 ∧ z = y + y ∨ m = 1 ∧ z = S (y + y))))) ∧ BitCount(f,g,n + n,S v)))
    Exact native replay linehave 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 : ∃ i. Lt(i,n + n) ∧ (BetaAt(x4,x5,i,1) ∧ Lt(v,S i))
    Exact native replay linehave 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 : ∃ q. ∃ Q. ∃ bit. BetaAt(x,x1,x6,q) ∧ (BetaAt(x2,x3,x6,Q) ∧ (BetaAt(x4,x5,x6,bit) ∧ (bit = 0 ∧ Q = q + q ∨ bit = 1 ∧ Q = S (q + q))))
    Exact native replay linehave 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 : ∃ P. ∃ Q. ∃ R. Pow(p,S x6,P) ∧ (BetaAt(x2,x3,x6,Q) ∧ DivRem(n + n,P,Q,R))
    Exact native replay linehave 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 : Le(x10,n + n)
    Exact native replay linehave 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 : Lt(0,p)
    Exact native replay linehave 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 : Le(D,x10)
    Exact native replay linehave 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