dirichlet_convolution_entry_complement

Exact expanded first-order arithmetic statement

forall F G n d q z. ~(n=0) -> ((((~((d)=0)) /\ ((n)=(d)*(q)))) \/ ((((d)=0 \/ ~(exists pvs_factor_swap_complementnondivisor. (n) = (d) * pvs_factor_swap_complementnondivisor)) /\ ((q)=(d))))) -> ((((~((q)=0)) /\ (exists dc_quotient_swap_source dc_left_swap_source dc_right_swap_source. (((n)=(q)*dc_quotient_swap_source) /\ (((exists dst_positive_code_swap_sourceleft dst_positive_scale_swap_sourceleft dst_negative_code_swap_sourceleft dst_negative_scale_swap_sourceleft dst_positive_swap_sourceleft dst_negative_swap_sourceleft. (((F) = (((((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) * S ((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) + ((dst_positive_scale_swap_sourceleft) + (dst_positive_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))) * S ((((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) * S ((dst_positive_code_swap_sourceleft) + (dst_positive_scale_swap_sourceleft)) + ((dst_positive_scale_swap_sourceleft) + (dst_positive_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))) + ((((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft))) + (((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) * S ((dst_negative_code_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)) + ((dst_negative_scale_swap_sourceleft) + (dst_negative_scale_swap_sourceleft)))))) /\ (((((exists ff_h_pvs_swap_sourceleftpositive. ff_h_pvs_swap_sourceleftpositive + S (dst_positive_swap_sourceleft) = S ((S (q)) * dst_positive_scale_swap_sourceleft)) /\ exists ff_q_pvs_swap_sourceleftpositive. dst_positive_code_swap_sourceleft = ff_q_pvs_swap_sourceleftpositive * S ((S (q)) * dst_positive_scale_swap_sourceleft) + (dst_positive_swap_sourceleft))) /\ (((((exists ff_h_pvs_swap_sourceleftnegative. ff_h_pvs_swap_sourceleftnegative + S (dst_negative_swap_sourceleft) = S ((S (q)) * dst_negative_scale_swap_sourceleft)) /\ exists ff_q_pvs_swap_sourceleftnegative. dst_negative_code_swap_sourceleft = ff_q_pvs_swap_sourceleftnegative * S ((S (q)) * dst_negative_scale_swap_sourceleft) + (dst_negative_swap_sourceleft))) /\ (exists ge_balance_positive_swap_sourceleftvalue ge_balance_negative_swap_sourceleftvalue. (((((dc_left_swap_source) = 2 * (ge_balance_positive_swap_sourceleftvalue) /\ (ge_balance_negative_swap_sourceleftvalue) = 0) \/ exists ge_signed_half_swap_sourceleftvaluedecode. (((dc_left_swap_source) = 2 * ge_signed_half_swap_sourceleftvaluedecode + 1 /\ (ge_balance_positive_swap_sourceleftvalue) = 0) /\ (ge_balance_negative_swap_sourceleftvalue) = S ge_signed_half_swap_sourceleftvaluedecode))) /\ ((dst_positive_swap_sourceleft) + ge_balance_negative_swap_sourceleftvalue = (dst_negative_swap_sourceleft) + ge_balance_positive_swap_sourceleftvalue))))))))) /\ (((exists dst_positive_code_swap_sourceright dst_positive_scale_swap_sourceright dst_negative_code_swap_sourceright dst_negative_scale_swap_sourceright dst_positive_swap_sourceright dst_negative_swap_sourceright. (((G) = (((((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) * S ((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) + ((dst_positive_scale_swap_sourceright) + (dst_positive_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))) * S ((((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) * S ((dst_positive_code_swap_sourceright) + (dst_positive_scale_swap_sourceright)) + ((dst_positive_scale_swap_sourceright) + (dst_positive_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))) + ((((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright))) + (((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) * S ((dst_negative_code_swap_sourceright) + (dst_negative_scale_swap_sourceright)) + ((dst_negative_scale_swap_sourceright) + (dst_negative_scale_swap_sourceright)))))) /\ (((((exists ff_h_pvs_swap_sourcerightpositive. ff_h_pvs_swap_sourcerightpositive + S (dst_positive_swap_sourceright) = S ((S (dc_quotient_swap_source)) * dst_positive_scale_swap_sourceright)) /\ exists ff_q_pvs_swap_sourcerightpositive. dst_positive_code_swap_sourceright = ff_q_pvs_swap_sourcerightpositive * S ((S (dc_quotient_swap_source)) * dst_positive_scale_swap_sourceright) + (dst_positive_swap_sourceright))) /\ (((((exists ff_h_pvs_swap_sourcerightnegative. ff_h_pvs_swap_sourcerightnegative + S (dst_negative_swap_sourceright) = S ((S (dc_quotient_swap_source)) * dst_negative_scale_swap_sourceright)) /\ exists ff_q_pvs_swap_sourcerightnegative. dst_negative_code_swap_sourceright = ff_q_pvs_swap_sourcerightnegative * S ((S (dc_quotient_swap_source)) * dst_negative_scale_swap_sourceright) + (dst_negative_swap_sourceright))) /\ (exists ge_balance_positive_swap_sourcerightvalue ge_balance_negative_swap_sourcerightvalue. (((((dc_right_swap_source) = 2 * (ge_balance_positive_swap_sourcerightvalue) /\ (ge_balance_negative_swap_sourcerightvalue) = 0) \/ exists ge_signed_half_swap_sourcerightvaluedecode. (((dc_right_swap_source) = 2 * ge_signed_half_swap_sourcerightvaluedecode + 1 /\ (ge_balance_positive_swap_sourcerightvalue) = 0) /\ (ge_balance_negative_swap_sourcerightvalue) = S ge_signed_half_swap_sourcerightvaluedecode))) /\ ((dst_positive_swap_sourceright) + ge_balance_negative_swap_sourcerightvalue = (dst_negative_swap_sourceright) + ge_balance_positive_swap_sourcerightvalue))))))))) /\ (exists sto_ap_swap_sourceproduct sto_an_swap_sourceproduct sto_bp_swap_sourceproduct sto_bn_swap_sourceproduct sto_cp_swap_sourceproduct sto_cn_swap_sourceproduct. (((((dc_left_swap_source) = 2 * (sto_ap_swap_sourceproduct) /\ (sto_an_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductleft. (((dc_left_swap_source) = 2 * ge_signed_half_swap_sourceproductleft + 1 /\ (sto_ap_swap_sourceproduct) = 0) /\ (sto_an_swap_sourceproduct) = S ge_signed_half_swap_sourceproductleft))) /\ ((((((dc_right_swap_source) = 2 * (sto_bp_swap_sourceproduct) /\ (sto_bn_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductright. (((dc_right_swap_source) = 2 * ge_signed_half_swap_sourceproductright + 1 /\ (sto_bp_swap_sourceproduct) = 0) /\ (sto_bn_swap_sourceproduct) = S ge_signed_half_swap_sourceproductright))) /\ ((((((z) = 2 * (sto_cp_swap_sourceproduct) /\ (sto_cn_swap_sourceproduct) = 0) \/ exists ge_signed_half_swap_sourceproductoutput. (((z) = 2 * ge_signed_half_swap_sourceproductoutput + 1 /\ (sto_cp_swap_sourceproduct) = 0) /\ (sto_cn_swap_sourceproduct) = S ge_signed_half_swap_sourceproductoutput))) /\ ((sto_ap_swap_sourceproduct * sto_bp_swap_sourceproduct + sto_an_swap_sourceproduct * sto_bn_swap_sourceproduct) + sto_cn_swap_sourceproduct = (sto_ap_swap_sourceproduct * sto_bn_swap_sourceproduct + sto_an_swap_sourceproduct * sto_bp_swap_sourceproduct) + sto_cp_swap_sourceproduct))))))))))))))) \/ ((((q)=0 \/ ~(exists pvs_factor_swap_sourcenondivisor. (n) = (q) * pvs_factor_swap_sourcenondivisor)) /\ ((z)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_swap_target dc_left_swap_target dc_right_swap_target. (((n)=(d)*dc_quotient_swap_target) /\ (((exists dst_positive_code_swap_targetleft dst_positive_scale_swap_targetleft dst_negative_code_swap_targetleft dst_negative_scale_swap_targetleft dst_positive_swap_targetleft dst_negative_swap_targetleft. (((G) = (((((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) * S ((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) + ((dst_positive_scale_swap_targetleft) + (dst_positive_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))) * S ((((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) * S ((dst_positive_code_swap_targetleft) + (dst_positive_scale_swap_targetleft)) + ((dst_positive_scale_swap_targetleft) + (dst_positive_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))) + ((((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft))) + (((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) * S ((dst_negative_code_swap_targetleft) + (dst_negative_scale_swap_targetleft)) + ((dst_negative_scale_swap_targetleft) + (dst_negative_scale_swap_targetleft)))))) /\ (((((exists ff_h_pvs_swap_targetleftpositive. ff_h_pvs_swap_targetleftpositive + S (dst_positive_swap_targetleft) = S ((S (d)) * dst_positive_scale_swap_targetleft)) /\ exists ff_q_pvs_swap_targetleftpositive. dst_positive_code_swap_targetleft = ff_q_pvs_swap_targetleftpositive * S ((S (d)) * dst_positive_scale_swap_targetleft) + (dst_positive_swap_targetleft))) /\ (((((exists ff_h_pvs_swap_targetleftnegative. ff_h_pvs_swap_targetleftnegative + S (dst_negative_swap_targetleft) = S ((S (d)) * dst_negative_scale_swap_targetleft)) /\ exists ff_q_pvs_swap_targetleftnegative. dst_negative_code_swap_targetleft = ff_q_pvs_swap_targetleftnegative * S ((S (d)) * dst_negative_scale_swap_targetleft) + (dst_negative_swap_targetleft))) /\ (exists ge_balance_positive_swap_targetleftvalue ge_balance_negative_swap_targetleftvalue. (((((dc_left_swap_target) = 2 * (ge_balance_positive_swap_targetleftvalue) /\ (ge_balance_negative_swap_targetleftvalue) = 0) \/ exists ge_signed_half_swap_targetleftvaluedecode. (((dc_left_swap_target) = 2 * ge_signed_half_swap_targetleftvaluedecode + 1 /\ (ge_balance_positive_swap_targetleftvalue) = 0) /\ (ge_balance_negative_swap_targetleftvalue) = S ge_signed_half_swap_targetleftvaluedecode))) /\ ((dst_positive_swap_targetleft) + ge_balance_negative_swap_targetleftvalue = (dst_negative_swap_targetleft) + ge_balance_positive_swap_targetleftvalue))))))))) /\ (((exists dst_positive_code_swap_targetright dst_positive_scale_swap_targetright dst_negative_code_swap_targetright dst_negative_scale_swap_targetright dst_positive_swap_targetright dst_negative_swap_targetright. (((F) = (((((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) * S ((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) + ((dst_positive_scale_swap_targetright) + (dst_positive_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))) * S ((((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) * S ((dst_positive_code_swap_targetright) + (dst_positive_scale_swap_targetright)) + ((dst_positive_scale_swap_targetright) + (dst_positive_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))) + ((((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright))) + (((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) * S ((dst_negative_code_swap_targetright) + (dst_negative_scale_swap_targetright)) + ((dst_negative_scale_swap_targetright) + (dst_negative_scale_swap_targetright)))))) /\ (((((exists ff_h_pvs_swap_targetrightpositive. ff_h_pvs_swap_targetrightpositive + S (dst_positive_swap_targetright) = S ((S (dc_quotient_swap_target)) * dst_positive_scale_swap_targetright)) /\ exists ff_q_pvs_swap_targetrightpositive. dst_positive_code_swap_targetright = ff_q_pvs_swap_targetrightpositive * S ((S (dc_quotient_swap_target)) * dst_positive_scale_swap_targetright) + (dst_positive_swap_targetright))) /\ (((((exists ff_h_pvs_swap_targetrightnegative. ff_h_pvs_swap_targetrightnegative + S (dst_negative_swap_targetright) = S ((S (dc_quotient_swap_target)) * dst_negative_scale_swap_targetright)) /\ exists ff_q_pvs_swap_targetrightnegative. dst_negative_code_swap_targetright = ff_q_pvs_swap_targetrightnegative * S ((S (dc_quotient_swap_target)) * dst_negative_scale_swap_targetright) + (dst_negative_swap_targetright))) /\ (exists ge_balance_positive_swap_targetrightvalue ge_balance_negative_swap_targetrightvalue. (((((dc_right_swap_target) = 2 * (ge_balance_positive_swap_targetrightvalue) /\ (ge_balance_negative_swap_targetrightvalue) = 0) \/ exists ge_signed_half_swap_targetrightvaluedecode. (((dc_right_swap_target) = 2 * ge_signed_half_swap_targetrightvaluedecode + 1 /\ (ge_balance_positive_swap_targetrightvalue) = 0) /\ (ge_balance_negative_swap_targetrightvalue) = S ge_signed_half_swap_targetrightvaluedecode))) /\ ((dst_positive_swap_targetright) + ge_balance_negative_swap_targetrightvalue = (dst_negative_swap_targetright) + ge_balance_positive_swap_targetrightvalue))))))))) /\ (exists sto_ap_swap_targetproduct sto_an_swap_targetproduct sto_bp_swap_targetproduct sto_bn_swap_targetproduct sto_cp_swap_targetproduct sto_cn_swap_targetproduct. (((((dc_left_swap_target) = 2 * (sto_ap_swap_targetproduct) /\ (sto_an_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductleft. (((dc_left_swap_target) = 2 * ge_signed_half_swap_targetproductleft + 1 /\ (sto_ap_swap_targetproduct) = 0) /\ (sto_an_swap_targetproduct) = S ge_signed_half_swap_targetproductleft))) /\ ((((((dc_right_swap_target) = 2 * (sto_bp_swap_targetproduct) /\ (sto_bn_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductright. (((dc_right_swap_target) = 2 * ge_signed_half_swap_targetproductright + 1 /\ (sto_bp_swap_targetproduct) = 0) /\ (sto_bn_swap_targetproduct) = S ge_signed_half_swap_targetproductright))) /\ ((((((z) = 2 * (sto_cp_swap_targetproduct) /\ (sto_cn_swap_targetproduct) = 0) \/ exists ge_signed_half_swap_targetproductoutput. (((z) = 2 * ge_signed_half_swap_targetproductoutput + 1 /\ (sto_cp_swap_targetproduct) = 0) /\ (sto_cn_swap_targetproduct) = S ge_signed_half_swap_targetproductoutput))) /\ ((sto_ap_swap_targetproduct * sto_bp_swap_targetproduct + sto_an_swap_targetproduct * sto_bn_swap_targetproduct) + sto_cn_swap_targetproduct = (sto_ap_swap_targetproduct * sto_bn_swap_targetproduct + sto_an_swap_targetproduct * sto_bp_swap_targetproduct) + sto_cp_swap_targetproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_swap_targetnondivisor. (n) = (d) * pvs_factor_swap_targetnondivisor)) /\ ((z)=0))))