prime_field_polynomial_right_divides_divisor_bounded

Exact expanded first-order arithmetic statement

forall p db dc D ab ac L. (((forall fom_index_pfp_right_divisor_bound_source_canonical. (exists fom_gap_pfp_right_divisor_bound_source_canonical_index_bound. fom_gap_pfp_right_divisor_bound_source_canonical_index_bound + S (fom_index_pfp_right_divisor_bound_source_canonical) = L) -> exists fom_value_pfp_right_divisor_bound_source_canonical. ((((exists fom_beta_height_pfp_right_divisor_bound_source_canonical_entry. fom_beta_height_pfp_right_divisor_bound_source_canonical_entry + S (fom_value_pfp_right_divisor_bound_source_canonical) = S ((S (fom_index_pfp_right_divisor_bound_source_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_divisor_bound_source_canonical_entry. ab = fom_beta_quotient_pfp_right_divisor_bound_source_canonical_entry * S ((S (fom_index_pfp_right_divisor_bound_source_canonical)) * ac) + (fom_value_pfp_right_divisor_bound_source_canonical))) /\ (exists fom_gap_pfp_right_divisor_bound_source_canonical_value_bound. fom_gap_pfp_right_divisor_bound_source_canonical_value_bound + S (fom_value_pfp_right_divisor_bound_source_canonical) = p))) /\ ((exists pfrd_qb_right_divisor_bound_source pfrd_qc_right_divisor_bound_source pfrd_qlen_right_divisor_bound_source pfrd_pb_right_divisor_bound_source pfrd_pc_right_divisor_bound_source pfrd_plen_right_divisor_bound_source. ((((forall fom_index_pfp_right_divisor_bound_source_productleft. (exists fom_gap_pfp_right_divisor_bound_source_productleft_index_bound. fom_gap_pfp_right_divisor_bound_source_productleft_index_bound + S (fom_index_pfp_right_divisor_bound_source_productleft) = pfrd_qlen_right_divisor_bound_source) -> exists fom_value_pfp_right_divisor_bound_source_productleft. ((((exists fom_beta_height_pfp_right_divisor_bound_source_productleft_entry. fom_beta_height_pfp_right_divisor_bound_source_productleft_entry + S (fom_value_pfp_right_divisor_bound_source_productleft) = S ((S (fom_index_pfp_right_divisor_bound_source_productleft)) * pfrd_qc_right_divisor_bound_source)) /\ exists fom_beta_quotient_pfp_right_divisor_bound_source_productleft_entry. pfrd_qb_right_divisor_bound_source = fom_beta_quotient_pfp_right_divisor_bound_source_productleft_entry * S ((S (fom_index_pfp_right_divisor_bound_source_productleft)) * pfrd_qc_right_divisor_bound_source) + (fom_value_pfp_right_divisor_bound_source_productleft))) /\ (exists fom_gap_pfp_right_divisor_bound_source_productleft_value_bound. fom_gap_pfp_right_divisor_bound_source_productleft_value_bound + S (fom_value_pfp_right_divisor_bound_source_productleft) = p))) /\ (((forall fom_index_pfp_right_divisor_bound_source_productright. (exists fom_gap_pfp_right_divisor_bound_source_productright_index_bound. fom_gap_pfp_right_divisor_bound_source_productright_index_bound + S (fom_index_pfp_right_divisor_bound_source_productright) = D) -> exists fom_value_pfp_right_divisor_bound_source_productright. ((((exists fom_beta_height_pfp_right_divisor_bound_source_productright_entry. fom_beta_height_pfp_right_divisor_bound_source_productright_entry + S (fom_value_pfp_right_divisor_bound_source_productright) = S ((S (fom_index_pfp_right_divisor_bound_source_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_divisor_bound_source_productright_entry. db = fom_beta_quotient_pfp_right_divisor_bound_source_productright_entry * S ((S (fom_index_pfp_right_divisor_bound_source_productright)) * dc) + (fom_value_pfp_right_divisor_bound_source_productright))) /\ (exists fom_gap_pfp_right_divisor_bound_source_productright_value_bound. fom_gap_pfp_right_divisor_bound_source_productright_value_bound + S (fom_value_pfp_right_divisor_bound_source_productright) = p))) /\ (((((((pfrd_qlen_right_divisor_bound_source)=0 \/ (D)=0) /\ (((pfrd_plen_right_divisor_bound_source)=0)))) \/ (((~((pfrd_qlen_right_divisor_bound_source)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_divisor_bound_source)+(D)=S (pfrd_plen_right_divisor_bound_source)))))))) /\ ((forall pfc_index_right_divisor_bound_source_productcoefficients. (exists pfa_gap_right_divisor_bound_source_productcoefficientsbound. pfa_gap_right_divisor_bound_source_productcoefficientsbound + S (pfc_index_right_divisor_bound_source_productcoefficients) = (pfrd_plen_right_divisor_bound_source)) -> exists pfc_value_right_divisor_bound_source_productcoefficients. ((((exists ff_h_pfp_right_divisor_bound_source_productcoefficientsentry. ff_h_pfp_right_divisor_bound_source_productcoefficientsentry + S (pfc_value_right_divisor_bound_source_productcoefficients) = S ((S (pfc_index_right_divisor_bound_source_productcoefficients)) * pfrd_pc_right_divisor_bound_source)) /\ exists ff_q_pfp_right_divisor_bound_source_productcoefficientsentry. pfrd_pb_right_divisor_bound_source = ff_q_pfp_right_divisor_bound_source_productcoefficientsentry * S ((S (pfc_index_right_divisor_bound_source_productcoefficients)) * pfrd_pc_right_divisor_bound_source) + (pfc_value_right_divisor_bound_source_productcoefficients))) /\ ((exists pfc_terms_code_right_divisor_bound_source_productcoefficientscoefficient pfc_terms_scale_right_divisor_bound_source_productcoefficientscoefficient pfc_natural_sum_right_divisor_bound_source_productcoefficientscoefficient. ((forall pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonalbound. pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_divisor_bound_source_productcoefficients))) -> exists pfc_value_right_divisor_bound_source_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_divisor_bound_source_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_bound_source_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_divisor_bound_source_productcoefficientscoefficient = ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_bound_source_productcoefficientscoefficient) + (pfc_value_right_divisor_bound_source_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm pfc_left_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm pfc_right_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)+pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm=(pfc_index_right_divisor_bound_source_productcoefficients)) /\ ((((((exists pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_divisor_bound_source)) /\ ((((exists ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_bound_source)) /\ exists ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_divisor_bound_source = ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_bound_source) + (pfc_left_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_divisor_bound_source)=(pfc_index_right_divisor_bound_source_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_divisor_bound_source_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_divisor_bound_source_productcoefficientscoefficientdiagonal)=pfc_left_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm*pfc_right_right_divisor_bound_source_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_divisor_bound_source_productcoefficientscoefficientsum fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_divisor_bound_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_divisor_bound_source_productcoefficientscoefficient) = S ((S (S (pfc_index_right_divisor_bound_source_productcoefficients))) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_divisor_bound_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_divisor_bound_source_productcoefficients))) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum) + (pfc_natural_sum_right_divisor_bound_source_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_divisor_bound_source_productcoefficients)) -> exists fs_a_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_bound_source_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_divisor_bound_source_productcoefficientscoefficient = fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_bound_source_productcoefficientscoefficient) + (fs_a_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_divisor_bound_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum) + (fs_r_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_divisor_bound_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_bound_source_productcoefficientscoefficientsum) + (fs_s_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_divisor_bound_source_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_divisor_bound_source_productcoefficientscoefficientresiduebound. pfa_gap_right_divisor_bound_source_productcoefficientscoefficientresiduebound + S (pfc_value_right_divisor_bound_source_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_divisor_bound_source_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_divisor_bound_source_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_divisor_bound_source_productcoefficientscoefficient) + (p) * pfa_offset_left_right_divisor_bound_source_productcoefficientscoefficientresiduecongruence = (pfc_value_right_divisor_bound_source_productcoefficients) + (p) * pfa_offset_right_right_divisor_bound_source_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_divisor_bound_source_target pfrep_left_right_divisor_bound_source_target pfrep_right_right_divisor_bound_source_target. ((exists pfrep_position_right_divisor_bound_source_targetfirst. ((pfrep_position_right_divisor_bound_source_targetfirst+S (pfrep_power_right_divisor_bound_source_target)=(pfrd_plen_right_divisor_bound_source)) /\ ((((exists ff_h_pfp_right_divisor_bound_source_targetfirstentry. ff_h_pfp_right_divisor_bound_source_targetfirstentry + S (pfrep_left_right_divisor_bound_source_target) = S ((S (pfrep_position_right_divisor_bound_source_targetfirst)) * pfrd_pc_right_divisor_bound_source)) /\ exists ff_q_pfp_right_divisor_bound_source_targetfirstentry. pfrd_pb_right_divisor_bound_source = ff_q_pfp_right_divisor_bound_source_targetfirstentry * S ((S (pfrep_position_right_divisor_bound_source_targetfirst)) * pfrd_pc_right_divisor_bound_source) + (pfrep_left_right_divisor_bound_source_target)))))) \/ (((exists pfrep_gap_right_divisor_bound_source_targetfirstoutside. pfrep_gap_right_divisor_bound_source_targetfirstoutside+(pfrd_plen_right_divisor_bound_source)=(pfrep_power_right_divisor_bound_source_target)) /\ (((pfrep_left_right_divisor_bound_source_target)=0))))) -> ((exists pfrep_position_right_divisor_bound_source_targetsecond. ((pfrep_position_right_divisor_bound_source_targetsecond+S (pfrep_power_right_divisor_bound_source_target)=(L)) /\ ((((exists ff_h_pfp_right_divisor_bound_source_targetsecondentry. ff_h_pfp_right_divisor_bound_source_targetsecondentry + S (pfrep_right_right_divisor_bound_source_target) = S ((S (pfrep_position_right_divisor_bound_source_targetsecond)) * ac)) /\ exists ff_q_pfp_right_divisor_bound_source_targetsecondentry. ab = ff_q_pfp_right_divisor_bound_source_targetsecondentry * S ((S (pfrep_position_right_divisor_bound_source_targetsecond)) * ac) + (pfrep_right_right_divisor_bound_source_target)))))) \/ (((exists pfrep_gap_right_divisor_bound_source_targetsecondoutside. pfrep_gap_right_divisor_bound_source_targetsecondoutside+(L)=(pfrep_power_right_divisor_bound_source_target)) /\ (((pfrep_right_right_divisor_bound_source_target)=0))))) -> pfrep_left_right_divisor_bound_source_target=pfrep_right_right_divisor_bound_source_target))))))) -> (forall fom_index_pfp_right_divisor_bound_result. (exists fom_gap_pfp_right_divisor_bound_result_index_bound. fom_gap_pfp_right_divisor_bound_result_index_bound + S (fom_index_pfp_right_divisor_bound_result) = D) -> exists fom_value_pfp_right_divisor_bound_result. ((((exists fom_beta_height_pfp_right_divisor_bound_result_entry. fom_beta_height_pfp_right_divisor_bound_result_entry + S (fom_value_pfp_right_divisor_bound_result) = S ((S (fom_index_pfp_right_divisor_bound_result)) * dc)) /\ exists fom_beta_quotient_pfp_right_divisor_bound_result_entry. db = fom_beta_quotient_pfp_right_divisor_bound_result_entry * S ((S (fom_index_pfp_right_divisor_bound_result)) * dc) + (fom_value_pfp_right_divisor_bound_result))) /\ (exists fom_gap_pfp_right_divisor_bound_result_value_bound. fom_gap_pfp_right_divisor_bound_result_value_bound + S (fom_value_pfp_right_divisor_bound_result) = p)))