prime_field_polynomial_monic_normalization_exists_unique

Exact expanded first-order arithmetic statement

forall p ab ac L d. (~((p) = 1) /\ forall pfa_factor_left_normalization_unique_prime pfa_factor_right_normalization_unique_prime. (p) = pfa_factor_left_normalization_unique_prime * pfa_factor_right_normalization_unique_prime -> pfa_factor_left_normalization_unique_prime = 1 \/ pfa_factor_right_normalization_unique_prime = 1) -> ((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_unique_inputcoefficients. (exists fom_gap_pfp_normalization_unique_inputcoefficients_index_bound. fom_gap_pfp_normalization_unique_inputcoefficients_index_bound + S (fom_index_pfp_normalization_unique_inputcoefficients) = L) -> exists fom_value_pfp_normalization_unique_inputcoefficients. ((((exists fom_beta_height_pfp_normalization_unique_inputcoefficients_entry. fom_beta_height_pfp_normalization_unique_inputcoefficients_entry + S (fom_value_pfp_normalization_unique_inputcoefficients) = S ((S (fom_index_pfp_normalization_unique_inputcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_normalization_unique_inputcoefficients_entry. ab = fom_beta_quotient_pfp_normalization_unique_inputcoefficients_entry * S ((S (fom_index_pfp_normalization_unique_inputcoefficients)) * ac) + (fom_value_pfp_normalization_unique_inputcoefficients))) /\ (exists fom_gap_pfp_normalization_unique_inputcoefficients_value_bound. fom_gap_pfp_normalization_unique_inputcoefficients_value_bound + S (fom_value_pfp_normalization_unique_inputcoefficients) = p))) /\ ((exists pfd_leading_normalization_unique_input. ((((exists ff_h_pfp_normalization_unique_inputentry. ff_h_pfp_normalization_unique_inputentry + S (pfd_leading_normalization_unique_input) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_unique_inputentry. ab = ff_q_pfp_normalization_unique_inputentry * S ((S (0)) * ac) + (pfd_leading_normalization_unique_input))) /\ ((~(pfd_leading_normalization_unique_input=0)))))))))) -> exists k bb bc. (((((~((L) = 0)) /\ (((exists pfm_leading_normalization_unique_graph. ((((exists ff_h_pfp_normalization_unique_graphsource. ff_h_pfp_normalization_unique_graphsource + S (pfm_leading_normalization_unique_graph) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_unique_graphsource. ab = ff_q_pfp_normalization_unique_graphsource * S ((S (0)) * ac) + (pfm_leading_normalization_unique_graph))) /\ ((((~((pfm_leading_normalization_unique_graph) = 0)) /\ ((((exists pfa_gap_normalization_unique_graphinversemultiplicationleft. pfa_gap_normalization_unique_graphinversemultiplicationleft + S (pfm_leading_normalization_unique_graph) = (p)) /\ (((exists pfa_gap_normalization_unique_graphinversemultiplicationright. pfa_gap_normalization_unique_graphinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_unique_graphinversemultiplicationresultbound. pfa_gap_normalization_unique_graphinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_unique_graphinversemultiplicationresultcongruence pfa_offset_right_normalization_unique_graphinversemultiplicationresultcongruence. ((pfm_leading_normalization_unique_graph) * (k)) + (p) * pfa_offset_left_normalization_unique_graphinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_unique_graphinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_unique_graphscalescalar. pfa_gap_normalization_unique_graphscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_unique_graphscale. (exists pfa_gap_normalization_unique_graphscaleindex. pfa_gap_normalization_unique_graphscaleindex + S (pfp_index_normalization_unique_graphscale) = (L)) -> exists pfp_source_normalization_unique_graphscale pfp_value_normalization_unique_graphscale. ((((exists ff_h_pfp_normalization_unique_graphscalesource. ff_h_pfp_normalization_unique_graphscalesource + S (pfp_source_normalization_unique_graphscale) = S ((S (pfp_index_normalization_unique_graphscale)) * ac)) /\ exists ff_q_pfp_normalization_unique_graphscalesource. ab = ff_q_pfp_normalization_unique_graphscalesource * S ((S (pfp_index_normalization_unique_graphscale)) * ac) + (pfp_source_normalization_unique_graphscale))) /\ (((((exists ff_h_pfp_normalization_unique_graphscaletarget. ff_h_pfp_normalization_unique_graphscaletarget + S (pfp_value_normalization_unique_graphscale) = S ((S (pfp_index_normalization_unique_graphscale)) * bc)) /\ exists ff_q_pfp_normalization_unique_graphscaletarget. bb = ff_q_pfp_normalization_unique_graphscaletarget * S ((S (pfp_index_normalization_unique_graphscale)) * bc) + (pfp_value_normalization_unique_graphscale))) /\ ((((exists pfa_gap_normalization_unique_graphscaleoperationleft. pfa_gap_normalization_unique_graphscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_unique_graphscaleoperationright. pfa_gap_normalization_unique_graphscaleoperationright + S (pfp_source_normalization_unique_graphscale) = (p)) /\ ((((exists pfa_gap_normalization_unique_graphscaleoperationresultbound. pfa_gap_normalization_unique_graphscaleoperationresultbound + S (pfp_value_normalization_unique_graphscale) = (p)) /\ ((exists pfa_offset_left_normalization_unique_graphscaleoperationresultcongruence pfa_offset_right_normalization_unique_graphscaleoperationresultcongruence. ((k) * (pfp_source_normalization_unique_graphscale)) + (p) * pfa_offset_left_normalization_unique_graphscaleoperationresultcongruence = (pfp_value_normalization_unique_graphscale) + (p) * pfa_offset_right_normalization_unique_graphscaleoperationresultcongruence)))))))))))))))))))))) /\ (((((~((L) = 0)) /\ (((forall fom_index_pfp_normalization_unique_moniccoefficients. (exists fom_gap_pfp_normalization_unique_moniccoefficients_index_bound. fom_gap_pfp_normalization_unique_moniccoefficients_index_bound + S (fom_index_pfp_normalization_unique_moniccoefficients) = L) -> exists fom_value_pfp_normalization_unique_moniccoefficients. ((((exists fom_beta_height_pfp_normalization_unique_moniccoefficients_entry. fom_beta_height_pfp_normalization_unique_moniccoefficients_entry + S (fom_value_pfp_normalization_unique_moniccoefficients) = S ((S (fom_index_pfp_normalization_unique_moniccoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_unique_moniccoefficients_entry. bb = fom_beta_quotient_pfp_normalization_unique_moniccoefficients_entry * S ((S (fom_index_pfp_normalization_unique_moniccoefficients)) * bc) + (fom_value_pfp_normalization_unique_moniccoefficients))) /\ (exists fom_gap_pfp_normalization_unique_moniccoefficients_value_bound. fom_gap_pfp_normalization_unique_moniccoefficients_value_bound + S (fom_value_pfp_normalization_unique_moniccoefficients) = p))) /\ ((((exists ff_h_pfp_normalization_unique_monicleading. ff_h_pfp_normalization_unique_monicleading + S (1) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_unique_monicleading. bb = ff_q_pfp_normalization_unique_monicleading * S ((S (0)) * bc) + (1)))))))) /\ ((((((L)=S (d)) /\ (((forall fom_index_pfp_normalization_unique_degreecoefficients. (exists fom_gap_pfp_normalization_unique_degreecoefficients_index_bound. fom_gap_pfp_normalization_unique_degreecoefficients_index_bound + S (fom_index_pfp_normalization_unique_degreecoefficients) = L) -> exists fom_value_pfp_normalization_unique_degreecoefficients. ((((exists fom_beta_height_pfp_normalization_unique_degreecoefficients_entry. fom_beta_height_pfp_normalization_unique_degreecoefficients_entry + S (fom_value_pfp_normalization_unique_degreecoefficients) = S ((S (fom_index_pfp_normalization_unique_degreecoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_normalization_unique_degreecoefficients_entry. bb = fom_beta_quotient_pfp_normalization_unique_degreecoefficients_entry * S ((S (fom_index_pfp_normalization_unique_degreecoefficients)) * bc) + (fom_value_pfp_normalization_unique_degreecoefficients))) /\ (exists fom_gap_pfp_normalization_unique_degreecoefficients_value_bound. fom_gap_pfp_normalization_unique_degreecoefficients_value_bound + S (fom_value_pfp_normalization_unique_degreecoefficients) = p))) /\ ((exists pfd_leading_normalization_unique_degree. ((((exists ff_h_pfp_normalization_unique_degreeentry. ff_h_pfp_normalization_unique_degreeentry + S (pfd_leading_normalization_unique_degree) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_unique_degreeentry. bb = ff_q_pfp_normalization_unique_degreeentry * S ((S (0)) * bc) + (pfd_leading_normalization_unique_degree))) /\ ((~(pfd_leading_normalization_unique_degree=0)))))))))) /\ ((forall j cb cc. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_uniquecomparison. ((((exists ff_h_pfp_normalization_uniquecomparisonsource. ff_h_pfp_normalization_uniquecomparisonsource + S (pfm_leading_normalization_uniquecomparison) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_uniquecomparisonsource. ab = ff_q_pfp_normalization_uniquecomparisonsource * S ((S (0)) * ac) + (pfm_leading_normalization_uniquecomparison))) /\ ((((~((pfm_leading_normalization_uniquecomparison) = 0)) /\ ((((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationleft. pfa_gap_normalization_uniquecomparisoninversemultiplicationleft + S (pfm_leading_normalization_uniquecomparison) = (p)) /\ (((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationright. pfa_gap_normalization_uniquecomparisoninversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_uniquecomparisoninversemultiplicationresultbound. pfa_gap_normalization_uniquecomparisoninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_uniquecomparisoninversemultiplicationresultcongruence pfa_offset_right_normalization_uniquecomparisoninversemultiplicationresultcongruence. ((pfm_leading_normalization_uniquecomparison) * (j)) + (p) * pfa_offset_left_normalization_uniquecomparisoninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_uniquecomparisoninversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_uniquecomparisonscalescalar. pfa_gap_normalization_uniquecomparisonscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_uniquecomparisonscale. (exists pfa_gap_normalization_uniquecomparisonscaleindex. pfa_gap_normalization_uniquecomparisonscaleindex + S (pfp_index_normalization_uniquecomparisonscale) = (L)) -> exists pfp_source_normalization_uniquecomparisonscale pfp_value_normalization_uniquecomparisonscale. ((((exists ff_h_pfp_normalization_uniquecomparisonscalesource. ff_h_pfp_normalization_uniquecomparisonscalesource + S (pfp_source_normalization_uniquecomparisonscale) = S ((S (pfp_index_normalization_uniquecomparisonscale)) * ac)) /\ exists ff_q_pfp_normalization_uniquecomparisonscalesource. ab = ff_q_pfp_normalization_uniquecomparisonscalesource * S ((S (pfp_index_normalization_uniquecomparisonscale)) * ac) + (pfp_source_normalization_uniquecomparisonscale))) /\ (((((exists ff_h_pfp_normalization_uniquecomparisonscaletarget. ff_h_pfp_normalization_uniquecomparisonscaletarget + S (pfp_value_normalization_uniquecomparisonscale) = S ((S (pfp_index_normalization_uniquecomparisonscale)) * cc)) /\ exists ff_q_pfp_normalization_uniquecomparisonscaletarget. cb = ff_q_pfp_normalization_uniquecomparisonscaletarget * S ((S (pfp_index_normalization_uniquecomparisonscale)) * cc) + (pfp_value_normalization_uniquecomparisonscale))) /\ ((((exists pfa_gap_normalization_uniquecomparisonscaleoperationleft. pfa_gap_normalization_uniquecomparisonscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_uniquecomparisonscaleoperationright. pfa_gap_normalization_uniquecomparisonscaleoperationright + S (pfp_source_normalization_uniquecomparisonscale) = (p)) /\ ((((exists pfa_gap_normalization_uniquecomparisonscaleoperationresultbound. pfa_gap_normalization_uniquecomparisonscaleoperationresultbound + S (pfp_value_normalization_uniquecomparisonscale) = (p)) /\ ((exists pfa_offset_left_normalization_uniquecomparisonscaleoperationresultcongruence pfa_offset_right_normalization_uniquecomparisonscaleoperationresultcongruence. ((j) * (pfp_source_normalization_uniquecomparisonscale)) + (p) * pfa_offset_left_normalization_uniquecomparisonscaleoperationresultcongruence = (pfp_value_normalization_uniquecomparisonscale) + (p) * pfa_offset_right_normalization_uniquecomparisonscaleoperationresultcongruence)))))))))))))))))))))) -> ((j=(k)) /\ ((forall mdr_i_pfp_normalization_uniqueequal mdr_a_pfp_normalization_uniqueequal. (exists mdr_gap_pfp_normalization_uniqueequalb. mdr_gap_pfp_normalization_uniqueequalb + S (mdr_i_pfp_normalization_uniqueequal) = (L)) -> (((exists ff_h_mdr_pfp_normalization_uniqueequalo. ff_h_mdr_pfp_normalization_uniqueequalo + S (mdr_a_pfp_normalization_uniqueequal) = S ((S (mdr_i_pfp_normalization_uniqueequal)) * cc)) /\ exists ff_q_mdr_pfp_normalization_uniqueequalo. cb = ff_q_mdr_pfp_normalization_uniqueequalo * S ((S (mdr_i_pfp_normalization_uniqueequal)) * cc) + (mdr_a_pfp_normalization_uniqueequal))) -> (((exists ff_h_mdr_pfp_normalization_uniqueequaln. ff_h_mdr_pfp_normalization_uniqueequaln + S (mdr_a_pfp_normalization_uniqueequal) = S ((S (mdr_i_pfp_normalization_uniqueequal)) * bc)) /\ exists ff_q_mdr_pfp_normalization_uniqueequaln. bb = ff_q_mdr_pfp_normalization_uniqueequaln * S ((S (mdr_i_pfp_normalization_uniqueequal)) * bc) + (mdr_a_pfp_normalization_uniqueequal))))))))))))))