prime_field_polynomial_synthetic_zero_remainder_iff

Exact expanded first-order arithmetic statement

forall p b c a n qb qc r. (~((p) = 1) /\ forall pfa_factor_left_root_prime pfa_factor_right_root_prime. (p) = pfa_factor_left_root_prime * pfa_factor_right_root_prime -> pfa_factor_left_root_prime = 1 \/ pfa_factor_right_root_prime = 1) -> (exists pfs_history_code_root_division pfs_history_scale_root_division. ((((exists pfa_gap_root_divisiontracebase. pfa_gap_root_divisiontracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_divisiontraceinitial. ff_h_pfp_root_divisiontraceinitial + S (0) = S ((S (0)) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontraceinitial. pfs_history_code_root_division = ff_q_pfp_root_divisiontraceinitial * S ((S (0)) * pfs_history_scale_root_division) + (0))) /\ (((((exists ff_h_pfp_root_divisiontraceterminal. ff_h_pfp_root_divisiontraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontraceterminal. pfs_history_code_root_division = ff_q_pfp_root_divisiontraceterminal * S ((S (S (n))) * pfs_history_scale_root_division) + (r))) /\ ((forall pfh_index_root_divisiontracesteps. (exists pfa_gap_root_divisiontracestepsindex. pfa_gap_root_divisiontracestepsindex + S (pfh_index_root_divisiontracesteps) = (S (n))) -> (exists pfh_coefficient_root_divisiontracestepsstep pfh_before_root_divisiontracestepsstep pfh_after_root_divisiontracestepsstep pfh_product_root_divisiontracestepsstep. ((((exists ff_h_pfp_root_divisiontracestepsstepcoefficient. ff_h_pfp_root_divisiontracestepsstepcoefficient + S (pfh_coefficient_root_divisiontracestepsstep) = S ((S (pfh_index_root_divisiontracesteps)) * c)) /\ exists ff_q_pfp_root_divisiontracestepsstepcoefficient. b = ff_q_pfp_root_divisiontracestepsstepcoefficient * S ((S (pfh_index_root_divisiontracesteps)) * c) + (pfh_coefficient_root_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_root_divisiontracestepsstepbefore. ff_h_pfp_root_divisiontracestepsstepbefore + S (pfh_before_root_divisiontracestepsstep) = S ((S (pfh_index_root_divisiontracesteps)) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontracestepsstepbefore. pfs_history_code_root_division = ff_q_pfp_root_divisiontracestepsstepbefore * S ((S (pfh_index_root_divisiontracesteps)) * pfs_history_scale_root_division) + (pfh_before_root_divisiontracestepsstep))) /\ (((((exists ff_h_pfp_root_divisiontracestepsstepafter. ff_h_pfp_root_divisiontracestepsstepafter + S (pfh_after_root_divisiontracestepsstep) = S ((S (S (pfh_index_root_divisiontracesteps))) * pfs_history_scale_root_division)) /\ exists ff_q_pfp_root_divisiontracestepsstepafter. pfs_history_code_root_division = ff_q_pfp_root_divisiontracestepsstepafter * S ((S (S (pfh_index_root_divisiontracesteps))) * pfs_history_scale_root_division) + (pfh_after_root_divisiontracestepsstep))) /\ (((((exists pfa_gap_root_divisiontracestepsstepmultiplyleft. pfa_gap_root_divisiontracestepsstepmultiplyleft + S (pfh_before_root_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_root_divisiontracestepsstepmultiplyright. pfa_gap_root_divisiontracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_divisiontracestepsstepmultiplyresultbound. pfa_gap_root_divisiontracestepsstepmultiplyresultbound + S (pfh_product_root_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_divisiontracestepsstepmultiplyresultcongruence pfa_offset_right_root_divisiontracestepsstepmultiplyresultcongruence. ((pfh_before_root_divisiontracestepsstep) * (a)) + (p) * pfa_offset_left_root_divisiontracestepsstepmultiplyresultcongruence = (pfh_product_root_divisiontracestepsstep) + (p) * pfa_offset_right_root_divisiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_divisiontracestepsstepaddleft. pfa_gap_root_divisiontracestepsstepaddleft + S (pfh_product_root_divisiontracestepsstep) = (p)) /\ (((exists pfa_gap_root_divisiontracestepsstepaddright. pfa_gap_root_divisiontracestepsstepaddright + S (pfh_coefficient_root_divisiontracestepsstep) = (p)) /\ ((((exists pfa_gap_root_divisiontracestepsstepaddresultbound. pfa_gap_root_divisiontracestepsstepaddresultbound + S (pfh_after_root_divisiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_divisiontracestepsstepaddresultcongruence pfa_offset_right_root_divisiontracestepsstepaddresultcongruence. ((pfh_product_root_divisiontracestepsstep) + (pfh_coefficient_root_divisiontracestepsstep)) + (p) * pfa_offset_left_root_divisiontracestepsstepaddresultcongruence = (pfh_after_root_divisiontracestepsstep) + (p) * pfa_offset_right_root_divisiontracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_root_divisionquotient ff_source_mcp_pfs_root_divisionquotient ff_target_mcp_pfs_root_divisionquotient. (exists mcp_gap_pfs_root_divisionquotient_bound. mcp_gap_pfs_root_divisionquotient_bound + S (ff_index_mcp_pfs_root_divisionquotient) = (n)) -> (((exists fs_h_mcp_pfs_root_divisionquotient_source. fs_h_mcp_pfs_root_divisionquotient_source + S (ff_source_mcp_pfs_root_divisionquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_root_divisionquotient)) * pfs_history_scale_root_division)) /\ exists fs_q_mcp_pfs_root_divisionquotient_source. pfs_history_code_root_division = fs_q_mcp_pfs_root_divisionquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_root_divisionquotient)) * pfs_history_scale_root_division) + (ff_source_mcp_pfs_root_divisionquotient))) -> (((exists fs_h_mcp_pfs_root_divisionquotient_target. fs_h_mcp_pfs_root_divisionquotient_target + S (ff_target_mcp_pfs_root_divisionquotient) = S ((S (ff_index_mcp_pfs_root_divisionquotient)) * qc)) /\ exists fs_q_mcp_pfs_root_divisionquotient_target. qb = fs_q_mcp_pfs_root_divisionquotient_target * S ((S (ff_index_mcp_pfs_root_divisionquotient)) * qc) + (ff_target_mcp_pfs_root_divisionquotient))) -> ff_target_mcp_pfs_root_divisionquotient = ff_source_mcp_pfs_root_divisionquotient)))) -> ((r=0 -> (exists pfh_trace_code_root_forward pfh_trace_scale_root_forward. (((exists pfa_gap_root_forwardtracebase. pfa_gap_root_forwardtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_forwardtraceinitial. ff_h_pfp_root_forwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtraceinitial. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtraceinitial * S ((S (0)) * pfh_trace_scale_root_forward) + (0))) /\ (((((exists ff_h_pfp_root_forwardtraceterminal. ff_h_pfp_root_forwardtraceterminal + S (0) = S ((S (S n)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtraceterminal. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtraceterminal * S ((S (S n)) * pfh_trace_scale_root_forward) + (0))) /\ ((forall pfh_index_root_forwardtracesteps. (exists pfa_gap_root_forwardtracestepsindex. pfa_gap_root_forwardtracestepsindex + S (pfh_index_root_forwardtracesteps) = (S n)) -> (exists pfh_coefficient_root_forwardtracestepsstep pfh_before_root_forwardtracestepsstep pfh_after_root_forwardtracestepsstep pfh_product_root_forwardtracestepsstep. ((((exists ff_h_pfp_root_forwardtracestepsstepcoefficient. ff_h_pfp_root_forwardtracestepsstepcoefficient + S (pfh_coefficient_root_forwardtracestepsstep) = S ((S (pfh_index_root_forwardtracesteps)) * c)) /\ exists ff_q_pfp_root_forwardtracestepsstepcoefficient. b = ff_q_pfp_root_forwardtracestepsstepcoefficient * S ((S (pfh_index_root_forwardtracesteps)) * c) + (pfh_coefficient_root_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_forwardtracestepsstepbefore. ff_h_pfp_root_forwardtracestepsstepbefore + S (pfh_before_root_forwardtracestepsstep) = S ((S (pfh_index_root_forwardtracesteps)) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtracestepsstepbefore. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtracestepsstepbefore * S ((S (pfh_index_root_forwardtracesteps)) * pfh_trace_scale_root_forward) + (pfh_before_root_forwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_forwardtracestepsstepafter. ff_h_pfp_root_forwardtracestepsstepafter + S (pfh_after_root_forwardtracestepsstep) = S ((S (S (pfh_index_root_forwardtracesteps))) * pfh_trace_scale_root_forward)) /\ exists ff_q_pfp_root_forwardtracestepsstepafter. pfh_trace_code_root_forward = ff_q_pfp_root_forwardtracestepsstepafter * S ((S (S (pfh_index_root_forwardtracesteps))) * pfh_trace_scale_root_forward) + (pfh_after_root_forwardtracestepsstep))) /\ (((((exists pfa_gap_root_forwardtracestepsstepmultiplyleft. pfa_gap_root_forwardtracestepsstepmultiplyleft + S (pfh_before_root_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_forwardtracestepsstepmultiplyright. pfa_gap_root_forwardtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_forwardtracestepsstepmultiplyresultbound. pfa_gap_root_forwardtracestepsstepmultiplyresultbound + S (pfh_product_root_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_forwardtracestepsstepmultiplyresultcongruence pfa_offset_right_root_forwardtracestepsstepmultiplyresultcongruence. ((pfh_before_root_forwardtracestepsstep) * (a)) + (p) * pfa_offset_left_root_forwardtracestepsstepmultiplyresultcongruence = (pfh_product_root_forwardtracestepsstep) + (p) * pfa_offset_right_root_forwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_forwardtracestepsstepaddleft. pfa_gap_root_forwardtracestepsstepaddleft + S (pfh_product_root_forwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_forwardtracestepsstepaddright. pfa_gap_root_forwardtracestepsstepaddright + S (pfh_coefficient_root_forwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_root_forwardtracestepsstepaddresultbound. pfa_gap_root_forwardtracestepsstepaddresultbound + S (pfh_after_root_forwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_forwardtracestepsstepaddresultcongruence pfa_offset_right_root_forwardtracestepsstepaddresultcongruence. ((pfh_product_root_forwardtracestepsstep) + (pfh_coefficient_root_forwardtracestepsstep)) + (p) * pfa_offset_left_root_forwardtracestepsstepaddresultcongruence = (pfh_after_root_forwardtracestepsstep) + (p) * pfa_offset_right_root_forwardtracestepsstepaddresultcongruence)))))))))))))))))))))))))))) /\ (((exists pfh_trace_code_root_backward pfh_trace_scale_root_backward. (((exists pfa_gap_root_backwardtracebase. pfa_gap_root_backwardtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_root_backwardtraceinitial. ff_h_pfp_root_backwardtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtraceinitial. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtraceinitial * S ((S (0)) * pfh_trace_scale_root_backward) + (0))) /\ (((((exists ff_h_pfp_root_backwardtraceterminal. ff_h_pfp_root_backwardtraceterminal + S (0) = S ((S (S n)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtraceterminal. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtraceterminal * S ((S (S n)) * pfh_trace_scale_root_backward) + (0))) /\ ((forall pfh_index_root_backwardtracesteps. (exists pfa_gap_root_backwardtracestepsindex. pfa_gap_root_backwardtracestepsindex + S (pfh_index_root_backwardtracesteps) = (S n)) -> (exists pfh_coefficient_root_backwardtracestepsstep pfh_before_root_backwardtracestepsstep pfh_after_root_backwardtracestepsstep pfh_product_root_backwardtracestepsstep. ((((exists ff_h_pfp_root_backwardtracestepsstepcoefficient. ff_h_pfp_root_backwardtracestepsstepcoefficient + S (pfh_coefficient_root_backwardtracestepsstep) = S ((S (pfh_index_root_backwardtracesteps)) * c)) /\ exists ff_q_pfp_root_backwardtracestepsstepcoefficient. b = ff_q_pfp_root_backwardtracestepsstepcoefficient * S ((S (pfh_index_root_backwardtracesteps)) * c) + (pfh_coefficient_root_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_backwardtracestepsstepbefore. ff_h_pfp_root_backwardtracestepsstepbefore + S (pfh_before_root_backwardtracestepsstep) = S ((S (pfh_index_root_backwardtracesteps)) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtracestepsstepbefore. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtracestepsstepbefore * S ((S (pfh_index_root_backwardtracesteps)) * pfh_trace_scale_root_backward) + (pfh_before_root_backwardtracestepsstep))) /\ (((((exists ff_h_pfp_root_backwardtracestepsstepafter. ff_h_pfp_root_backwardtracestepsstepafter + S (pfh_after_root_backwardtracestepsstep) = S ((S (S (pfh_index_root_backwardtracesteps))) * pfh_trace_scale_root_backward)) /\ exists ff_q_pfp_root_backwardtracestepsstepafter. pfh_trace_code_root_backward = ff_q_pfp_root_backwardtracestepsstepafter * S ((S (S (pfh_index_root_backwardtracesteps))) * pfh_trace_scale_root_backward) + (pfh_after_root_backwardtracestepsstep))) /\ (((((exists pfa_gap_root_backwardtracestepsstepmultiplyleft. pfa_gap_root_backwardtracestepsstepmultiplyleft + S (pfh_before_root_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_backwardtracestepsstepmultiplyright. pfa_gap_root_backwardtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_root_backwardtracestepsstepmultiplyresultbound. pfa_gap_root_backwardtracestepsstepmultiplyresultbound + S (pfh_product_root_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_backwardtracestepsstepmultiplyresultcongruence pfa_offset_right_root_backwardtracestepsstepmultiplyresultcongruence. ((pfh_before_root_backwardtracestepsstep) * (a)) + (p) * pfa_offset_left_root_backwardtracestepsstepmultiplyresultcongruence = (pfh_product_root_backwardtracestepsstep) + (p) * pfa_offset_right_root_backwardtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_root_backwardtracestepsstepaddleft. pfa_gap_root_backwardtracestepsstepaddleft + S (pfh_product_root_backwardtracestepsstep) = (p)) /\ (((exists pfa_gap_root_backwardtracestepsstepaddright. pfa_gap_root_backwardtracestepsstepaddright + S (pfh_coefficient_root_backwardtracestepsstep) = (p)) /\ ((((exists pfa_gap_root_backwardtracestepsstepaddresultbound. pfa_gap_root_backwardtracestepsstepaddresultbound + S (pfh_after_root_backwardtracestepsstep) = (p)) /\ ((exists pfa_offset_left_root_backwardtracestepsstepaddresultcongruence pfa_offset_right_root_backwardtracestepsstepaddresultcongruence. ((pfh_product_root_backwardtracestepsstep) + (pfh_coefficient_root_backwardtracestepsstep)) + (p) * pfa_offset_left_root_backwardtracestepsstepaddresultcongruence = (pfh_after_root_backwardtracestepsstep) + (p) * pfa_offset_right_root_backwardtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> r=0)))