prime_scaled_inverse_prefix_exists

Exact expanded PA statement

forall p a n. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_full_prime esi_prime_right_esip_full_prime. p = esi_prime_left_esip_full_prime * esi_prime_right_esip_full_prime -> esi_prime_left_esip_full_prime = 1 \/ esi_prime_right_esip_full_prime = 1)) -> ~(a = 0) -> (exists esip_gap_full_target_bound. esip_gap_full_target_bound + S (a) = p) -> exists b c. (forall esip_index_full_result. (exists esip_gap_full_result_prefix_bound. esip_gap_full_result_prefix_bound + S (esip_index_full_result) = n) -> exists esip_mate_full_result. ((((exists ff_h_esip_full_result_entry. ff_h_esip_full_result_entry + S (esip_mate_full_result) = S ((S (esip_index_full_result)) * c)) /\ exists ff_q_esip_full_result_entry. b = ff_q_esip_full_result_entry * S ((S (esip_index_full_result)) * c) + (esip_mate_full_result))) /\ ((exists esip_gap_full_result_relation_index_bound. esip_gap_full_result_relation_index_bound + S (esip_index_full_result) = n) /\ ((((~((S esip_index_full_result) = 0) /\ (exists esip_gap_full_result_relation_scaled_left_bound. esip_gap_full_result_relation_scaled_left_bound + S (S esip_index_full_result) = p))) /\ (((~(esip_mate_full_result = 0) /\ (exists esip_gap_full_result_relation_scaled_right_bound. esip_gap_full_result_relation_scaled_right_bound + S (esip_mate_full_result) = p))) /\ (exists esi_mod_left_full_result_relation_scaled_mod esi_mod_right_full_result_relation_scaled_mod. ((S esip_index_full_result) * esip_mate_full_result) + p * esi_mod_left_full_result_relation_scaled_mod = (a) + p * esi_mod_right_full_result_relation_scaled_mod)))))))