prime_field_polynomial_empty_right_divisor_implies_equivalent_zero

Exact expanded first-order arithmetic statement

forall p db dc ab ac L. (((forall fom_index_pfp_empty_divisor_canonical. (exists fom_gap_pfp_empty_divisor_canonical_index_bound. fom_gap_pfp_empty_divisor_canonical_index_bound + S (fom_index_pfp_empty_divisor_canonical) = L) -> exists fom_value_pfp_empty_divisor_canonical. ((((exists fom_beta_height_pfp_empty_divisor_canonical_entry. fom_beta_height_pfp_empty_divisor_canonical_entry + S (fom_value_pfp_empty_divisor_canonical) = S ((S (fom_index_pfp_empty_divisor_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_empty_divisor_canonical_entry. ab = fom_beta_quotient_pfp_empty_divisor_canonical_entry * S ((S (fom_index_pfp_empty_divisor_canonical)) * ac) + (fom_value_pfp_empty_divisor_canonical))) /\ (exists fom_gap_pfp_empty_divisor_canonical_value_bound. fom_gap_pfp_empty_divisor_canonical_value_bound + S (fom_value_pfp_empty_divisor_canonical) = p))) /\ ((exists pfgu_qb_empty_divisor pfgu_qc_empty_divisor pfgu_Q_empty_divisor pfgu_pb_empty_divisor pfgu_pc_empty_divisor pfgu_P_empty_divisor. ((((forall fom_index_pfp_empty_divisor_productleft. (exists fom_gap_pfp_empty_divisor_productleft_index_bound. fom_gap_pfp_empty_divisor_productleft_index_bound + S (fom_index_pfp_empty_divisor_productleft) = pfgu_Q_empty_divisor) -> exists fom_value_pfp_empty_divisor_productleft. ((((exists fom_beta_height_pfp_empty_divisor_productleft_entry. fom_beta_height_pfp_empty_divisor_productleft_entry + S (fom_value_pfp_empty_divisor_productleft) = S ((S (fom_index_pfp_empty_divisor_productleft)) * pfgu_qc_empty_divisor)) /\ exists fom_beta_quotient_pfp_empty_divisor_productleft_entry. pfgu_qb_empty_divisor = fom_beta_quotient_pfp_empty_divisor_productleft_entry * S ((S (fom_index_pfp_empty_divisor_productleft)) * pfgu_qc_empty_divisor) + (fom_value_pfp_empty_divisor_productleft))) /\ (exists fom_gap_pfp_empty_divisor_productleft_value_bound. fom_gap_pfp_empty_divisor_productleft_value_bound + S (fom_value_pfp_empty_divisor_productleft) = p))) /\ (((forall fom_index_pfp_empty_divisor_productright. (exists fom_gap_pfp_empty_divisor_productright_index_bound. fom_gap_pfp_empty_divisor_productright_index_bound + S (fom_index_pfp_empty_divisor_productright) = 0) -> exists fom_value_pfp_empty_divisor_productright. ((((exists fom_beta_height_pfp_empty_divisor_productright_entry. fom_beta_height_pfp_empty_divisor_productright_entry + S (fom_value_pfp_empty_divisor_productright) = S ((S (fom_index_pfp_empty_divisor_productright)) * dc)) /\ exists fom_beta_quotient_pfp_empty_divisor_productright_entry. db = fom_beta_quotient_pfp_empty_divisor_productright_entry * S ((S (fom_index_pfp_empty_divisor_productright)) * dc) + (fom_value_pfp_empty_divisor_productright))) /\ (exists fom_gap_pfp_empty_divisor_productright_value_bound. fom_gap_pfp_empty_divisor_productright_value_bound + S (fom_value_pfp_empty_divisor_productright) = p))) /\ (((((((pfgu_Q_empty_divisor)=0 \/ (0)=0) /\ (((pfgu_P_empty_divisor)=0)))) \/ (((~((pfgu_Q_empty_divisor)=0)) /\ (((~((0)=0)) /\ (((pfgu_Q_empty_divisor)+(0)=S (pfgu_P_empty_divisor)))))))) /\ ((forall pfc_index_empty_divisor_productcoefficients. (exists pfa_gap_empty_divisor_productcoefficientsbound. pfa_gap_empty_divisor_productcoefficientsbound + S (pfc_index_empty_divisor_productcoefficients) = (pfgu_P_empty_divisor)) -> exists pfc_value_empty_divisor_productcoefficients. ((((exists ff_h_pfp_empty_divisor_productcoefficientsentry. ff_h_pfp_empty_divisor_productcoefficientsentry + S (pfc_value_empty_divisor_productcoefficients) = S ((S (pfc_index_empty_divisor_productcoefficients)) * pfgu_pc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_productcoefficientsentry. pfgu_pb_empty_divisor = ff_q_pfp_empty_divisor_productcoefficientsentry * S ((S (pfc_index_empty_divisor_productcoefficients)) * pfgu_pc_empty_divisor) + (pfc_value_empty_divisor_productcoefficients))) /\ ((exists pfc_terms_code_empty_divisor_productcoefficientscoefficient pfc_terms_scale_empty_divisor_productcoefficientscoefficient pfc_natural_sum_empty_divisor_productcoefficientscoefficient. ((forall pfc_index_empty_divisor_productcoefficientscoefficientdiagonal. (exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonalbound. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonalbound + S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal) = (S (pfc_index_empty_divisor_productcoefficients))) -> exists pfc_value_empty_divisor_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry + S (pfc_value_empty_divisor_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry. pfc_terms_code_empty_divisor_productcoefficientscoefficient = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient) + (pfc_value_empty_divisor_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm. (((pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)+pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm=(pfc_index_empty_divisor_productcoefficients)) /\ ((((((exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal) = (pfgu_Q_empty_divisor)) /\ ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfgu_qc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_empty_divisor = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) * pfgu_qc_empty_divisor) + (pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_empty_divisor)=(pfc_index_empty_divisor_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm) = (0)) /\ ((((exists ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_empty_divisor_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_empty_divisor_productcoefficientscoefficientdiagonaltermrightoutside+(0)=(pfc_complement_empty_divisor_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_empty_divisor_productcoefficientscoefficientdiagonal)=pfc_left_empty_divisor_productcoefficientscoefficientdiagonalterm*pfc_right_empty_divisor_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_empty_divisor_productcoefficientscoefficientsum fs_v_pfc_empty_divisor_productcoefficientscoefficientsum. ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_start. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_start. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_empty_divisor_productcoefficientscoefficient) = S ((S (S (pfc_index_empty_divisor_productcoefficients))) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_empty_divisor_productcoefficients))) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (pfc_natural_sum_empty_divisor_productcoefficientscoefficient))) /\ forall fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps = S (pfc_index_empty_divisor_productcoefficients)) -> exists fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_empty_divisor_productcoefficientscoefficient = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_empty_divisor_productcoefficientscoefficient) + (fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_empty_divisor_productcoefficientscoefficientsum = fs_q_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_empty_divisor_productcoefficientscoefficientsum) + (fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps = fs_r_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps + fs_a_pfc_empty_divisor_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_empty_divisor_productcoefficientscoefficientresiduebound. pfa_gap_empty_divisor_productcoefficientscoefficientresiduebound + S (pfc_value_empty_divisor_productcoefficients) = (p)) /\ ((exists pfa_offset_left_empty_divisor_productcoefficientscoefficientresiduecongruence pfa_offset_right_empty_divisor_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_empty_divisor_productcoefficientscoefficient) + (p) * pfa_offset_left_empty_divisor_productcoefficientscoefficientresiduecongruence = (pfc_value_empty_divisor_productcoefficients) + (p) * pfa_offset_right_empty_divisor_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_empty_divisor_target pfrep_left_empty_divisor_target pfrep_right_empty_divisor_target. ((exists pfrep_position_empty_divisor_targetfirst. ((pfrep_position_empty_divisor_targetfirst+S (pfrep_power_empty_divisor_target)=(pfgu_P_empty_divisor)) /\ ((((exists ff_h_pfp_empty_divisor_targetfirstentry. ff_h_pfp_empty_divisor_targetfirstentry + S (pfrep_left_empty_divisor_target) = S ((S (pfrep_position_empty_divisor_targetfirst)) * pfgu_pc_empty_divisor)) /\ exists ff_q_pfp_empty_divisor_targetfirstentry. pfgu_pb_empty_divisor = ff_q_pfp_empty_divisor_targetfirstentry * S ((S (pfrep_position_empty_divisor_targetfirst)) * pfgu_pc_empty_divisor) + (pfrep_left_empty_divisor_target)))))) \/ (((exists pfrep_gap_empty_divisor_targetfirstoutside. pfrep_gap_empty_divisor_targetfirstoutside+(pfgu_P_empty_divisor)=(pfrep_power_empty_divisor_target)) /\ (((pfrep_left_empty_divisor_target)=0))))) -> ((exists pfrep_position_empty_divisor_targetsecond. ((pfrep_position_empty_divisor_targetsecond+S (pfrep_power_empty_divisor_target)=(L)) /\ ((((exists ff_h_pfp_empty_divisor_targetsecondentry. ff_h_pfp_empty_divisor_targetsecondentry + S (pfrep_right_empty_divisor_target) = S ((S (pfrep_position_empty_divisor_targetsecond)) * ac)) /\ exists ff_q_pfp_empty_divisor_targetsecondentry. ab = ff_q_pfp_empty_divisor_targetsecondentry * S ((S (pfrep_position_empty_divisor_targetsecond)) * ac) + (pfrep_right_empty_divisor_target)))))) \/ (((exists pfrep_gap_empty_divisor_targetsecondoutside. pfrep_gap_empty_divisor_targetsecondoutside+(L)=(pfrep_power_empty_divisor_target)) /\ (((pfrep_right_empty_divisor_target)=0))))) -> pfrep_left_empty_divisor_target=pfrep_right_empty_divisor_target))))))) -> (forall pfrep_power_empty_divisor_result pfrep_left_empty_divisor_result pfrep_right_empty_divisor_result. ((exists pfrep_position_empty_divisor_resultfirst. ((pfrep_position_empty_divisor_resultfirst+S (pfrep_power_empty_divisor_result)=(L)) /\ ((((exists ff_h_pfp_empty_divisor_resultfirstentry. ff_h_pfp_empty_divisor_resultfirstentry + S (pfrep_left_empty_divisor_result) = S ((S (pfrep_position_empty_divisor_resultfirst)) * ac)) /\ exists ff_q_pfp_empty_divisor_resultfirstentry. ab = ff_q_pfp_empty_divisor_resultfirstentry * S ((S (pfrep_position_empty_divisor_resultfirst)) * ac) + (pfrep_left_empty_divisor_result)))))) \/ (((exists pfrep_gap_empty_divisor_resultfirstoutside. pfrep_gap_empty_divisor_resultfirstoutside+(L)=(pfrep_power_empty_divisor_result)) /\ (((pfrep_left_empty_divisor_result)=0))))) -> ((exists pfrep_position_empty_divisor_resultsecond. ((pfrep_position_empty_divisor_resultsecond+S (pfrep_power_empty_divisor_result)=(0)) /\ ((((exists ff_h_pfp_empty_divisor_resultsecondentry. ff_h_pfp_empty_divisor_resultsecondentry + S (pfrep_right_empty_divisor_result) = S ((S (pfrep_position_empty_divisor_resultsecond)) * dc)) /\ exists ff_q_pfp_empty_divisor_resultsecondentry. db = ff_q_pfp_empty_divisor_resultsecondentry * S ((S (pfrep_position_empty_divisor_resultsecond)) * dc) + (pfrep_right_empty_divisor_result)))))) \/ (((exists pfrep_gap_empty_divisor_resultsecondoutside. pfrep_gap_empty_divisor_resultsecondoutside+(0)=(pfrep_power_empty_divisor_result)) /\ (((pfrep_right_empty_divisor_result)=0))))) -> pfrep_left_empty_divisor_result=pfrep_right_empty_divisor_result)