MK0006

beta_prime_product_valuation_eq_sum

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

For a prime and any nonzero finite factor list, the exact product valuation equals the finite sum of its actual factor valuations.

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

Exact expanded first-order arithmetic statement

forall p b c vb vc l z e g. ((~(p = 1) /\ forall frm_prime_left_mkm_product_prime frm_prime_right_mkm_product_prime. p = frm_prime_left_mkm_product_prime * frm_prime_right_mkm_product_prime -> frm_prime_left_mkm_product_prime = 1 \/ frm_prime_right_mkm_product_prime = 1)) -> (forall gcrt_positive_index_mkm_product_nonzero gcrt_positive_value_mkm_product_nonzero. (exists ff_lt_gcrt_mkm_product_nonzero_bound. ff_lt_gcrt_mkm_product_nonzero_bound + S gcrt_positive_index_mkm_product_nonzero = l) -> (((exists ff_h_gcrt_mkm_product_nonzero_entry. ff_h_gcrt_mkm_product_nonzero_entry + S (gcrt_positive_value_mkm_product_nonzero) = S ((S (gcrt_positive_index_mkm_product_nonzero)) * c)) /\ exists ff_q_gcrt_mkm_product_nonzero_entry. b = ff_q_gcrt_mkm_product_nonzero_entry * S ((S (gcrt_positive_index_mkm_product_nonzero)) * c) + (gcrt_positive_value_mkm_product_nonzero))) -> ~(gcrt_positive_value_mkm_product_nonzero = 0)) -> (forall mkm_index_product_valuations. (exists mkm_lt_product_valuations_bound. mkm_lt_product_valuations_bound + S (mkm_index_product_valuations) = (l)) -> (exists mkm_value_product_valuations_point mkm_exponent_product_valuations_point. (((exists fs_h_mkm_product_valuations_point_source. fs_h_mkm_product_valuations_point_source + S (mkm_value_product_valuations_point) = S ((S (mkm_index_product_valuations)) * c)) /\ exists fs_q_mkm_product_valuations_point_source. b = fs_q_mkm_product_valuations_point_source * S ((S (mkm_index_product_valuations)) * c) + (mkm_value_product_valuations_point))) /\ ((((exists fs_h_mkm_product_valuations_point_decoded. fs_h_mkm_product_valuations_point_decoded + S (mkm_exponent_product_valuations_point) = S ((S (mkm_index_product_valuations)) * vc)) /\ exists fs_q_mkm_product_valuations_point_decoded. vb = fs_q_mkm_product_valuations_point_decoded * S ((S (mkm_index_product_valuations)) * vc) + (mkm_exponent_product_valuations_point))) /\ (((exists bpv_gap_mkm_product_valuations_point_valuation_exponent_bound. bpv_gap_mkm_product_valuations_point_valuation_exponent_bound + mkm_exponent_product_valuations_point = (mkm_value_product_valuations_point)) /\ (exists bpv_result_mkm_product_valuations_point_valuation_selected. ((exists ff_b_mkm_product_valuations_point_valuation_selected_power ff_c_mkm_product_valuations_point_valuation_selected_power. ((forall ff_i_mkm_product_valuations_point_valuation_selected_power_repeat. (exists ff_lt_mkm_product_valuations_point_valuation_selected_power_repeat_bound. ff_lt_mkm_product_valuations_point_valuation_selected_power_repeat_bound + S ff_i_mkm_product_valuations_point_valuation_selected_power_repeat = mkm_exponent_product_valuations_point) -> (((exists ff_h_mkm_product_valuations_point_valuation_selected_power_repeat_decoded. ff_h_mkm_product_valuations_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_selected_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_repeat_decoded. ff_b_mkm_product_valuations_point_valuation_selected_power = ff_q_mkm_product_valuations_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_product_valuations_point_valuation_selected_power_product ff_v_mkm_product_valuations_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_start. ff_h_mkm_product_valuations_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_start. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_terminal. ff_h_mkm_product_valuations_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_product_valuations_point_valuation_selected) = S ((S (mkm_exponent_product_valuations_point)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_terminal. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_product_valuations_point)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (bpv_result_mkm_product_valuations_point_valuation_selected))) /\ forall ff_i_mkm_product_valuations_point_valuation_selected_power_product. (exists ff_lt_mkm_product_valuations_point_valuation_selected_power_product_bound. ff_lt_mkm_product_valuations_point_valuation_selected_power_product_bound + S ff_i_mkm_product_valuations_point_valuation_selected_power_product = mkm_exponent_product_valuations_point) -> exists ff_p_mkm_product_valuations_point_valuation_selected_power_product ff_r_mkm_product_valuations_point_valuation_selected_power_product ff_s_mkm_product_valuations_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_factor. ff_h_mkm_product_valuations_point_valuation_selected_power_product_factor + S (ff_p_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_c_mkm_product_valuations_point_valuation_selected_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_factor. ff_b_mkm_product_valuations_point_valuation_selected_power = ff_q_mkm_product_valuations_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_c_mkm_product_valuations_point_valuation_selected_power) + (ff_p_mkm_product_valuations_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_partial. ff_h_mkm_product_valuations_point_valuation_selected_power_product_partial + S (ff_r_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_partial. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (ff_r_mkm_product_valuations_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_successor. ff_h_mkm_product_valuations_point_valuation_selected_power_product_successor + S (ff_s_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_successor. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (ff_s_mkm_product_valuations_point_valuation_selected_power_product))) /\ ff_s_mkm_product_valuations_point_valuation_selected_power_product = ff_r_mkm_product_valuations_point_valuation_selected_power_product * ff_p_mkm_product_valuations_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_valuations_point_valuation_selected_divides. (mkm_value_product_valuations_point) = bpv_result_mkm_product_valuations_point_valuation_selected * bpv_factor_mkm_product_valuations_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_product_valuations_point_valuation. (exists bpv_gap_mkm_product_valuations_point_valuation_candidate_bound. bpv_gap_mkm_product_valuations_point_valuation_candidate_bound + bpv_candidate_mkm_product_valuations_point_valuation = (mkm_value_product_valuations_point)) -> (exists bpv_result_mkm_product_valuations_point_valuation_candidate. ((exists ff_b_mkm_product_valuations_point_valuation_candidate_power ff_c_mkm_product_valuations_point_valuation_candidate_power. ((forall ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_product_valuations_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_product_valuations_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat = bpv_candidate_mkm_product_valuations_point_valuation) -> (((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_product_valuations_point_valuation_candidate_power = ff_q_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_valuations_point_valuation_candidate_power_product ff_v_mkm_product_valuations_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_start. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_start. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_terminal. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_product_valuations_point_valuation_candidate) = S ((S (bpv_candidate_mkm_product_valuations_point_valuation)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_terminal. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_valuations_point_valuation)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (bpv_result_mkm_product_valuations_point_valuation_candidate))) /\ forall ff_i_mkm_product_valuations_point_valuation_candidate_power_product. (exists ff_lt_mkm_product_valuations_point_valuation_candidate_power_product_bound. ff_lt_mkm_product_valuations_point_valuation_candidate_power_product_bound + S ff_i_mkm_product_valuations_point_valuation_candidate_power_product = bpv_candidate_mkm_product_valuations_point_valuation) -> exists ff_p_mkm_product_valuations_point_valuation_candidate_power_product ff_r_mkm_product_valuations_point_valuation_candidate_power_product ff_s_mkm_product_valuations_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_factor. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_factor + S (ff_p_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_c_mkm_product_valuations_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_factor. ff_b_mkm_product_valuations_point_valuation_candidate_power = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_c_mkm_product_valuations_point_valuation_candidate_power) + (ff_p_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_partial. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_partial + S (ff_r_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_partial. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (ff_r_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_successor. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_successor + S (ff_s_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_successor. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (ff_s_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ff_s_mkm_product_valuations_point_valuation_candidate_power_product = ff_r_mkm_product_valuations_point_valuation_candidate_power_product * ff_p_mkm_product_valuations_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_valuations_point_valuation_candidate_divides. (mkm_value_product_valuations_point) = bpv_result_mkm_product_valuations_point_valuation_candidate * bpv_factor_mkm_product_valuations_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_product_valuations_point_valuation_maximal. bpv_gap_mkm_product_valuations_point_valuation_maximal + bpv_candidate_mkm_product_valuations_point_valuation = mkm_exponent_product_valuations_point))))) -> (exists ff_u_mkm_product_value ff_v_mkm_product_value. ((((exists ff_h_mkm_product_value_start. ff_h_mkm_product_value_start + S (1) = S ((S (0)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_start. ff_u_mkm_product_value = ff_q_mkm_product_value_start * S ((S (0)) * ff_v_mkm_product_value) + (1))) /\ ((((exists ff_h_mkm_product_value_terminal. ff_h_mkm_product_value_terminal + S (z) = S ((S (l)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_terminal. ff_u_mkm_product_value = ff_q_mkm_product_value_terminal * S ((S (l)) * ff_v_mkm_product_value) + (z))) /\ forall ff_i_mkm_product_value. (exists ff_lt_mkm_product_value_bound. ff_lt_mkm_product_value_bound + S ff_i_mkm_product_value = l) -> exists ff_p_mkm_product_value ff_r_mkm_product_value ff_s_mkm_product_value. ((((exists ff_h_mkm_product_value_factor. ff_h_mkm_product_value_factor + S (ff_p_mkm_product_value) = S ((S (ff_i_mkm_product_value)) * c)) /\ exists ff_q_mkm_product_value_factor. b = ff_q_mkm_product_value_factor * S ((S (ff_i_mkm_product_value)) * c) + (ff_p_mkm_product_value))) /\ ((((exists ff_h_mkm_product_value_partial. ff_h_mkm_product_value_partial + S (ff_r_mkm_product_value) = S ((S (ff_i_mkm_product_value)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_partial. ff_u_mkm_product_value = ff_q_mkm_product_value_partial * S ((S (ff_i_mkm_product_value)) * ff_v_mkm_product_value) + (ff_r_mkm_product_value))) /\ ((((exists ff_h_mkm_product_value_successor. ff_h_mkm_product_value_successor + S (ff_s_mkm_product_value) = S ((S (S ff_i_mkm_product_value)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_successor. ff_u_mkm_product_value = ff_q_mkm_product_value_successor * S ((S (S ff_i_mkm_product_value)) * ff_v_mkm_product_value) + (ff_s_mkm_product_value))) /\ ff_s_mkm_product_value = ff_r_mkm_product_value * ff_p_mkm_product_value)))))) -> (exists fs_u_mkm_product_sum fs_v_mkm_product_sum. ((((exists fs_h_mkm_product_sum_body_start. fs_h_mkm_product_sum_body_start + S (0) = S ((S (0)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_start. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_start * S ((S (0)) * fs_v_mkm_product_sum) + (0))) /\ ((((exists fs_h_mkm_product_sum_body_terminal. fs_h_mkm_product_sum_body_terminal + S (e) = S ((S (l)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_terminal. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_terminal * S ((S (l)) * fs_v_mkm_product_sum) + (e))) /\ forall fs_i_mkm_product_sum_body_steps. (exists fs_lt_mkm_product_sum_body_steps_bound. fs_lt_mkm_product_sum_body_steps_bound + S fs_i_mkm_product_sum_body_steps = l) -> exists fs_a_mkm_product_sum_body_steps fs_r_mkm_product_sum_body_steps fs_s_mkm_product_sum_body_steps. ((((exists fs_h_mkm_product_sum_body_steps_summand. fs_h_mkm_product_sum_body_steps_summand + S (fs_a_mkm_product_sum_body_steps) = S ((S (fs_i_mkm_product_sum_body_steps)) * vc)) /\ exists fs_q_mkm_product_sum_body_steps_summand. vb = fs_q_mkm_product_sum_body_steps_summand * S ((S (fs_i_mkm_product_sum_body_steps)) * vc) + (fs_a_mkm_product_sum_body_steps))) /\ ((((exists fs_h_mkm_product_sum_body_steps_partial. fs_h_mkm_product_sum_body_steps_partial + S (fs_r_mkm_product_sum_body_steps) = S ((S (fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_steps_partial. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_steps_partial * S ((S (fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum) + (fs_r_mkm_product_sum_body_steps))) /\ ((((exists fs_h_mkm_product_sum_body_steps_successor. fs_h_mkm_product_sum_body_steps_successor + S (fs_s_mkm_product_sum_body_steps) = S ((S (S fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_steps_successor. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_steps_successor * S ((S (S fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum) + (fs_s_mkm_product_sum_body_steps))) /\ fs_s_mkm_product_sum_body_steps = fs_r_mkm_product_sum_body_steps + fs_a_mkm_product_sum_body_steps)))))) -> (((exists bpv_gap_mkm_product_val_exponent_bound. bpv_gap_mkm_product_val_exponent_bound + g = (z)) /\ (exists bpv_result_mkm_product_val_selected. ((exists ff_b_mkm_product_val_selected_power ff_c_mkm_product_val_selected_power. ((forall ff_i_mkm_product_val_selected_power_repeat. (exists ff_lt_mkm_product_val_selected_power_repeat_bound. ff_lt_mkm_product_val_selected_power_repeat_bound + S ff_i_mkm_product_val_selected_power_repeat = g) -> (((exists ff_h_mkm_product_val_selected_power_repeat_decoded. ff_h_mkm_product_val_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_val_selected_power_repeat)) * ff_c_mkm_product_val_selected_power)) /\ exists ff_q_mkm_product_val_selected_power_repeat_decoded. ff_b_mkm_product_val_selected_power = ff_q_mkm_product_val_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_val_selected_power_repeat)) * ff_c_mkm_product_val_selected_power) + (p)))) /\ (exists ff_u_mkm_product_val_selected_power_product ff_v_mkm_product_val_selected_power_product. ((((exists ff_h_mkm_product_val_selected_power_product_start. ff_h_mkm_product_val_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_start. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_val_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_terminal. ff_h_mkm_product_val_selected_power_product_terminal + S (bpv_result_mkm_product_val_selected) = S ((S (g)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_terminal. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_terminal * S ((S (g)) * ff_v_mkm_product_val_selected_power_product) + (bpv_result_mkm_product_val_selected))) /\ forall ff_i_mkm_product_val_selected_power_product. (exists ff_lt_mkm_product_val_selected_power_product_bound. ff_lt_mkm_product_val_selected_power_product_bound + S ff_i_mkm_product_val_selected_power_product = g) -> exists ff_p_mkm_product_val_selected_power_product ff_r_mkm_product_val_selected_power_product ff_s_mkm_product_val_selected_power_product. ((((exists ff_h_mkm_product_val_selected_power_product_factor. ff_h_mkm_product_val_selected_power_product_factor + S (ff_p_mkm_product_val_selected_power_product) = S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_c_mkm_product_val_selected_power)) /\ exists ff_q_mkm_product_val_selected_power_product_factor. ff_b_mkm_product_val_selected_power = ff_q_mkm_product_val_selected_power_product_factor * S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_c_mkm_product_val_selected_power) + (ff_p_mkm_product_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_partial. ff_h_mkm_product_val_selected_power_product_partial + S (ff_r_mkm_product_val_selected_power_product) = S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_partial. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_partial * S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product) + (ff_r_mkm_product_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_successor. ff_h_mkm_product_val_selected_power_product_successor + S (ff_s_mkm_product_val_selected_power_product) = S ((S (S ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_successor. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_successor * S ((S (S ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product) + (ff_s_mkm_product_val_selected_power_product))) /\ ff_s_mkm_product_val_selected_power_product = ff_r_mkm_product_val_selected_power_product * ff_p_mkm_product_val_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_val_selected_divides. (z) = bpv_result_mkm_product_val_selected * bpv_factor_mkm_product_val_selected_divides)))) /\ forall bpv_candidate_mkm_product_val. (exists bpv_gap_mkm_product_val_candidate_bound. bpv_gap_mkm_product_val_candidate_bound + bpv_candidate_mkm_product_val = (z)) -> (exists bpv_result_mkm_product_val_candidate. ((exists ff_b_mkm_product_val_candidate_power ff_c_mkm_product_val_candidate_power. ((forall ff_i_mkm_product_val_candidate_power_repeat. (exists ff_lt_mkm_product_val_candidate_power_repeat_bound. ff_lt_mkm_product_val_candidate_power_repeat_bound + S ff_i_mkm_product_val_candidate_power_repeat = bpv_candidate_mkm_product_val) -> (((exists ff_h_mkm_product_val_candidate_power_repeat_decoded. ff_h_mkm_product_val_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_val_candidate_power_repeat)) * ff_c_mkm_product_val_candidate_power)) /\ exists ff_q_mkm_product_val_candidate_power_repeat_decoded. ff_b_mkm_product_val_candidate_power = ff_q_mkm_product_val_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_val_candidate_power_repeat)) * ff_c_mkm_product_val_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_val_candidate_power_product ff_v_mkm_product_val_candidate_power_product. ((((exists ff_h_mkm_product_val_candidate_power_product_start. ff_h_mkm_product_val_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_start. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_val_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_terminal. ff_h_mkm_product_val_candidate_power_product_terminal + S (bpv_result_mkm_product_val_candidate) = S ((S (bpv_candidate_mkm_product_val)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_terminal. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_val)) * ff_v_mkm_product_val_candidate_power_product) + (bpv_result_mkm_product_val_candidate))) /\ forall ff_i_mkm_product_val_candidate_power_product. (exists ff_lt_mkm_product_val_candidate_power_product_bound. ff_lt_mkm_product_val_candidate_power_product_bound + S ff_i_mkm_product_val_candidate_power_product = bpv_candidate_mkm_product_val) -> exists ff_p_mkm_product_val_candidate_power_product ff_r_mkm_product_val_candidate_power_product ff_s_mkm_product_val_candidate_power_product. ((((exists ff_h_mkm_product_val_candidate_power_product_factor. ff_h_mkm_product_val_candidate_power_product_factor + S (ff_p_mkm_product_val_candidate_power_product) = S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_c_mkm_product_val_candidate_power)) /\ exists ff_q_mkm_product_val_candidate_power_product_factor. ff_b_mkm_product_val_candidate_power = ff_q_mkm_product_val_candidate_power_product_factor * S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_c_mkm_product_val_candidate_power) + (ff_p_mkm_product_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_partial. ff_h_mkm_product_val_candidate_power_product_partial + S (ff_r_mkm_product_val_candidate_power_product) = S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_partial. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_partial * S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product) + (ff_r_mkm_product_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_successor. ff_h_mkm_product_val_candidate_power_product_successor + S (ff_s_mkm_product_val_candidate_power_product) = S ((S (S ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_successor. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_successor * S ((S (S ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product) + (ff_s_mkm_product_val_candidate_power_product))) /\ ff_s_mkm_product_val_candidate_power_product = ff_r_mkm_product_val_candidate_power_product * ff_p_mkm_product_val_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_val_candidate_divides. (z) = bpv_result_mkm_product_val_candidate * bpv_factor_mkm_product_val_candidate_divides))) -> (exists bpv_gap_mkm_product_val_maximal. bpv_gap_mkm_product_val_maximal + bpv_candidate_mkm_product_val = g)) -> g = e

Constructive proof overview

Generated structural guide

For a prime and any nonzero finite factor list, the exact product valuation equals the finite sum of its actual factor valuations.

The unchanged tactic script uses 12 declared prerequisites and contains 150 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_sum_zero Stable theorem; checked-use authorized beta_product_zero Stable theorem; checked-use authorized prime_power_valuation_one_zero Alpha theorem; checked-use authorized beta_product_succ_decompose Stable theorem; checked-use authorized beta_sum_succ_decompose Stable theorem; checked-use authorized crt_positive_moduli_prefix_drop_last Alpha theorem; checked-use authorized MK0002 beta_valuation_prefix_drop_last power_valuation_exists Alpha theorem; checked-use authorized MK0003 beta_valuation_prefix_last crt_positive_moduli_prefix_product_nonzero Alpha theorem; checked-use authorized crt_positive_moduli_prefix_last_nonzero Alpha theorem; checked-use authorized prime_power_valuation_mul Alpha theorem; checked-use authorized

Direct dependents

MK0007 beta_prime_product_valuation_from_sum

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

150 script commands · 27 reading checkpoints · 8 local claims

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

Named ingredients (2)
beta valuation prefix drop lastbeta valuation prefix last

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

01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro vb
  5. L5
    intro vc
02Induction on lL6–15

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

  1. L6
    induction l
  2. L7
    intro z
  3. L8
    intro e
  4. L9
    intro g
  5. L10
    intro hp
  6. L11
    intro hn
  7. L12
    intro hv
  8. L13
    intro hprod
  9. L14
    intro hsum
  10. L15
    intro hg
03Establish hezeroL16–25

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

  1. L16
    have hezero : e = 0
  2. L17
    specialize beta_sum_zero vb
  3. L18
    specialize beta_sum_zero vc
  4. L19
    specialize beta_sum_zero e
  5. L20
    apply beta_sum_zero
  6. L21
    exact hsum
  7. L22
    rewrite hezero
  8. L23
    specialize prime_power_valuation_one_zero p
  9. L24
    specialize prime_power_valuation_one_zero z
  10. L25
    specialize prime_power_valuation_one_zero g
04Use earlier factsL26–33

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

  1. L26
    apply prime_power_valuation_one_zero
  2. L27
    specialize beta_product_zero b
  3. L28
    specialize beta_product_zero c
  4. L29
    specialize beta_product_zero z
  5. L30
    apply beta_product_zero
  6. L31
    exact hprod
  7. L32
    exact hp
  8. L33
    exact hg
05Fix variables and assumptionsL34–42

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

  1. L34
    intro z
  2. L35
    intro e
  3. L36
    intro g
  4. L37
    intro hp
  5. L38
    intro hn
  6. L39
    intro hv
  7. L40
    intro hprod
  8. L41
    intro hsum
  9. L42
    intro hg
06Establish hprodpartL43–49

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

  1. L43
    have hprodpart : ∃ a. ∃ w. BetaAt(b,c,l,a) ∧ (Product(b,c,l,w) ∧ z = w · a)Definitions: BetaAtProduct
  2. L44
    specialize beta_product_succ_decompose b
  3. L45
    specialize beta_product_succ_decompose c
  4. L46
    specialize beta_product_succ_decompose l
  5. L47
    specialize beta_product_succ_decompose z
  6. L48
    apply beta_product_succ_decompose
  7. L49
    exact hprod
07Separate the logical casesL50–53

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

  1. L50
    cases hprodpart
  2. L51
    cases hprodpart_witness
  3. L52
    cases hprodpart_witness_witness
  4. L53
    cases hprodpart_witness_witness_right
08Establish hsumpartL54–60

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

  1. L54
    have hsumpart : ∃ v. ∃ E. BetaAt(vb,vc,l,v) ∧ (Sum(vb,vc,l,E) ∧ e = E + v)Definitions: BetaAtSum
  2. L55
    specialize beta_sum_succ_decompose vb
  3. L56
    specialize beta_sum_succ_decompose vc
  4. L57
    specialize beta_sum_succ_decompose l
  5. L58
    specialize beta_sum_succ_decompose e
  6. L59
    apply beta_sum_succ_decompose
  7. L60
    exact hsum
09Separate the logical casesL61–64

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

  1. L61
    cases hsumpart
  2. L62
    cases hsumpart_witness
  3. L63
    cases hsumpart_witness_witness
  4. L64
    cases hsumpart_witness_witness_right
10Establish hnprevL65–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix drop last.

  1. L65
    have hnprev : ∀ gcrt_positive_index_mkm_product_previous_nonzero. ∀ gcrt_positive_value_mkm_product_previous_nonzero. Lt(gcrt_positive_index_mkm_product_previous_nonzero,l) → BetaAt(b,c,gcrt_positive_index_mkm_product_previous_nonzero,gcrt_positive_value_mkm_product_previous_nonzero) → ¬gcrt_positive_value_mkm_product_previous_nonzero = 0Definitions: LtBetaAt
  2. L66
    specialize crt_positive_moduli_prefix_drop_last b
  3. L67
    specialize crt_positive_moduli_prefix_drop_last c
  4. L68
    specialize crt_positive_moduli_prefix_drop_last l
  5. L69
    apply crt_positive_moduli_prefix_drop_last
  6. L70
    exact hn
11Establish hvprevL71–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta valuation prefix drop last.

  1. L71
    have hvprev : BetaValuationPrefix(p,b,c,vb,vc,l)Definitions: BetaValuationPrefix
  2. L72
    specialize beta_valuation_prefix_drop_last p
  3. L73
    specialize beta_valuation_prefix_drop_last b
  4. L74
    specialize beta_valuation_prefix_drop_last c
  5. L75
    specialize beta_valuation_prefix_drop_last vb
  6. L76
    specialize beta_valuation_prefix_drop_last vc
  7. L77
    specialize beta_valuation_prefix_drop_last l
  8. L78
    apply beta_valuation_prefix_drop_last
  9. L79
    exact hv
12Establish hpreviousL80–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation exists.

  1. L80
    have hprevious : ∃ v. BoundedPowerValuation(p,x1,x1,v)Definitions: BoundedPowerValuation
  2. L81
    specialize power_valuation_exists p
  3. L82
    specialize power_valuation_exists x1
  4. L83
    apply power_valuation_exists
13Separate the logical casesL84–84

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

  1. L84
    cases hprevious
14Establish hprevious_valueL85–94

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

  1. L85
    have hprevious_value : x4 = x3
  2. L86
    specialize IH x1
  3. L87
    specialize IH x3
  4. L88
    specialize IH x4
  5. L89
    apply IH
  6. L90
    exact hp
  7. L91
    exact hnprev
  8. L92
    exact hvprev
  9. L93
    exact hprodpart_witness_witness_right_left
  10. L94
    exact hsumpart_witness_witness_right_left
15Use earlier factsL95–95

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

  1. L95
    exact hprevious_witness
16Calculate and transport equalitiesL96–101

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

  1. L96
    rewrite hprevious_value at hprevious_witness
  2. L97
    rewrite hprevious_value at hprevious_witness
  3. L98
    rewrite hprevious_value at hprevious_witness
  4. L99
    rewrite hprevious_value at hprevious_witness
  5. L100
    rewrite hprevious_value at hprevious_witness
  6. L101
    rewrite hprevious_value at hprevious_witness
17Establish hlastL102–111

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

  1. L102
    have hlast : BoundedPowerValuation(p,x,x,x2)Definitions: BoundedPowerValuation
  2. L103
    specialize beta_valuation_prefix_last p
  3. L104
    specialize beta_valuation_prefix_last b
  4. L105
    specialize beta_valuation_prefix_last c
  5. L106
    specialize beta_valuation_prefix_last vb
  6. L107
    specialize beta_valuation_prefix_last vc
  7. L108
    specialize beta_valuation_prefix_last l
  8. L109
    specialize beta_valuation_prefix_last x
  9. L110
    specialize beta_valuation_prefix_last x2
  10. L111
    apply beta_valuation_prefix_last
18Use earlier factsL112–114

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

  1. L112
    exact hv
  2. L113
    exact hprodpart_witness_witness_left
  3. L114
    exact hsumpart_witness_witness_left
19Calculate and transport equalitiesL115–119

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

  1. L115
    rewrite hprodpart_witness_witness_right_right at hg
  2. L116
    rewrite hprodpart_witness_witness_right_right at hg
  3. L117
    rewrite hprodpart_witness_witness_right_right at hg
  4. L118
    rewrite hprodpart_witness_witness_right_right at hg
  5. L119
    trans x3 + x2
20Use earlier factsL120–127

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

  1. L120
    specialize prime_power_valuation_mul p
  2. L121
    specialize prime_power_valuation_mul x1
  3. L122
    specialize prime_power_valuation_mul x
  4. L123
    specialize prime_power_valuation_mul x3
  5. L124
    specialize prime_power_valuation_mul x2
  6. L125
    specialize prime_power_valuation_mul g
  7. L126
    apply prime_power_valuation_mul
  8. L127
    exact hp
21Fix variables and assumptionsL128–128

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

  1. L128
    intro hzero
22Use earlier factsL129–136

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

  1. L129
    specialize crt_positive_moduli_prefix_product_nonzero b
  2. L130
    specialize crt_positive_moduli_prefix_product_nonzero c
  3. L131
    specialize crt_positive_moduli_prefix_product_nonzero l
  4. L132
    specialize crt_positive_moduli_prefix_product_nonzero x1
  5. L133
    apply crt_positive_moduli_prefix_product_nonzero
  6. L134
    exact hnprev
  7. L135
    exact hprodpart_witness_witness_right_left
  8. L136
    exact hzero
23Fix variables and assumptionsL137–137

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

  1. L137
    intro hzero
24Use earlier factsL138–147

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

  1. L138
    specialize crt_positive_moduli_prefix_last_nonzero b
  2. L139
    specialize crt_positive_moduli_prefix_last_nonzero c
  3. L140
    specialize crt_positive_moduli_prefix_last_nonzero l
  4. L141
    specialize crt_positive_moduli_prefix_last_nonzero x
  5. L142
    apply crt_positive_moduli_prefix_last_nonzero
  6. L143
    exact hn
  7. L144
    exact hprodpart_witness_witness_left
  8. L145
    exact hzero
  9. L146
    exact hprevious_witness
  10. L147
    exact hlast
25Use earlier factsL148–148

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

  1. L148
    exact hg
26Calculate and transport equalitiesL149–149

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

  1. L149
    symm
27Use earlier factsL150–150

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

  1. L150
    exact hsumpart_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 150 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro vb
  5. 0005intro vc
  6. 0006induction l
  7. 0007intro z
  8. 0008intro e
  9. 0009intro g
  10. 0010intro hp
  11. 0011intro hn
  12. 0012intro hv
  13. 0013intro hprod
  14. 0014intro hsum
  15. 0015intro hg
  16. 0016have hezero : e = 0
  17. 0017specialize beta_sum_zero vb
  18. 0018specialize beta_sum_zero vc
  19. 0019specialize beta_sum_zero e
  20. 0020apply beta_sum_zero
  21. 0021exact hsum
  22. 0022rewrite hezero
  23. 0023specialize prime_power_valuation_one_zero p
  24. 0024specialize prime_power_valuation_one_zero z
  25. 0025specialize prime_power_valuation_one_zero g
  26. 0026apply prime_power_valuation_one_zero
  27. 0027specialize beta_product_zero b
  28. 0028specialize beta_product_zero c
  29. 0029specialize beta_product_zero z
  30. 0030apply beta_product_zero
  31. 0031exact hprod
  32. 0032exact hp
  33. 0033exact hg
  34. 0034intro z
  35. 0035intro e
  36. 0036intro g
  37. 0037intro hp
  38. 0038intro hn
  39. 0039intro hv
  40. 0040intro hprod
  41. 0041intro hsum
  42. 0042intro hg
  43. 0043have hprodpart : exists a w. (((exists fs_h_mkm_product_last. fs_h_mkm_product_last + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_product_last. b = fs_q_mkm_product_last * S ((S (l)) * c) + (a))) /\ ((exists ff_u_mkm_product_before ff_v_mkm_product_before. ((((exists ff_h_mkm_product_before_start. ff_h_mkm_product_before_start + S (1) = S ((S (0)) * ff_v_mkm_product_before)) /\ exists ff_q_mkm_product_before_start. ff_u_mkm_product_before = ff_q_mkm_product_before_start * S ((S (0)) * ff_v_mkm_product_before) + (1))) /\ ((((exists ff_h_mkm_product_before_terminal. ff_h_mkm_product_before_terminal + S (w) = S ((S (l)) * ff_v_mkm_product_before)) /\ exists ff_q_mkm_product_before_terminal. ff_u_mkm_product_before = ff_q_mkm_product_before_terminal * S ((S (l)) * ff_v_mkm_product_before) + (w))) /\ forall ff_i_mkm_product_before. (exists ff_lt_mkm_product_before_bound. ff_lt_mkm_product_before_bound + S ff_i_mkm_product_before = l) -> exists ff_p_mkm_product_before ff_r_mkm_product_before ff_s_mkm_product_before. ((((exists ff_h_mkm_product_before_factor. ff_h_mkm_product_before_factor + S (ff_p_mkm_product_before) = S ((S (ff_i_mkm_product_before)) * c)) /\ exists ff_q_mkm_product_before_factor. b = ff_q_mkm_product_before_factor * S ((S (ff_i_mkm_product_before)) * c) + (ff_p_mkm_product_before))) /\ ((((exists ff_h_mkm_product_before_partial. ff_h_mkm_product_before_partial + S (ff_r_mkm_product_before) = S ((S (ff_i_mkm_product_before)) * ff_v_mkm_product_before)) /\ exists ff_q_mkm_product_before_partial. ff_u_mkm_product_before = ff_q_mkm_product_before_partial * S ((S (ff_i_mkm_product_before)) * ff_v_mkm_product_before) + (ff_r_mkm_product_before))) /\ ((((exists ff_h_mkm_product_before_successor. ff_h_mkm_product_before_successor + S (ff_s_mkm_product_before) = S ((S (S ff_i_mkm_product_before)) * ff_v_mkm_product_before)) /\ exists ff_q_mkm_product_before_successor. ff_u_mkm_product_before = ff_q_mkm_product_before_successor * S ((S (S ff_i_mkm_product_before)) * ff_v_mkm_product_before) + (ff_s_mkm_product_before))) /\ ff_s_mkm_product_before = ff_r_mkm_product_before * ff_p_mkm_product_before)))))) /\ z = w * a)
  44. 0044specialize beta_product_succ_decompose b
  45. 0045specialize beta_product_succ_decompose c
  46. 0046specialize beta_product_succ_decompose l
  47. 0047specialize beta_product_succ_decompose z
  48. 0048apply beta_product_succ_decompose
  49. 0049exact hprod
  50. 0050cases hprodpart
  51. 0051cases hprodpart_witness
  52. 0052cases hprodpart_witness_witness
  53. 0053cases hprodpart_witness_witness_right
  54. 0054have hsumpart : exists v E. (((exists fs_h_mkm_product_last_exponent. fs_h_mkm_product_last_exponent + S (v) = S ((S (l)) * vc)) /\ exists fs_q_mkm_product_last_exponent. vb = fs_q_mkm_product_last_exponent * S ((S (l)) * vc) + (v))) /\ ((exists fs_u_mkm_product_sum_before fs_v_mkm_product_sum_before. ((((exists fs_h_mkm_product_sum_before_body_start. fs_h_mkm_product_sum_before_body_start + S (0) = S ((S (0)) * fs_v_mkm_product_sum_before)) /\ exists fs_q_mkm_product_sum_before_body_start. fs_u_mkm_product_sum_before = fs_q_mkm_product_sum_before_body_start * S ((S (0)) * fs_v_mkm_product_sum_before) + (0))) /\ ((((exists fs_h_mkm_product_sum_before_body_terminal. fs_h_mkm_product_sum_before_body_terminal + S (E) = S ((S (l)) * fs_v_mkm_product_sum_before)) /\ exists fs_q_mkm_product_sum_before_body_terminal. fs_u_mkm_product_sum_before = fs_q_mkm_product_sum_before_body_terminal * S ((S (l)) * fs_v_mkm_product_sum_before) + (E))) /\ forall fs_i_mkm_product_sum_before_body_steps. (exists fs_lt_mkm_product_sum_before_body_steps_bound. fs_lt_mkm_product_sum_before_body_steps_bound + S fs_i_mkm_product_sum_before_body_steps = l) -> exists fs_a_mkm_product_sum_before_body_steps fs_r_mkm_product_sum_before_body_steps fs_s_mkm_product_sum_before_body_steps. ((((exists fs_h_mkm_product_sum_before_body_steps_summand. fs_h_mkm_product_sum_before_body_steps_summand + S (fs_a_mkm_product_sum_before_body_steps) = S ((S (fs_i_mkm_product_sum_before_body_steps)) * vc)) /\ exists fs_q_mkm_product_sum_before_body_steps_summand. vb = fs_q_mkm_product_sum_before_body_steps_summand * S ((S (fs_i_mkm_product_sum_before_body_steps)) * vc) + (fs_a_mkm_product_sum_before_body_steps))) /\ ((((exists fs_h_mkm_product_sum_before_body_steps_partial. fs_h_mkm_product_sum_before_body_steps_partial + S (fs_r_mkm_product_sum_before_body_steps) = S ((S (fs_i_mkm_product_sum_before_body_steps)) * fs_v_mkm_product_sum_before)) /\ exists fs_q_mkm_product_sum_before_body_steps_partial. fs_u_mkm_product_sum_before = fs_q_mkm_product_sum_before_body_steps_partial * S ((S (fs_i_mkm_product_sum_before_body_steps)) * fs_v_mkm_product_sum_before) + (fs_r_mkm_product_sum_before_body_steps))) /\ ((((exists fs_h_mkm_product_sum_before_body_steps_successor. fs_h_mkm_product_sum_before_body_steps_successor + S (fs_s_mkm_product_sum_before_body_steps) = S ((S (S fs_i_mkm_product_sum_before_body_steps)) * fs_v_mkm_product_sum_before)) /\ exists fs_q_mkm_product_sum_before_body_steps_successor. fs_u_mkm_product_sum_before = fs_q_mkm_product_sum_before_body_steps_successor * S ((S (S fs_i_mkm_product_sum_before_body_steps)) * fs_v_mkm_product_sum_before) + (fs_s_mkm_product_sum_before_body_steps))) /\ fs_s_mkm_product_sum_before_body_steps = fs_r_mkm_product_sum_before_body_steps + fs_a_mkm_product_sum_before_body_steps)))))) /\ e = E + v)
  55. 0055specialize beta_sum_succ_decompose vb
  56. 0056specialize beta_sum_succ_decompose vc
  57. 0057specialize beta_sum_succ_decompose l
  58. 0058specialize beta_sum_succ_decompose e
  59. 0059apply beta_sum_succ_decompose
  60. 0060exact hsum
  61. 0061cases hsumpart
  62. 0062cases hsumpart_witness
  63. 0063cases hsumpart_witness_witness
  64. 0064cases hsumpart_witness_witness_right
  65. 0065have hnprev : forall gcrt_positive_index_mkm_product_previous_nonzero gcrt_positive_value_mkm_product_previous_nonzero. (exists ff_lt_gcrt_mkm_product_previous_nonzero_bound. ff_lt_gcrt_mkm_product_previous_nonzero_bound + S gcrt_positive_index_mkm_product_previous_nonzero = l) -> (((exists ff_h_gcrt_mkm_product_previous_nonzero_entry. ff_h_gcrt_mkm_product_previous_nonzero_entry + S (gcrt_positive_value_mkm_product_previous_nonzero) = S ((S (gcrt_positive_index_mkm_product_previous_nonzero)) * c)) /\ exists ff_q_gcrt_mkm_product_previous_nonzero_entry. b = ff_q_gcrt_mkm_product_previous_nonzero_entry * S ((S (gcrt_positive_index_mkm_product_previous_nonzero)) * c) + (gcrt_positive_value_mkm_product_previous_nonzero))) -> ~(gcrt_positive_value_mkm_product_previous_nonzero = 0)
  66. 0066specialize crt_positive_moduli_prefix_drop_last b
  67. 0067specialize crt_positive_moduli_prefix_drop_last c
  68. 0068specialize crt_positive_moduli_prefix_drop_last l
  69. 0069apply crt_positive_moduli_prefix_drop_last
  70. 0070exact hn
  71. 0071have hvprev : forall mkm_index_product_previous_values. (exists mkm_lt_product_previous_values_bound. mkm_lt_product_previous_values_bound + S (mkm_index_product_previous_values) = (l)) -> (exists mkm_value_product_previous_values_point mkm_exponent_product_previous_values_point. (((exists fs_h_mkm_product_previous_values_point_source. fs_h_mkm_product_previous_values_point_source + S (mkm_value_product_previous_values_point) = S ((S (mkm_index_product_previous_values)) * c)) /\ exists fs_q_mkm_product_previous_values_point_source. b = fs_q_mkm_product_previous_values_point_source * S ((S (mkm_index_product_previous_values)) * c) + (mkm_value_product_previous_values_point))) /\ ((((exists fs_h_mkm_product_previous_values_point_decoded. fs_h_mkm_product_previous_values_point_decoded + S (mkm_exponent_product_previous_values_point) = S ((S (mkm_index_product_previous_values)) * vc)) /\ exists fs_q_mkm_product_previous_values_point_decoded. vb = fs_q_mkm_product_previous_values_point_decoded * S ((S (mkm_index_product_previous_values)) * vc) + (mkm_exponent_product_previous_values_point))) /\ (((exists bpv_gap_mkm_product_previous_values_point_valuation_exponent_bound. bpv_gap_mkm_product_previous_values_point_valuation_exponent_bound + mkm_exponent_product_previous_values_point = (mkm_value_product_previous_values_point)) /\ (exists bpv_result_mkm_product_previous_values_point_valuation_selected. ((exists ff_b_mkm_product_previous_values_point_valuation_selected_power ff_c_mkm_product_previous_values_point_valuation_selected_power. ((forall ff_i_mkm_product_previous_values_point_valuation_selected_power_repeat. (exists ff_lt_mkm_product_previous_values_point_valuation_selected_power_repeat_bound. ff_lt_mkm_product_previous_values_point_valuation_selected_power_repeat_bound + S ff_i_mkm_product_previous_values_point_valuation_selected_power_repeat = mkm_exponent_product_previous_values_point) -> (((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_repeat_decoded. ff_h_mkm_product_previous_values_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_repeat)) * ff_c_mkm_product_previous_values_point_valuation_selected_power)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_repeat_decoded. ff_b_mkm_product_previous_values_point_valuation_selected_power = ff_q_mkm_product_previous_values_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_repeat)) * ff_c_mkm_product_previous_values_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_product_previous_values_point_valuation_selected_power_product ff_v_mkm_product_previous_values_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_product_start. ff_h_mkm_product_previous_values_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_product_start. ff_u_mkm_product_previous_values_point_valuation_selected_power_product = ff_q_mkm_product_previous_values_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_product_terminal. ff_h_mkm_product_previous_values_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_product_previous_values_point_valuation_selected) = S ((S (mkm_exponent_product_previous_values_point)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_product_terminal. ff_u_mkm_product_previous_values_point_valuation_selected_power_product = ff_q_mkm_product_previous_values_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_product_previous_values_point)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product) + (bpv_result_mkm_product_previous_values_point_valuation_selected))) /\ forall ff_i_mkm_product_previous_values_point_valuation_selected_power_product. (exists ff_lt_mkm_product_previous_values_point_valuation_selected_power_product_bound. ff_lt_mkm_product_previous_values_point_valuation_selected_power_product_bound + S ff_i_mkm_product_previous_values_point_valuation_selected_power_product = mkm_exponent_product_previous_values_point) -> exists ff_p_mkm_product_previous_values_point_valuation_selected_power_product ff_r_mkm_product_previous_values_point_valuation_selected_power_product ff_s_mkm_product_previous_values_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_product_factor. ff_h_mkm_product_previous_values_point_valuation_selected_power_product_factor + S (ff_p_mkm_product_previous_values_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_c_mkm_product_previous_values_point_valuation_selected_power)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_product_factor. ff_b_mkm_product_previous_values_point_valuation_selected_power = ff_q_mkm_product_previous_values_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_c_mkm_product_previous_values_point_valuation_selected_power) + (ff_p_mkm_product_previous_values_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_product_partial. ff_h_mkm_product_previous_values_point_valuation_selected_power_product_partial + S (ff_r_mkm_product_previous_values_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_product_partial. ff_u_mkm_product_previous_values_point_valuation_selected_power_product = ff_q_mkm_product_previous_values_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product) + (ff_r_mkm_product_previous_values_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_selected_power_product_successor. ff_h_mkm_product_previous_values_point_valuation_selected_power_product_successor + S (ff_s_mkm_product_previous_values_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_selected_power_product_successor. ff_u_mkm_product_previous_values_point_valuation_selected_power_product = ff_q_mkm_product_previous_values_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_product_previous_values_point_valuation_selected_power_product)) * ff_v_mkm_product_previous_values_point_valuation_selected_power_product) + (ff_s_mkm_product_previous_values_point_valuation_selected_power_product))) /\ ff_s_mkm_product_previous_values_point_valuation_selected_power_product = ff_r_mkm_product_previous_values_point_valuation_selected_power_product * ff_p_mkm_product_previous_values_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_previous_values_point_valuation_selected_divides. (mkm_value_product_previous_values_point) = bpv_result_mkm_product_previous_values_point_valuation_selected * bpv_factor_mkm_product_previous_values_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_product_previous_values_point_valuation. (exists bpv_gap_mkm_product_previous_values_point_valuation_candidate_bound. bpv_gap_mkm_product_previous_values_point_valuation_candidate_bound + bpv_candidate_mkm_product_previous_values_point_valuation = (mkm_value_product_previous_values_point)) -> (exists bpv_result_mkm_product_previous_values_point_valuation_candidate. ((exists ff_b_mkm_product_previous_values_point_valuation_candidate_power ff_c_mkm_product_previous_values_point_valuation_candidate_power. ((forall ff_i_mkm_product_previous_values_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_product_previous_values_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_product_previous_values_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_product_previous_values_point_valuation_candidate_power_repeat = bpv_candidate_mkm_product_previous_values_point_valuation) -> (((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_product_previous_values_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_previous_values_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_product_previous_values_point_valuation_candidate_power = ff_q_mkm_product_previous_values_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_previous_values_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_previous_values_point_valuation_candidate_power_product ff_v_mkm_product_previous_values_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_start. ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_start. ff_u_mkm_product_previous_values_point_valuation_candidate_power_product = ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_terminal. ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_product_previous_values_point_valuation_candidate) = S ((S (bpv_candidate_mkm_product_previous_values_point_valuation)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_terminal. ff_u_mkm_product_previous_values_point_valuation_candidate_power_product = ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_previous_values_point_valuation)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product) + (bpv_result_mkm_product_previous_values_point_valuation_candidate))) /\ forall ff_i_mkm_product_previous_values_point_valuation_candidate_power_product. (exists ff_lt_mkm_product_previous_values_point_valuation_candidate_power_product_bound. ff_lt_mkm_product_previous_values_point_valuation_candidate_power_product_bound + S ff_i_mkm_product_previous_values_point_valuation_candidate_power_product = bpv_candidate_mkm_product_previous_values_point_valuation) -> exists ff_p_mkm_product_previous_values_point_valuation_candidate_power_product ff_r_mkm_product_previous_values_point_valuation_candidate_power_product ff_s_mkm_product_previous_values_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_factor. ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_factor + S (ff_p_mkm_product_previous_values_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_c_mkm_product_previous_values_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_factor. ff_b_mkm_product_previous_values_point_valuation_candidate_power = ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_c_mkm_product_previous_values_point_valuation_candidate_power) + (ff_p_mkm_product_previous_values_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_partial. ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_partial + S (ff_r_mkm_product_previous_values_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_partial. ff_u_mkm_product_previous_values_point_valuation_candidate_power_product = ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product) + (ff_r_mkm_product_previous_values_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_successor. ff_h_mkm_product_previous_values_point_valuation_candidate_power_product_successor + S (ff_s_mkm_product_previous_values_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_successor. ff_u_mkm_product_previous_values_point_valuation_candidate_power_product = ff_q_mkm_product_previous_values_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_product_previous_values_point_valuation_candidate_power_product)) * ff_v_mkm_product_previous_values_point_valuation_candidate_power_product) + (ff_s_mkm_product_previous_values_point_valuation_candidate_power_product))) /\ ff_s_mkm_product_previous_values_point_valuation_candidate_power_product = ff_r_mkm_product_previous_values_point_valuation_candidate_power_product * ff_p_mkm_product_previous_values_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_previous_values_point_valuation_candidate_divides. (mkm_value_product_previous_values_point) = bpv_result_mkm_product_previous_values_point_valuation_candidate * bpv_factor_mkm_product_previous_values_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_product_previous_values_point_valuation_maximal. bpv_gap_mkm_product_previous_values_point_valuation_maximal + bpv_candidate_mkm_product_previous_values_point_valuation = mkm_exponent_product_previous_values_point))))
  72. 0072specialize beta_valuation_prefix_drop_last p
  73. 0073specialize beta_valuation_prefix_drop_last b
  74. 0074specialize beta_valuation_prefix_drop_last c
  75. 0075specialize beta_valuation_prefix_drop_last vb
  76. 0076specialize beta_valuation_prefix_drop_last vc
  77. 0077specialize beta_valuation_prefix_drop_last l
  78. 0078apply beta_valuation_prefix_drop_last
  79. 0079exact hv
  80. 0080have hprevious : exists v. ((exists bpv_gap_mkm_product_previous_val_exponent_bound. bpv_gap_mkm_product_previous_val_exponent_bound + v = (x1)) /\ (exists bpv_result_mkm_product_previous_val_selected. ((exists ff_b_mkm_product_previous_val_selected_power ff_c_mkm_product_previous_val_selected_power. ((forall ff_i_mkm_product_previous_val_selected_power_repeat. (exists ff_lt_mkm_product_previous_val_selected_power_repeat_bound. ff_lt_mkm_product_previous_val_selected_power_repeat_bound + S ff_i_mkm_product_previous_val_selected_power_repeat = v) -> (((exists ff_h_mkm_product_previous_val_selected_power_repeat_decoded. ff_h_mkm_product_previous_val_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_previous_val_selected_power_repeat)) * ff_c_mkm_product_previous_val_selected_power)) /\ exists ff_q_mkm_product_previous_val_selected_power_repeat_decoded. ff_b_mkm_product_previous_val_selected_power = ff_q_mkm_product_previous_val_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_previous_val_selected_power_repeat)) * ff_c_mkm_product_previous_val_selected_power) + (p)))) /\ (exists ff_u_mkm_product_previous_val_selected_power_product ff_v_mkm_product_previous_val_selected_power_product. ((((exists ff_h_mkm_product_previous_val_selected_power_product_start. ff_h_mkm_product_previous_val_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_previous_val_selected_power_product)) /\ exists ff_q_mkm_product_previous_val_selected_power_product_start. ff_u_mkm_product_previous_val_selected_power_product = ff_q_mkm_product_previous_val_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_previous_val_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_previous_val_selected_power_product_terminal. ff_h_mkm_product_previous_val_selected_power_product_terminal + S (bpv_result_mkm_product_previous_val_selected) = S ((S (v)) * ff_v_mkm_product_previous_val_selected_power_product)) /\ exists ff_q_mkm_product_previous_val_selected_power_product_terminal. ff_u_mkm_product_previous_val_selected_power_product = ff_q_mkm_product_previous_val_selected_power_product_terminal * S ((S (v)) * ff_v_mkm_product_previous_val_selected_power_product) + (bpv_result_mkm_product_previous_val_selected))) /\ forall ff_i_mkm_product_previous_val_selected_power_product. (exists ff_lt_mkm_product_previous_val_selected_power_product_bound. ff_lt_mkm_product_previous_val_selected_power_product_bound + S ff_i_mkm_product_previous_val_selected_power_product = v) -> exists ff_p_mkm_product_previous_val_selected_power_product ff_r_mkm_product_previous_val_selected_power_product ff_s_mkm_product_previous_val_selected_power_product. ((((exists ff_h_mkm_product_previous_val_selected_power_product_factor. ff_h_mkm_product_previous_val_selected_power_product_factor + S (ff_p_mkm_product_previous_val_selected_power_product) = S ((S (ff_i_mkm_product_previous_val_selected_power_product)) * ff_c_mkm_product_previous_val_selected_power)) /\ exists ff_q_mkm_product_previous_val_selected_power_product_factor. ff_b_mkm_product_previous_val_selected_power = ff_q_mkm_product_previous_val_selected_power_product_factor * S ((S (ff_i_mkm_product_previous_val_selected_power_product)) * ff_c_mkm_product_previous_val_selected_power) + (ff_p_mkm_product_previous_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_previous_val_selected_power_product_partial. ff_h_mkm_product_previous_val_selected_power_product_partial + S (ff_r_mkm_product_previous_val_selected_power_product) = S ((S (ff_i_mkm_product_previous_val_selected_power_product)) * ff_v_mkm_product_previous_val_selected_power_product)) /\ exists ff_q_mkm_product_previous_val_selected_power_product_partial. ff_u_mkm_product_previous_val_selected_power_product = ff_q_mkm_product_previous_val_selected_power_product_partial * S ((S (ff_i_mkm_product_previous_val_selected_power_product)) * ff_v_mkm_product_previous_val_selected_power_product) + (ff_r_mkm_product_previous_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_previous_val_selected_power_product_successor. ff_h_mkm_product_previous_val_selected_power_product_successor + S (ff_s_mkm_product_previous_val_selected_power_product) = S ((S (S ff_i_mkm_product_previous_val_selected_power_product)) * ff_v_mkm_product_previous_val_selected_power_product)) /\ exists ff_q_mkm_product_previous_val_selected_power_product_successor. ff_u_mkm_product_previous_val_selected_power_product = ff_q_mkm_product_previous_val_selected_power_product_successor * S ((S (S ff_i_mkm_product_previous_val_selected_power_product)) * ff_v_mkm_product_previous_val_selected_power_product) + (ff_s_mkm_product_previous_val_selected_power_product))) /\ ff_s_mkm_product_previous_val_selected_power_product = ff_r_mkm_product_previous_val_selected_power_product * ff_p_mkm_product_previous_val_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_previous_val_selected_divides. (x1) = bpv_result_mkm_product_previous_val_selected * bpv_factor_mkm_product_previous_val_selected_divides)))) /\ forall bpv_candidate_mkm_product_previous_val. (exists bpv_gap_mkm_product_previous_val_candidate_bound. bpv_gap_mkm_product_previous_val_candidate_bound + bpv_candidate_mkm_product_previous_val = (x1)) -> (exists bpv_result_mkm_product_previous_val_candidate. ((exists ff_b_mkm_product_previous_val_candidate_power ff_c_mkm_product_previous_val_candidate_power. ((forall ff_i_mkm_product_previous_val_candidate_power_repeat. (exists ff_lt_mkm_product_previous_val_candidate_power_repeat_bound. ff_lt_mkm_product_previous_val_candidate_power_repeat_bound + S ff_i_mkm_product_previous_val_candidate_power_repeat = bpv_candidate_mkm_product_previous_val) -> (((exists ff_h_mkm_product_previous_val_candidate_power_repeat_decoded. ff_h_mkm_product_previous_val_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_previous_val_candidate_power_repeat)) * ff_c_mkm_product_previous_val_candidate_power)) /\ exists ff_q_mkm_product_previous_val_candidate_power_repeat_decoded. ff_b_mkm_product_previous_val_candidate_power = ff_q_mkm_product_previous_val_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_previous_val_candidate_power_repeat)) * ff_c_mkm_product_previous_val_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_previous_val_candidate_power_product ff_v_mkm_product_previous_val_candidate_power_product. ((((exists ff_h_mkm_product_previous_val_candidate_power_product_start. ff_h_mkm_product_previous_val_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_previous_val_candidate_power_product)) /\ exists ff_q_mkm_product_previous_val_candidate_power_product_start. ff_u_mkm_product_previous_val_candidate_power_product = ff_q_mkm_product_previous_val_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_previous_val_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_previous_val_candidate_power_product_terminal. ff_h_mkm_product_previous_val_candidate_power_product_terminal + S (bpv_result_mkm_product_previous_val_candidate) = S ((S (bpv_candidate_mkm_product_previous_val)) * ff_v_mkm_product_previous_val_candidate_power_product)) /\ exists ff_q_mkm_product_previous_val_candidate_power_product_terminal. ff_u_mkm_product_previous_val_candidate_power_product = ff_q_mkm_product_previous_val_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_previous_val)) * ff_v_mkm_product_previous_val_candidate_power_product) + (bpv_result_mkm_product_previous_val_candidate))) /\ forall ff_i_mkm_product_previous_val_candidate_power_product. (exists ff_lt_mkm_product_previous_val_candidate_power_product_bound. ff_lt_mkm_product_previous_val_candidate_power_product_bound + S ff_i_mkm_product_previous_val_candidate_power_product = bpv_candidate_mkm_product_previous_val) -> exists ff_p_mkm_product_previous_val_candidate_power_product ff_r_mkm_product_previous_val_candidate_power_product ff_s_mkm_product_previous_val_candidate_power_product. ((((exists ff_h_mkm_product_previous_val_candidate_power_product_factor. ff_h_mkm_product_previous_val_candidate_power_product_factor + S (ff_p_mkm_product_previous_val_candidate_power_product) = S ((S (ff_i_mkm_product_previous_val_candidate_power_product)) * ff_c_mkm_product_previous_val_candidate_power)) /\ exists ff_q_mkm_product_previous_val_candidate_power_product_factor. ff_b_mkm_product_previous_val_candidate_power = ff_q_mkm_product_previous_val_candidate_power_product_factor * S ((S (ff_i_mkm_product_previous_val_candidate_power_product)) * ff_c_mkm_product_previous_val_candidate_power) + (ff_p_mkm_product_previous_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_previous_val_candidate_power_product_partial. ff_h_mkm_product_previous_val_candidate_power_product_partial + S (ff_r_mkm_product_previous_val_candidate_power_product) = S ((S (ff_i_mkm_product_previous_val_candidate_power_product)) * ff_v_mkm_product_previous_val_candidate_power_product)) /\ exists ff_q_mkm_product_previous_val_candidate_power_product_partial. ff_u_mkm_product_previous_val_candidate_power_product = ff_q_mkm_product_previous_val_candidate_power_product_partial * S ((S (ff_i_mkm_product_previous_val_candidate_power_product)) * ff_v_mkm_product_previous_val_candidate_power_product) + (ff_r_mkm_product_previous_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_previous_val_candidate_power_product_successor. ff_h_mkm_product_previous_val_candidate_power_product_successor + S (ff_s_mkm_product_previous_val_candidate_power_product) = S ((S (S ff_i_mkm_product_previous_val_candidate_power_product)) * ff_v_mkm_product_previous_val_candidate_power_product)) /\ exists ff_q_mkm_product_previous_val_candidate_power_product_successor. ff_u_mkm_product_previous_val_candidate_power_product = ff_q_mkm_product_previous_val_candidate_power_product_successor * S ((S (S ff_i_mkm_product_previous_val_candidate_power_product)) * ff_v_mkm_product_previous_val_candidate_power_product) + (ff_s_mkm_product_previous_val_candidate_power_product))) /\ ff_s_mkm_product_previous_val_candidate_power_product = ff_r_mkm_product_previous_val_candidate_power_product * ff_p_mkm_product_previous_val_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_previous_val_candidate_divides. (x1) = bpv_result_mkm_product_previous_val_candidate * bpv_factor_mkm_product_previous_val_candidate_divides))) -> (exists bpv_gap_mkm_product_previous_val_maximal. bpv_gap_mkm_product_previous_val_maximal + bpv_candidate_mkm_product_previous_val = v)
  81. 0081specialize power_valuation_exists p
  82. 0082specialize power_valuation_exists x1
  83. 0083apply power_valuation_exists
  84. 0084cases hprevious
  85. 0085have hprevious_value : x4 = x3
  86. 0086specialize IH x1
  87. 0087specialize IH x3
  88. 0088specialize IH x4
  89. 0089apply IH
  90. 0090exact hp
  91. 0091exact hnprev
  92. 0092exact hvprev
  93. 0093exact hprodpart_witness_witness_right_left
  94. 0094exact hsumpart_witness_witness_right_left
  95. 0095exact hprevious_witness
  96. 0096rewrite hprevious_value at hprevious_witness
  97. 0097rewrite hprevious_value at hprevious_witness
  98. 0098rewrite hprevious_value at hprevious_witness
  99. 0099rewrite hprevious_value at hprevious_witness
  100. 0100rewrite hprevious_value at hprevious_witness
  101. 0101rewrite hprevious_value at hprevious_witness
  102. 0102have hlast : ((exists bpv_gap_mkm_product_last_val_exponent_bound. bpv_gap_mkm_product_last_val_exponent_bound + x2 = (x)) /\ (exists bpv_result_mkm_product_last_val_selected. ((exists ff_b_mkm_product_last_val_selected_power ff_c_mkm_product_last_val_selected_power. ((forall ff_i_mkm_product_last_val_selected_power_repeat. (exists ff_lt_mkm_product_last_val_selected_power_repeat_bound. ff_lt_mkm_product_last_val_selected_power_repeat_bound + S ff_i_mkm_product_last_val_selected_power_repeat = x2) -> (((exists ff_h_mkm_product_last_val_selected_power_repeat_decoded. ff_h_mkm_product_last_val_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_last_val_selected_power_repeat)) * ff_c_mkm_product_last_val_selected_power)) /\ exists ff_q_mkm_product_last_val_selected_power_repeat_decoded. ff_b_mkm_product_last_val_selected_power = ff_q_mkm_product_last_val_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_last_val_selected_power_repeat)) * ff_c_mkm_product_last_val_selected_power) + (p)))) /\ (exists ff_u_mkm_product_last_val_selected_power_product ff_v_mkm_product_last_val_selected_power_product. ((((exists ff_h_mkm_product_last_val_selected_power_product_start. ff_h_mkm_product_last_val_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_last_val_selected_power_product)) /\ exists ff_q_mkm_product_last_val_selected_power_product_start. ff_u_mkm_product_last_val_selected_power_product = ff_q_mkm_product_last_val_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_last_val_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_last_val_selected_power_product_terminal. ff_h_mkm_product_last_val_selected_power_product_terminal + S (bpv_result_mkm_product_last_val_selected) = S ((S (x2)) * ff_v_mkm_product_last_val_selected_power_product)) /\ exists ff_q_mkm_product_last_val_selected_power_product_terminal. ff_u_mkm_product_last_val_selected_power_product = ff_q_mkm_product_last_val_selected_power_product_terminal * S ((S (x2)) * ff_v_mkm_product_last_val_selected_power_product) + (bpv_result_mkm_product_last_val_selected))) /\ forall ff_i_mkm_product_last_val_selected_power_product. (exists ff_lt_mkm_product_last_val_selected_power_product_bound. ff_lt_mkm_product_last_val_selected_power_product_bound + S ff_i_mkm_product_last_val_selected_power_product = x2) -> exists ff_p_mkm_product_last_val_selected_power_product ff_r_mkm_product_last_val_selected_power_product ff_s_mkm_product_last_val_selected_power_product. ((((exists ff_h_mkm_product_last_val_selected_power_product_factor. ff_h_mkm_product_last_val_selected_power_product_factor + S (ff_p_mkm_product_last_val_selected_power_product) = S ((S (ff_i_mkm_product_last_val_selected_power_product)) * ff_c_mkm_product_last_val_selected_power)) /\ exists ff_q_mkm_product_last_val_selected_power_product_factor. ff_b_mkm_product_last_val_selected_power = ff_q_mkm_product_last_val_selected_power_product_factor * S ((S (ff_i_mkm_product_last_val_selected_power_product)) * ff_c_mkm_product_last_val_selected_power) + (ff_p_mkm_product_last_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_last_val_selected_power_product_partial. ff_h_mkm_product_last_val_selected_power_product_partial + S (ff_r_mkm_product_last_val_selected_power_product) = S ((S (ff_i_mkm_product_last_val_selected_power_product)) * ff_v_mkm_product_last_val_selected_power_product)) /\ exists ff_q_mkm_product_last_val_selected_power_product_partial. ff_u_mkm_product_last_val_selected_power_product = ff_q_mkm_product_last_val_selected_power_product_partial * S ((S (ff_i_mkm_product_last_val_selected_power_product)) * ff_v_mkm_product_last_val_selected_power_product) + (ff_r_mkm_product_last_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_last_val_selected_power_product_successor. ff_h_mkm_product_last_val_selected_power_product_successor + S (ff_s_mkm_product_last_val_selected_power_product) = S ((S (S ff_i_mkm_product_last_val_selected_power_product)) * ff_v_mkm_product_last_val_selected_power_product)) /\ exists ff_q_mkm_product_last_val_selected_power_product_successor. ff_u_mkm_product_last_val_selected_power_product = ff_q_mkm_product_last_val_selected_power_product_successor * S ((S (S ff_i_mkm_product_last_val_selected_power_product)) * ff_v_mkm_product_last_val_selected_power_product) + (ff_s_mkm_product_last_val_selected_power_product))) /\ ff_s_mkm_product_last_val_selected_power_product = ff_r_mkm_product_last_val_selected_power_product * ff_p_mkm_product_last_val_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_last_val_selected_divides. (x) = bpv_result_mkm_product_last_val_selected * bpv_factor_mkm_product_last_val_selected_divides)))) /\ forall bpv_candidate_mkm_product_last_val. (exists bpv_gap_mkm_product_last_val_candidate_bound. bpv_gap_mkm_product_last_val_candidate_bound + bpv_candidate_mkm_product_last_val = (x)) -> (exists bpv_result_mkm_product_last_val_candidate. ((exists ff_b_mkm_product_last_val_candidate_power ff_c_mkm_product_last_val_candidate_power. ((forall ff_i_mkm_product_last_val_candidate_power_repeat. (exists ff_lt_mkm_product_last_val_candidate_power_repeat_bound. ff_lt_mkm_product_last_val_candidate_power_repeat_bound + S ff_i_mkm_product_last_val_candidate_power_repeat = bpv_candidate_mkm_product_last_val) -> (((exists ff_h_mkm_product_last_val_candidate_power_repeat_decoded. ff_h_mkm_product_last_val_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_last_val_candidate_power_repeat)) * ff_c_mkm_product_last_val_candidate_power)) /\ exists ff_q_mkm_product_last_val_candidate_power_repeat_decoded. ff_b_mkm_product_last_val_candidate_power = ff_q_mkm_product_last_val_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_last_val_candidate_power_repeat)) * ff_c_mkm_product_last_val_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_last_val_candidate_power_product ff_v_mkm_product_last_val_candidate_power_product. ((((exists ff_h_mkm_product_last_val_candidate_power_product_start. ff_h_mkm_product_last_val_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_last_val_candidate_power_product)) /\ exists ff_q_mkm_product_last_val_candidate_power_product_start. ff_u_mkm_product_last_val_candidate_power_product = ff_q_mkm_product_last_val_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_last_val_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_last_val_candidate_power_product_terminal. ff_h_mkm_product_last_val_candidate_power_product_terminal + S (bpv_result_mkm_product_last_val_candidate) = S ((S (bpv_candidate_mkm_product_last_val)) * ff_v_mkm_product_last_val_candidate_power_product)) /\ exists ff_q_mkm_product_last_val_candidate_power_product_terminal. ff_u_mkm_product_last_val_candidate_power_product = ff_q_mkm_product_last_val_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_last_val)) * ff_v_mkm_product_last_val_candidate_power_product) + (bpv_result_mkm_product_last_val_candidate))) /\ forall ff_i_mkm_product_last_val_candidate_power_product. (exists ff_lt_mkm_product_last_val_candidate_power_product_bound. ff_lt_mkm_product_last_val_candidate_power_product_bound + S ff_i_mkm_product_last_val_candidate_power_product = bpv_candidate_mkm_product_last_val) -> exists ff_p_mkm_product_last_val_candidate_power_product ff_r_mkm_product_last_val_candidate_power_product ff_s_mkm_product_last_val_candidate_power_product. ((((exists ff_h_mkm_product_last_val_candidate_power_product_factor. ff_h_mkm_product_last_val_candidate_power_product_factor + S (ff_p_mkm_product_last_val_candidate_power_product) = S ((S (ff_i_mkm_product_last_val_candidate_power_product)) * ff_c_mkm_product_last_val_candidate_power)) /\ exists ff_q_mkm_product_last_val_candidate_power_product_factor. ff_b_mkm_product_last_val_candidate_power = ff_q_mkm_product_last_val_candidate_power_product_factor * S ((S (ff_i_mkm_product_last_val_candidate_power_product)) * ff_c_mkm_product_last_val_candidate_power) + (ff_p_mkm_product_last_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_last_val_candidate_power_product_partial. ff_h_mkm_product_last_val_candidate_power_product_partial + S (ff_r_mkm_product_last_val_candidate_power_product) = S ((S (ff_i_mkm_product_last_val_candidate_power_product)) * ff_v_mkm_product_last_val_candidate_power_product)) /\ exists ff_q_mkm_product_last_val_candidate_power_product_partial. ff_u_mkm_product_last_val_candidate_power_product = ff_q_mkm_product_last_val_candidate_power_product_partial * S ((S (ff_i_mkm_product_last_val_candidate_power_product)) * ff_v_mkm_product_last_val_candidate_power_product) + (ff_r_mkm_product_last_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_last_val_candidate_power_product_successor. ff_h_mkm_product_last_val_candidate_power_product_successor + S (ff_s_mkm_product_last_val_candidate_power_product) = S ((S (S ff_i_mkm_product_last_val_candidate_power_product)) * ff_v_mkm_product_last_val_candidate_power_product)) /\ exists ff_q_mkm_product_last_val_candidate_power_product_successor. ff_u_mkm_product_last_val_candidate_power_product = ff_q_mkm_product_last_val_candidate_power_product_successor * S ((S (S ff_i_mkm_product_last_val_candidate_power_product)) * ff_v_mkm_product_last_val_candidate_power_product) + (ff_s_mkm_product_last_val_candidate_power_product))) /\ ff_s_mkm_product_last_val_candidate_power_product = ff_r_mkm_product_last_val_candidate_power_product * ff_p_mkm_product_last_val_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_last_val_candidate_divides. (x) = bpv_result_mkm_product_last_val_candidate * bpv_factor_mkm_product_last_val_candidate_divides))) -> (exists bpv_gap_mkm_product_last_val_maximal. bpv_gap_mkm_product_last_val_maximal + bpv_candidate_mkm_product_last_val = x2)
  103. 0103specialize beta_valuation_prefix_last p
  104. 0104specialize beta_valuation_prefix_last b
  105. 0105specialize beta_valuation_prefix_last c
  106. 0106specialize beta_valuation_prefix_last vb
  107. 0107specialize beta_valuation_prefix_last vc
  108. 0108specialize beta_valuation_prefix_last l
  109. 0109specialize beta_valuation_prefix_last x
  110. 0110specialize beta_valuation_prefix_last x2
  111. 0111apply beta_valuation_prefix_last
  112. 0112exact hv
  113. 0113exact hprodpart_witness_witness_left
  114. 0114exact hsumpart_witness_witness_left
  115. 0115rewrite hprodpart_witness_witness_right_right at hg
  116. 0116rewrite hprodpart_witness_witness_right_right at hg
  117. 0117rewrite hprodpart_witness_witness_right_right at hg
  118. 0118rewrite hprodpart_witness_witness_right_right at hg
  119. 0119trans x3 + x2
  120. 0120specialize prime_power_valuation_mul p
  121. 0121specialize prime_power_valuation_mul x1
  122. 0122specialize prime_power_valuation_mul x
  123. 0123specialize prime_power_valuation_mul x3
  124. 0124specialize prime_power_valuation_mul x2
  125. 0125specialize prime_power_valuation_mul g
  126. 0126apply prime_power_valuation_mul
  127. 0127exact hp
  128. 0128intro hzero
  129. 0129specialize crt_positive_moduli_prefix_product_nonzero b
  130. 0130specialize crt_positive_moduli_prefix_product_nonzero c
  131. 0131specialize crt_positive_moduli_prefix_product_nonzero l
  132. 0132specialize crt_positive_moduli_prefix_product_nonzero x1
  133. 0133apply crt_positive_moduli_prefix_product_nonzero
  134. 0134exact hnprev
  135. 0135exact hprodpart_witness_witness_right_left
  136. 0136exact hzero
  137. 0137intro hzero
  138. 0138specialize crt_positive_moduli_prefix_last_nonzero b
  139. 0139specialize crt_positive_moduli_prefix_last_nonzero c
  140. 0140specialize crt_positive_moduli_prefix_last_nonzero l
  141. 0141specialize crt_positive_moduli_prefix_last_nonzero x
  142. 0142apply crt_positive_moduli_prefix_last_nonzero
  143. 0143exact hn
  144. 0144exact hprodpart_witness_witness_left
  145. 0145exact hzero
  146. 0146exact hprevious_witness
  147. 0147exact hlast
  148. 0148exact hg
  149. 0149symm
  150. 0150exact hsumpart_witness_witness_right_right