prime_valuation_exponent_eq_transport

Exact expanded first-order arithmetic statement

forall p n e f. e = f -> (((exists bpd_gap_pvs_transport_source_selected_bound. bpd_gap_pvs_transport_source_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_transport_source_selected. ((exists bpvi_b_pvs_transport_source_selected_power bpvi_c_pvs_transport_source_selected_power. ((forall bpvi_i_pvs_transport_source_selected_power. (exists bpvi_repeat_gap_pvs_transport_source_selected_power. bpvi_repeat_gap_pvs_transport_source_selected_power + S bpvi_i_pvs_transport_source_selected_power = e) -> (((exists bpvi_h_pvs_transport_source_selected_power_repeat. bpvi_h_pvs_transport_source_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_repeat. bpvi_b_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_repeat * S ((S (bpvi_i_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power) + (p)))) /\ (exists bpvi_u_pvs_transport_source_selected_power bpvi_v_pvs_transport_source_selected_power. ((((exists bpvi_h_pvs_transport_source_selected_power_start. bpvi_h_pvs_transport_source_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_start. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_start * S ((S (0)) * bpvi_v_pvs_transport_source_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_terminal. bpvi_h_pvs_transport_source_selected_power_terminal + S (bpvi_result_pvs_transport_source_selected) = S ((S (e)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_terminal. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_result_pvs_transport_source_selected))) /\ forall bpvi_j_pvs_transport_source_selected_power. (exists bpvi_product_gap_pvs_transport_source_selected_power. bpvi_product_gap_pvs_transport_source_selected_power + S bpvi_j_pvs_transport_source_selected_power = e) -> exists bpvi_factor_pvs_transport_source_selected_power bpvi_partial_pvs_transport_source_selected_power bpvi_successor_pvs_transport_source_selected_power. ((((exists bpvi_h_pvs_transport_source_selected_power_factor. bpvi_h_pvs_transport_source_selected_power_factor + S (bpvi_factor_pvs_transport_source_selected_power) = S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_factor. bpvi_b_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_factor * S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power) + (bpvi_factor_pvs_transport_source_selected_power))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_partial. bpvi_h_pvs_transport_source_selected_power_partial + S (bpvi_partial_pvs_transport_source_selected_power) = S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_partial. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_partial * S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_partial_pvs_transport_source_selected_power))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_successor. bpvi_h_pvs_transport_source_selected_power_successor + S (bpvi_successor_pvs_transport_source_selected_power) = S ((S (S bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_successor. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_successor * S ((S (S bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_successor_pvs_transport_source_selected_power))) /\ bpvi_successor_pvs_transport_source_selected_power = bpvi_partial_pvs_transport_source_selected_power * bpvi_factor_pvs_transport_source_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_source_selected. n = bpvi_result_pvs_transport_source_selected * bpvi_divisor_factor_pvs_transport_source_selected))) /\ forall bpd_candidate_pvs_transport_source. (exists bpd_gap_pvs_transport_source_candidate_bound. bpd_gap_pvs_transport_source_candidate_bound + (bpd_candidate_pvs_transport_source) = (n)) -> (exists bpvi_result_pvs_transport_source_candidate. ((exists bpvi_b_pvs_transport_source_candidate_power bpvi_c_pvs_transport_source_candidate_power. ((forall bpvi_i_pvs_transport_source_candidate_power. (exists bpvi_repeat_gap_pvs_transport_source_candidate_power. bpvi_repeat_gap_pvs_transport_source_candidate_power + S bpvi_i_pvs_transport_source_candidate_power = bpd_candidate_pvs_transport_source) -> (((exists bpvi_h_pvs_transport_source_candidate_power_repeat. bpvi_h_pvs_transport_source_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_repeat. bpvi_b_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_repeat * S ((S (bpvi_i_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_transport_source_candidate_power bpvi_v_pvs_transport_source_candidate_power. ((((exists bpvi_h_pvs_transport_source_candidate_power_start. bpvi_h_pvs_transport_source_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_start. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_start * S ((S (0)) * bpvi_v_pvs_transport_source_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_terminal. bpvi_h_pvs_transport_source_candidate_power_terminal + S (bpvi_result_pvs_transport_source_candidate) = S ((S (bpd_candidate_pvs_transport_source)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_terminal. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_terminal * S ((S (bpd_candidate_pvs_transport_source)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_result_pvs_transport_source_candidate))) /\ forall bpvi_j_pvs_transport_source_candidate_power. (exists bpvi_product_gap_pvs_transport_source_candidate_power. bpvi_product_gap_pvs_transport_source_candidate_power + S bpvi_j_pvs_transport_source_candidate_power = bpd_candidate_pvs_transport_source) -> exists bpvi_factor_pvs_transport_source_candidate_power bpvi_partial_pvs_transport_source_candidate_power bpvi_successor_pvs_transport_source_candidate_power. ((((exists bpvi_h_pvs_transport_source_candidate_power_factor. bpvi_h_pvs_transport_source_candidate_power_factor + S (bpvi_factor_pvs_transport_source_candidate_power) = S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_factor. bpvi_b_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_factor * S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power) + (bpvi_factor_pvs_transport_source_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_partial. bpvi_h_pvs_transport_source_candidate_power_partial + S (bpvi_partial_pvs_transport_source_candidate_power) = S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_partial. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_partial * S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_partial_pvs_transport_source_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_successor. bpvi_h_pvs_transport_source_candidate_power_successor + S (bpvi_successor_pvs_transport_source_candidate_power) = S ((S (S bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_successor. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_successor * S ((S (S bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_successor_pvs_transport_source_candidate_power))) /\ bpvi_successor_pvs_transport_source_candidate_power = bpvi_partial_pvs_transport_source_candidate_power * bpvi_factor_pvs_transport_source_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_source_candidate. n = bpvi_result_pvs_transport_source_candidate * bpvi_divisor_factor_pvs_transport_source_candidate)) -> (exists bpd_gap_pvs_transport_source_maximal. bpd_gap_pvs_transport_source_maximal + (bpd_candidate_pvs_transport_source) = (e))) -> (((exists bpd_gap_pvs_transport_target_selected_bound. bpd_gap_pvs_transport_target_selected_bound + (f) = (n)) /\ (exists bpvi_result_pvs_transport_target_selected. ((exists bpvi_b_pvs_transport_target_selected_power bpvi_c_pvs_transport_target_selected_power. ((forall bpvi_i_pvs_transport_target_selected_power. (exists bpvi_repeat_gap_pvs_transport_target_selected_power. bpvi_repeat_gap_pvs_transport_target_selected_power + S bpvi_i_pvs_transport_target_selected_power = f) -> (((exists bpvi_h_pvs_transport_target_selected_power_repeat. bpvi_h_pvs_transport_target_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_repeat. bpvi_b_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_repeat * S ((S (bpvi_i_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power) + (p)))) /\ (exists bpvi_u_pvs_transport_target_selected_power bpvi_v_pvs_transport_target_selected_power. ((((exists bpvi_h_pvs_transport_target_selected_power_start. bpvi_h_pvs_transport_target_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_start. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_start * S ((S (0)) * bpvi_v_pvs_transport_target_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_terminal. bpvi_h_pvs_transport_target_selected_power_terminal + S (bpvi_result_pvs_transport_target_selected) = S ((S (f)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_terminal. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_result_pvs_transport_target_selected))) /\ forall bpvi_j_pvs_transport_target_selected_power. (exists bpvi_product_gap_pvs_transport_target_selected_power. bpvi_product_gap_pvs_transport_target_selected_power + S bpvi_j_pvs_transport_target_selected_power = f) -> exists bpvi_factor_pvs_transport_target_selected_power bpvi_partial_pvs_transport_target_selected_power bpvi_successor_pvs_transport_target_selected_power. ((((exists bpvi_h_pvs_transport_target_selected_power_factor. bpvi_h_pvs_transport_target_selected_power_factor + S (bpvi_factor_pvs_transport_target_selected_power) = S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_factor. bpvi_b_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_factor * S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power) + (bpvi_factor_pvs_transport_target_selected_power))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_partial. bpvi_h_pvs_transport_target_selected_power_partial + S (bpvi_partial_pvs_transport_target_selected_power) = S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_partial. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_partial * S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_partial_pvs_transport_target_selected_power))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_successor. bpvi_h_pvs_transport_target_selected_power_successor + S (bpvi_successor_pvs_transport_target_selected_power) = S ((S (S bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_successor. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_successor * S ((S (S bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_successor_pvs_transport_target_selected_power))) /\ bpvi_successor_pvs_transport_target_selected_power = bpvi_partial_pvs_transport_target_selected_power * bpvi_factor_pvs_transport_target_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_target_selected. n = bpvi_result_pvs_transport_target_selected * bpvi_divisor_factor_pvs_transport_target_selected))) /\ forall bpd_candidate_pvs_transport_target. (exists bpd_gap_pvs_transport_target_candidate_bound. bpd_gap_pvs_transport_target_candidate_bound + (bpd_candidate_pvs_transport_target) = (n)) -> (exists bpvi_result_pvs_transport_target_candidate. ((exists bpvi_b_pvs_transport_target_candidate_power bpvi_c_pvs_transport_target_candidate_power. ((forall bpvi_i_pvs_transport_target_candidate_power. (exists bpvi_repeat_gap_pvs_transport_target_candidate_power. bpvi_repeat_gap_pvs_transport_target_candidate_power + S bpvi_i_pvs_transport_target_candidate_power = bpd_candidate_pvs_transport_target) -> (((exists bpvi_h_pvs_transport_target_candidate_power_repeat. bpvi_h_pvs_transport_target_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_repeat. bpvi_b_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_repeat * S ((S (bpvi_i_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_transport_target_candidate_power bpvi_v_pvs_transport_target_candidate_power. ((((exists bpvi_h_pvs_transport_target_candidate_power_start. bpvi_h_pvs_transport_target_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_start. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_start * S ((S (0)) * bpvi_v_pvs_transport_target_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_terminal. bpvi_h_pvs_transport_target_candidate_power_terminal + S (bpvi_result_pvs_transport_target_candidate) = S ((S (bpd_candidate_pvs_transport_target)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_terminal. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_terminal * S ((S (bpd_candidate_pvs_transport_target)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_result_pvs_transport_target_candidate))) /\ forall bpvi_j_pvs_transport_target_candidate_power. (exists bpvi_product_gap_pvs_transport_target_candidate_power. bpvi_product_gap_pvs_transport_target_candidate_power + S bpvi_j_pvs_transport_target_candidate_power = bpd_candidate_pvs_transport_target) -> exists bpvi_factor_pvs_transport_target_candidate_power bpvi_partial_pvs_transport_target_candidate_power bpvi_successor_pvs_transport_target_candidate_power. ((((exists bpvi_h_pvs_transport_target_candidate_power_factor. bpvi_h_pvs_transport_target_candidate_power_factor + S (bpvi_factor_pvs_transport_target_candidate_power) = S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_factor. bpvi_b_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_factor * S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power) + (bpvi_factor_pvs_transport_target_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_partial. bpvi_h_pvs_transport_target_candidate_power_partial + S (bpvi_partial_pvs_transport_target_candidate_power) = S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_partial. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_partial * S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_partial_pvs_transport_target_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_successor. bpvi_h_pvs_transport_target_candidate_power_successor + S (bpvi_successor_pvs_transport_target_candidate_power) = S ((S (S bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_successor. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_successor * S ((S (S bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_successor_pvs_transport_target_candidate_power))) /\ bpvi_successor_pvs_transport_target_candidate_power = bpvi_partial_pvs_transport_target_candidate_power * bpvi_factor_pvs_transport_target_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_target_candidate. n = bpvi_result_pvs_transport_target_candidate * bpvi_divisor_factor_pvs_transport_target_candidate)) -> (exists bpd_gap_pvs_transport_target_maximal. bpd_gap_pvs_transport_target_maximal + (bpd_candidate_pvs_transport_target) = (f)))