dirichlet_convolution_entry_from_quotient

Exact expanded first-order arithmetic statement

forall F G n d q a b z. ~(d=0) -> n=d*q -> (exists dst_positive_code_keep_left dst_positive_scale_keep_left dst_negative_code_keep_left dst_negative_scale_keep_left dst_positive_keep_left dst_negative_keep_left. (((F) = (((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) * S ((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) + ((((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))))) /\ (((((exists ff_h_pvs_keep_leftpositive. ff_h_pvs_keep_leftpositive + S (dst_positive_keep_left) = S ((S (d)) * dst_positive_scale_keep_left)) /\ exists ff_q_pvs_keep_leftpositive. dst_positive_code_keep_left = ff_q_pvs_keep_leftpositive * S ((S (d)) * dst_positive_scale_keep_left) + (dst_positive_keep_left))) /\ (((((exists ff_h_pvs_keep_leftnegative. ff_h_pvs_keep_leftnegative + S (dst_negative_keep_left) = S ((S (d)) * dst_negative_scale_keep_left)) /\ exists ff_q_pvs_keep_leftnegative. dst_negative_code_keep_left = ff_q_pvs_keep_leftnegative * S ((S (d)) * dst_negative_scale_keep_left) + (dst_negative_keep_left))) /\ (exists ge_balance_positive_keep_leftvalue ge_balance_negative_keep_leftvalue. (((((a) = 2 * (ge_balance_positive_keep_leftvalue) /\ (ge_balance_negative_keep_leftvalue) = 0) \/ exists ge_signed_half_keep_leftvaluedecode. (((a) = 2 * ge_signed_half_keep_leftvaluedecode + 1 /\ (ge_balance_positive_keep_leftvalue) = 0) /\ (ge_balance_negative_keep_leftvalue) = S ge_signed_half_keep_leftvaluedecode))) /\ ((dst_positive_keep_left) + ge_balance_negative_keep_leftvalue = (dst_negative_keep_left) + ge_balance_positive_keep_leftvalue))))))))) -> (exists dst_positive_code_keep_right dst_positive_scale_keep_right dst_negative_code_keep_right dst_negative_scale_keep_right dst_positive_keep_right dst_negative_keep_right. (((G) = (((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) * S ((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) + ((((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))))) /\ (((((exists ff_h_pvs_keep_rightpositive. ff_h_pvs_keep_rightpositive + S (dst_positive_keep_right) = S ((S (q)) * dst_positive_scale_keep_right)) /\ exists ff_q_pvs_keep_rightpositive. dst_positive_code_keep_right = ff_q_pvs_keep_rightpositive * S ((S (q)) * dst_positive_scale_keep_right) + (dst_positive_keep_right))) /\ (((((exists ff_h_pvs_keep_rightnegative. ff_h_pvs_keep_rightnegative + S (dst_negative_keep_right) = S ((S (q)) * dst_negative_scale_keep_right)) /\ exists ff_q_pvs_keep_rightnegative. dst_negative_code_keep_right = ff_q_pvs_keep_rightnegative * S ((S (q)) * dst_negative_scale_keep_right) + (dst_negative_keep_right))) /\ (exists ge_balance_positive_keep_rightvalue ge_balance_negative_keep_rightvalue. (((((b) = 2 * (ge_balance_positive_keep_rightvalue) /\ (ge_balance_negative_keep_rightvalue) = 0) \/ exists ge_signed_half_keep_rightvaluedecode. (((b) = 2 * ge_signed_half_keep_rightvaluedecode + 1 /\ (ge_balance_positive_keep_rightvalue) = 0) /\ (ge_balance_negative_keep_rightvalue) = S ge_signed_half_keep_rightvaluedecode))) /\ ((dst_positive_keep_right) + ge_balance_negative_keep_rightvalue = (dst_negative_keep_right) + ge_balance_positive_keep_rightvalue))))))))) -> (exists sto_ap_keep_product sto_an_keep_product sto_bp_keep_product sto_bn_keep_product sto_cp_keep_product sto_cn_keep_product. (((((a) = 2 * (sto_ap_keep_product) /\ (sto_an_keep_product) = 0) \/ exists ge_signed_half_keep_productleft. (((a) = 2 * ge_signed_half_keep_productleft + 1 /\ (sto_ap_keep_product) = 0) /\ (sto_an_keep_product) = S ge_signed_half_keep_productleft))) /\ ((((((b) = 2 * (sto_bp_keep_product) /\ (sto_bn_keep_product) = 0) \/ exists ge_signed_half_keep_productright. (((b) = 2 * ge_signed_half_keep_productright + 1 /\ (sto_bp_keep_product) = 0) /\ (sto_bn_keep_product) = S ge_signed_half_keep_productright))) /\ ((((((z) = 2 * (sto_cp_keep_product) /\ (sto_cn_keep_product) = 0) \/ exists ge_signed_half_keep_productoutput. (((z) = 2 * ge_signed_half_keep_productoutput + 1 /\ (sto_cp_keep_product) = 0) /\ (sto_cn_keep_product) = S ge_signed_half_keep_productoutput))) /\ ((sto_ap_keep_product * sto_bp_keep_product + sto_an_keep_product * sto_bn_keep_product) + sto_cn_keep_product = (sto_ap_keep_product * sto_bn_keep_product + sto_an_keep_product * sto_bp_keep_product) + sto_cp_keep_product))))))) -> ((((~((d)=0)) /\ (exists dc_quotient_keep_result dc_left_keep_result dc_right_keep_result. (((n)=(d)*dc_quotient_keep_result) /\ (((exists dst_positive_code_keep_resultleft dst_positive_scale_keep_resultleft dst_negative_code_keep_resultleft dst_negative_scale_keep_resultleft dst_positive_keep_resultleft dst_negative_keep_resultleft. (((F) = (((((dst_positive_code_keep_resultleft) + (dst_positive_scale_keep_resultleft)) * S ((dst_positive_code_keep_resultleft) + (dst_positive_scale_keep_resultleft)) + ((dst_positive_scale_keep_resultleft) + (dst_positive_scale_keep_resultleft))) + (((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) * S ((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) + ((dst_negative_scale_keep_resultleft) + (dst_negative_scale_keep_resultleft)))) * S ((((dst_positive_code_keep_resultleft) + (dst_positive_scale_keep_resultleft)) * S ((dst_positive_code_keep_resultleft) + (dst_positive_scale_keep_resultleft)) + ((dst_positive_scale_keep_resultleft) + (dst_positive_scale_keep_resultleft))) + (((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) * S ((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) + ((dst_negative_scale_keep_resultleft) + (dst_negative_scale_keep_resultleft)))) + ((((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) * S ((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) + ((dst_negative_scale_keep_resultleft) + (dst_negative_scale_keep_resultleft))) + (((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) * S ((dst_negative_code_keep_resultleft) + (dst_negative_scale_keep_resultleft)) + ((dst_negative_scale_keep_resultleft) + (dst_negative_scale_keep_resultleft)))))) /\ (((((exists ff_h_pvs_keep_resultleftpositive. ff_h_pvs_keep_resultleftpositive + S (dst_positive_keep_resultleft) = S ((S (d)) * dst_positive_scale_keep_resultleft)) /\ exists ff_q_pvs_keep_resultleftpositive. dst_positive_code_keep_resultleft = ff_q_pvs_keep_resultleftpositive * S ((S (d)) * dst_positive_scale_keep_resultleft) + (dst_positive_keep_resultleft))) /\ (((((exists ff_h_pvs_keep_resultleftnegative. ff_h_pvs_keep_resultleftnegative + S (dst_negative_keep_resultleft) = S ((S (d)) * dst_negative_scale_keep_resultleft)) /\ exists ff_q_pvs_keep_resultleftnegative. dst_negative_code_keep_resultleft = ff_q_pvs_keep_resultleftnegative * S ((S (d)) * dst_negative_scale_keep_resultleft) + (dst_negative_keep_resultleft))) /\ (exists ge_balance_positive_keep_resultleftvalue ge_balance_negative_keep_resultleftvalue. (((((dc_left_keep_result) = 2 * (ge_balance_positive_keep_resultleftvalue) /\ (ge_balance_negative_keep_resultleftvalue) = 0) \/ exists ge_signed_half_keep_resultleftvaluedecode. (((dc_left_keep_result) = 2 * ge_signed_half_keep_resultleftvaluedecode + 1 /\ (ge_balance_positive_keep_resultleftvalue) = 0) /\ (ge_balance_negative_keep_resultleftvalue) = S ge_signed_half_keep_resultleftvaluedecode))) /\ ((dst_positive_keep_resultleft) + ge_balance_negative_keep_resultleftvalue = (dst_negative_keep_resultleft) + ge_balance_positive_keep_resultleftvalue))))))))) /\ (((exists dst_positive_code_keep_resultright dst_positive_scale_keep_resultright dst_negative_code_keep_resultright dst_negative_scale_keep_resultright dst_positive_keep_resultright dst_negative_keep_resultright. (((G) = (((((dst_positive_code_keep_resultright) + (dst_positive_scale_keep_resultright)) * S ((dst_positive_code_keep_resultright) + (dst_positive_scale_keep_resultright)) + ((dst_positive_scale_keep_resultright) + (dst_positive_scale_keep_resultright))) + (((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) * S ((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) + ((dst_negative_scale_keep_resultright) + (dst_negative_scale_keep_resultright)))) * S ((((dst_positive_code_keep_resultright) + (dst_positive_scale_keep_resultright)) * S ((dst_positive_code_keep_resultright) + (dst_positive_scale_keep_resultright)) + ((dst_positive_scale_keep_resultright) + (dst_positive_scale_keep_resultright))) + (((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) * S ((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) + ((dst_negative_scale_keep_resultright) + (dst_negative_scale_keep_resultright)))) + ((((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) * S ((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) + ((dst_negative_scale_keep_resultright) + (dst_negative_scale_keep_resultright))) + (((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) * S ((dst_negative_code_keep_resultright) + (dst_negative_scale_keep_resultright)) + ((dst_negative_scale_keep_resultright) + (dst_negative_scale_keep_resultright)))))) /\ (((((exists ff_h_pvs_keep_resultrightpositive. ff_h_pvs_keep_resultrightpositive + S (dst_positive_keep_resultright) = S ((S (dc_quotient_keep_result)) * dst_positive_scale_keep_resultright)) /\ exists ff_q_pvs_keep_resultrightpositive. dst_positive_code_keep_resultright = ff_q_pvs_keep_resultrightpositive * S ((S (dc_quotient_keep_result)) * dst_positive_scale_keep_resultright) + (dst_positive_keep_resultright))) /\ (((((exists ff_h_pvs_keep_resultrightnegative. ff_h_pvs_keep_resultrightnegative + S (dst_negative_keep_resultright) = S ((S (dc_quotient_keep_result)) * dst_negative_scale_keep_resultright)) /\ exists ff_q_pvs_keep_resultrightnegative. dst_negative_code_keep_resultright = ff_q_pvs_keep_resultrightnegative * S ((S (dc_quotient_keep_result)) * dst_negative_scale_keep_resultright) + (dst_negative_keep_resultright))) /\ (exists ge_balance_positive_keep_resultrightvalue ge_balance_negative_keep_resultrightvalue. (((((dc_right_keep_result) = 2 * (ge_balance_positive_keep_resultrightvalue) /\ (ge_balance_negative_keep_resultrightvalue) = 0) \/ exists ge_signed_half_keep_resultrightvaluedecode. (((dc_right_keep_result) = 2 * ge_signed_half_keep_resultrightvaluedecode + 1 /\ (ge_balance_positive_keep_resultrightvalue) = 0) /\ (ge_balance_negative_keep_resultrightvalue) = S ge_signed_half_keep_resultrightvaluedecode))) /\ ((dst_positive_keep_resultright) + ge_balance_negative_keep_resultrightvalue = (dst_negative_keep_resultright) + ge_balance_positive_keep_resultrightvalue))))))))) /\ (exists sto_ap_keep_resultproduct sto_an_keep_resultproduct sto_bp_keep_resultproduct sto_bn_keep_resultproduct sto_cp_keep_resultproduct sto_cn_keep_resultproduct. (((((dc_left_keep_result) = 2 * (sto_ap_keep_resultproduct) /\ (sto_an_keep_resultproduct) = 0) \/ exists ge_signed_half_keep_resultproductleft. (((dc_left_keep_result) = 2 * ge_signed_half_keep_resultproductleft + 1 /\ (sto_ap_keep_resultproduct) = 0) /\ (sto_an_keep_resultproduct) = S ge_signed_half_keep_resultproductleft))) /\ ((((((dc_right_keep_result) = 2 * (sto_bp_keep_resultproduct) /\ (sto_bn_keep_resultproduct) = 0) \/ exists ge_signed_half_keep_resultproductright. (((dc_right_keep_result) = 2 * ge_signed_half_keep_resultproductright + 1 /\ (sto_bp_keep_resultproduct) = 0) /\ (sto_bn_keep_resultproduct) = S ge_signed_half_keep_resultproductright))) /\ ((((((z) = 2 * (sto_cp_keep_resultproduct) /\ (sto_cn_keep_resultproduct) = 0) \/ exists ge_signed_half_keep_resultproductoutput. (((z) = 2 * ge_signed_half_keep_resultproductoutput + 1 /\ (sto_cp_keep_resultproduct) = 0) /\ (sto_cn_keep_resultproduct) = S ge_signed_half_keep_resultproductoutput))) /\ ((sto_ap_keep_resultproduct * sto_bp_keep_resultproduct + sto_an_keep_resultproduct * sto_bn_keep_resultproduct) + sto_cn_keep_resultproduct = (sto_ap_keep_resultproduct * sto_bn_keep_resultproduct + sto_an_keep_resultproduct * sto_bp_keep_resultproduct) + sto_cp_keep_resultproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_keep_resultnondivisor. (n) = (d) * pvs_factor_keep_resultnondivisor)) /\ ((z)=0))))