prime_field_polynomial_product_equivalent_nonzero_left_nonempty

Exact expanded first-order arithmetic statement

forall p qb qc Q db dc D pb pc P ab ac L a. ((((L)=S (a)) /\ (((forall fom_index_pfp_nonempty_targetcoefficients. (exists fom_gap_pfp_nonempty_targetcoefficients_index_bound. fom_gap_pfp_nonempty_targetcoefficients_index_bound + S (fom_index_pfp_nonempty_targetcoefficients) = L) -> exists fom_value_pfp_nonempty_targetcoefficients. ((((exists fom_beta_height_pfp_nonempty_targetcoefficients_entry. fom_beta_height_pfp_nonempty_targetcoefficients_entry + S (fom_value_pfp_nonempty_targetcoefficients) = S ((S (fom_index_pfp_nonempty_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_nonempty_targetcoefficients_entry. ab = fom_beta_quotient_pfp_nonempty_targetcoefficients_entry * S ((S (fom_index_pfp_nonempty_targetcoefficients)) * ac) + (fom_value_pfp_nonempty_targetcoefficients))) /\ (exists fom_gap_pfp_nonempty_targetcoefficients_value_bound. fom_gap_pfp_nonempty_targetcoefficients_value_bound + S (fom_value_pfp_nonempty_targetcoefficients) = p))) /\ ((exists pfd_leading_nonempty_target. ((((exists ff_h_pfp_nonempty_targetentry. ff_h_pfp_nonempty_targetentry + S (pfd_leading_nonempty_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_nonempty_targetentry. ab = ff_q_pfp_nonempty_targetentry * S ((S (0)) * ac) + (pfd_leading_nonempty_target))) /\ ((~(pfd_leading_nonempty_target=0)))))))))) -> (((forall fom_index_pfp_nonempty_productleft. (exists fom_gap_pfp_nonempty_productleft_index_bound. fom_gap_pfp_nonempty_productleft_index_bound + S (fom_index_pfp_nonempty_productleft) = Q) -> exists fom_value_pfp_nonempty_productleft. ((((exists fom_beta_height_pfp_nonempty_productleft_entry. fom_beta_height_pfp_nonempty_productleft_entry + S (fom_value_pfp_nonempty_productleft) = S ((S (fom_index_pfp_nonempty_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_nonempty_productleft_entry. qb = fom_beta_quotient_pfp_nonempty_productleft_entry * S ((S (fom_index_pfp_nonempty_productleft)) * qc) + (fom_value_pfp_nonempty_productleft))) /\ (exists fom_gap_pfp_nonempty_productleft_value_bound. fom_gap_pfp_nonempty_productleft_value_bound + S (fom_value_pfp_nonempty_productleft) = p))) /\ (((forall fom_index_pfp_nonempty_productright. (exists fom_gap_pfp_nonempty_productright_index_bound. fom_gap_pfp_nonempty_productright_index_bound + S (fom_index_pfp_nonempty_productright) = D) -> exists fom_value_pfp_nonempty_productright. ((((exists fom_beta_height_pfp_nonempty_productright_entry. fom_beta_height_pfp_nonempty_productright_entry + S (fom_value_pfp_nonempty_productright) = S ((S (fom_index_pfp_nonempty_productright)) * dc)) /\ exists fom_beta_quotient_pfp_nonempty_productright_entry. db = fom_beta_quotient_pfp_nonempty_productright_entry * S ((S (fom_index_pfp_nonempty_productright)) * dc) + (fom_value_pfp_nonempty_productright))) /\ (exists fom_gap_pfp_nonempty_productright_value_bound. fom_gap_pfp_nonempty_productright_value_bound + S (fom_value_pfp_nonempty_productright) = p))) /\ (((((((Q)=0 \/ (D)=0) /\ (((P)=0)))) \/ (((~((Q)=0)) /\ (((~((D)=0)) /\ (((Q)+(D)=S (P)))))))) /\ ((forall pfc_index_nonempty_productcoefficients. (exists pfa_gap_nonempty_productcoefficientsbound. pfa_gap_nonempty_productcoefficientsbound + S (pfc_index_nonempty_productcoefficients) = (P)) -> exists pfc_value_nonempty_productcoefficients. ((((exists ff_h_pfp_nonempty_productcoefficientsentry. ff_h_pfp_nonempty_productcoefficientsentry + S (pfc_value_nonempty_productcoefficients) = S ((S (pfc_index_nonempty_productcoefficients)) * pc)) /\ exists ff_q_pfp_nonempty_productcoefficientsentry. pb = ff_q_pfp_nonempty_productcoefficientsentry * S ((S (pfc_index_nonempty_productcoefficients)) * pc) + (pfc_value_nonempty_productcoefficients))) /\ ((exists pfc_terms_code_nonempty_productcoefficientscoefficient pfc_terms_scale_nonempty_productcoefficientscoefficient pfc_natural_sum_nonempty_productcoefficientscoefficient. ((forall pfc_index_nonempty_productcoefficientscoefficientdiagonal. (exists pfa_gap_nonempty_productcoefficientscoefficientdiagonalbound. pfa_gap_nonempty_productcoefficientscoefficientdiagonalbound + S (pfc_index_nonempty_productcoefficientscoefficientdiagonal) = (S (pfc_index_nonempty_productcoefficients))) -> exists pfc_value_nonempty_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonalentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonalentry + S (pfc_value_nonempty_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_productcoefficientscoefficient)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonalentry. pfc_terms_code_nonempty_productcoefficientscoefficient = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_nonempty_productcoefficientscoefficient) + (pfc_value_nonempty_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm pfc_left_nonempty_productcoefficientscoefficientdiagonalterm pfc_right_nonempty_productcoefficientscoefficientdiagonalterm. (((pfc_index_nonempty_productcoefficientscoefficientdiagonal)+pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm=(pfc_index_nonempty_productcoefficients)) /\ ((((((exists pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_nonempty_productcoefficientscoefficientdiagonal) = (Q)) /\ ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_nonempty_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_nonempty_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_nonempty_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermleftoutside+(Q)=(pfc_index_nonempty_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_nonempty_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_nonempty_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_nonempty_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_nonempty_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_nonempty_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_nonempty_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_nonempty_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_nonempty_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_nonempty_productcoefficientscoefficientdiagonal)=pfc_left_nonempty_productcoefficientscoefficientdiagonalterm*pfc_right_nonempty_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_nonempty_productcoefficientscoefficientsum fs_v_pfc_nonempty_productcoefficientscoefficientsum. ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_start. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_start. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_nonempty_productcoefficientscoefficient) = S ((S (S (pfc_index_nonempty_productcoefficients))) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_nonempty_productcoefficients))) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (pfc_natural_sum_nonempty_productcoefficientscoefficient))) /\ forall fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_nonempty_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_nonempty_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps = S (pfc_index_nonempty_productcoefficients)) -> exists fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_productcoefficientscoefficient)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_nonempty_productcoefficientscoefficient = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_nonempty_productcoefficientscoefficient) + (fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_nonempty_productcoefficientscoefficientsum = fs_q_pfc_nonempty_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_nonempty_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_nonempty_productcoefficientscoefficientsum) + (fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_nonempty_productcoefficientscoefficientsum_body_steps = fs_r_pfc_nonempty_productcoefficientscoefficientsum_body_steps + fs_a_pfc_nonempty_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_nonempty_productcoefficientscoefficientresiduebound. pfa_gap_nonempty_productcoefficientscoefficientresiduebound + S (pfc_value_nonempty_productcoefficients) = (p)) /\ ((exists pfa_offset_left_nonempty_productcoefficientscoefficientresiduecongruence pfa_offset_right_nonempty_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_nonempty_productcoefficientscoefficient) + (p) * pfa_offset_left_nonempty_productcoefficientscoefficientresiduecongruence = (pfc_value_nonempty_productcoefficients) + (p) * pfa_offset_right_nonempty_productcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_nonempty_target_equivalent pfrep_left_nonempty_target_equivalent pfrep_right_nonempty_target_equivalent. ((exists pfrep_position_nonempty_target_equivalentfirst. ((pfrep_position_nonempty_target_equivalentfirst+S (pfrep_power_nonempty_target_equivalent)=(P)) /\ ((((exists ff_h_pfp_nonempty_target_equivalentfirstentry. ff_h_pfp_nonempty_target_equivalentfirstentry + S (pfrep_left_nonempty_target_equivalent) = S ((S (pfrep_position_nonempty_target_equivalentfirst)) * pc)) /\ exists ff_q_pfp_nonempty_target_equivalentfirstentry. pb = ff_q_pfp_nonempty_target_equivalentfirstentry * S ((S (pfrep_position_nonempty_target_equivalentfirst)) * pc) + (pfrep_left_nonempty_target_equivalent)))))) \/ (((exists pfrep_gap_nonempty_target_equivalentfirstoutside. pfrep_gap_nonempty_target_equivalentfirstoutside+(P)=(pfrep_power_nonempty_target_equivalent)) /\ (((pfrep_left_nonempty_target_equivalent)=0))))) -> ((exists pfrep_position_nonempty_target_equivalentsecond. ((pfrep_position_nonempty_target_equivalentsecond+S (pfrep_power_nonempty_target_equivalent)=(L)) /\ ((((exists ff_h_pfp_nonempty_target_equivalentsecondentry. ff_h_pfp_nonempty_target_equivalentsecondentry + S (pfrep_right_nonempty_target_equivalent) = S ((S (pfrep_position_nonempty_target_equivalentsecond)) * ac)) /\ exists ff_q_pfp_nonempty_target_equivalentsecondentry. ab = ff_q_pfp_nonempty_target_equivalentsecondentry * S ((S (pfrep_position_nonempty_target_equivalentsecond)) * ac) + (pfrep_right_nonempty_target_equivalent)))))) \/ (((exists pfrep_gap_nonempty_target_equivalentsecondoutside. pfrep_gap_nonempty_target_equivalentsecondoutside+(L)=(pfrep_power_nonempty_target_equivalent)) /\ (((pfrep_right_nonempty_target_equivalent)=0))))) -> pfrep_left_nonempty_target_equivalent=pfrep_right_nonempty_target_equivalent) -> (~(Q=0))