gaussian_division_divisible_remainder_zero

Exact expanded first-order arithmetic statement

forall a b q r U V. (exists ge_division_product_divisible_equation. ((exists ge_first_rp_divisible_equationproduct ge_first_rn_divisible_equationproduct ge_first_ip_divisible_equationproduct ge_first_in_divisible_equationproduct ge_second_rp_divisible_equationproduct ge_second_rn_divisible_equationproduct ge_second_ip_divisible_equationproduct ge_second_in_divisible_equationproduct. ((exists ge_representation_real_code_divisible_equationproductfirst ge_representation_imaginary_code_divisible_equationproductfirst. (((b) = ((ge_representation_real_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst)) * S ((ge_representation_real_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst)) + ((ge_representation_imaginary_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst))) /\ ((exists ge_balance_positive_divisible_equationproductfirstreal ge_balance_negative_divisible_equationproductfirstreal. (((((ge_representation_real_code_divisible_equationproductfirst) = 2 * (ge_balance_positive_divisible_equationproductfirstreal) /\ (ge_balance_negative_divisible_equationproductfirstreal) = 0) \/ exists ge_signed_half_divisible_equationproductfirstrealdecode. (((ge_representation_real_code_divisible_equationproductfirst) = 2 * ge_signed_half_divisible_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductfirstreal) = 0) /\ (ge_balance_negative_divisible_equationproductfirstreal) = S ge_signed_half_divisible_equationproductfirstrealdecode))) /\ ((ge_first_rp_divisible_equationproduct) + ge_balance_negative_divisible_equationproductfirstreal = (ge_first_rn_divisible_equationproduct) + ge_balance_positive_divisible_equationproductfirstreal))) /\ (exists ge_balance_positive_divisible_equationproductfirstimaginary ge_balance_negative_divisible_equationproductfirstimaginary. (((((ge_representation_imaginary_code_divisible_equationproductfirst) = 2 * (ge_balance_positive_divisible_equationproductfirstimaginary) /\ (ge_balance_negative_divisible_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductfirst) = 2 * ge_signed_half_divisible_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductfirstimaginary) = S ge_signed_half_divisible_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_divisible_equationproduct) + ge_balance_negative_divisible_equationproductfirstimaginary = (ge_first_in_divisible_equationproduct) + ge_balance_positive_divisible_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_equationproductsecond ge_representation_imaginary_code_divisible_equationproductsecond. (((q) = ((ge_representation_real_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond)) * S ((ge_representation_real_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond)) + ((ge_representation_imaginary_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond))) /\ ((exists ge_balance_positive_divisible_equationproductsecondreal ge_balance_negative_divisible_equationproductsecondreal. (((((ge_representation_real_code_divisible_equationproductsecond) = 2 * (ge_balance_positive_divisible_equationproductsecondreal) /\ (ge_balance_negative_divisible_equationproductsecondreal) = 0) \/ exists ge_signed_half_divisible_equationproductsecondrealdecode. (((ge_representation_real_code_divisible_equationproductsecond) = 2 * ge_signed_half_divisible_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductsecondreal) = 0) /\ (ge_balance_negative_divisible_equationproductsecondreal) = S ge_signed_half_divisible_equationproductsecondrealdecode))) /\ ((ge_second_rp_divisible_equationproduct) + ge_balance_negative_divisible_equationproductsecondreal = (ge_second_rn_divisible_equationproduct) + ge_balance_positive_divisible_equationproductsecondreal))) /\ (exists ge_balance_positive_divisible_equationproductsecondimaginary ge_balance_negative_divisible_equationproductsecondimaginary. (((((ge_representation_imaginary_code_divisible_equationproductsecond) = 2 * (ge_balance_positive_divisible_equationproductsecondimaginary) /\ (ge_balance_negative_divisible_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductsecond) = 2 * ge_signed_half_divisible_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductsecondimaginary) = S ge_signed_half_divisible_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_divisible_equationproduct) + ge_balance_negative_divisible_equationproductsecondimaginary = (ge_second_in_divisible_equationproduct) + ge_balance_positive_divisible_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_equationproductoutput ge_representation_imaginary_code_divisible_equationproductoutput. (((ge_division_product_divisible_equation) = ((ge_representation_real_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput)) * S ((ge_representation_real_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput)) + ((ge_representation_imaginary_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput))) /\ ((exists ge_balance_positive_divisible_equationproductoutputreal ge_balance_negative_divisible_equationproductoutputreal. (((((ge_representation_real_code_divisible_equationproductoutput) = 2 * (ge_balance_positive_divisible_equationproductoutputreal) /\ (ge_balance_negative_divisible_equationproductoutputreal) = 0) \/ exists ge_signed_half_divisible_equationproductoutputrealdecode. (((ge_representation_real_code_divisible_equationproductoutput) = 2 * ge_signed_half_divisible_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductoutputreal) = 0) /\ (ge_balance_negative_divisible_equationproductoutputreal) = S ge_signed_half_divisible_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))))))) + ge_balance_negative_divisible_equationproductoutputreal = (((((((ge_first_rp_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))))))) + ge_balance_positive_divisible_equationproductoutputreal))) /\ (exists ge_balance_positive_divisible_equationproductoutputimaginary ge_balance_negative_divisible_equationproductoutputimaginary. (((((ge_representation_imaginary_code_divisible_equationproductoutput) = 2 * (ge_balance_positive_divisible_equationproductoutputimaginary) /\ (ge_balance_negative_divisible_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductoutput) = 2 * ge_signed_half_divisible_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductoutputimaginary) = S ge_signed_half_divisible_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))))))) + ge_balance_negative_divisible_equationproductoutputimaginary = (((((((ge_first_rp_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))))))) + ge_balance_positive_divisible_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_divisible_equationsum ge_first_rn_divisible_equationsum ge_first_ip_divisible_equationsum ge_first_in_divisible_equationsum ge_second_rp_divisible_equationsum ge_second_rn_divisible_equationsum ge_second_ip_divisible_equationsum ge_second_in_divisible_equationsum. ((exists ge_representation_real_code_divisible_equationsumfirst ge_representation_imaginary_code_divisible_equationsumfirst. (((ge_division_product_divisible_equation) = ((ge_representation_real_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst)) * S ((ge_representation_real_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst)) + ((ge_representation_imaginary_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst))) /\ ((exists ge_balance_positive_divisible_equationsumfirstreal ge_balance_negative_divisible_equationsumfirstreal. (((((ge_representation_real_code_divisible_equationsumfirst) = 2 * (ge_balance_positive_divisible_equationsumfirstreal) /\ (ge_balance_negative_divisible_equationsumfirstreal) = 0) \/ exists ge_signed_half_divisible_equationsumfirstrealdecode. (((ge_representation_real_code_divisible_equationsumfirst) = 2 * ge_signed_half_divisible_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumfirstreal) = 0) /\ (ge_balance_negative_divisible_equationsumfirstreal) = S ge_signed_half_divisible_equationsumfirstrealdecode))) /\ ((ge_first_rp_divisible_equationsum) + ge_balance_negative_divisible_equationsumfirstreal = (ge_first_rn_divisible_equationsum) + ge_balance_positive_divisible_equationsumfirstreal))) /\ (exists ge_balance_positive_divisible_equationsumfirstimaginary ge_balance_negative_divisible_equationsumfirstimaginary. (((((ge_representation_imaginary_code_divisible_equationsumfirst) = 2 * (ge_balance_positive_divisible_equationsumfirstimaginary) /\ (ge_balance_negative_divisible_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumfirst) = 2 * ge_signed_half_divisible_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumfirstimaginary) = S ge_signed_half_divisible_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_divisible_equationsum) + ge_balance_negative_divisible_equationsumfirstimaginary = (ge_first_in_divisible_equationsum) + ge_balance_positive_divisible_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_equationsumsecond ge_representation_imaginary_code_divisible_equationsumsecond. (((r) = ((ge_representation_real_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond)) * S ((ge_representation_real_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond)) + ((ge_representation_imaginary_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond))) /\ ((exists ge_balance_positive_divisible_equationsumsecondreal ge_balance_negative_divisible_equationsumsecondreal. (((((ge_representation_real_code_divisible_equationsumsecond) = 2 * (ge_balance_positive_divisible_equationsumsecondreal) /\ (ge_balance_negative_divisible_equationsumsecondreal) = 0) \/ exists ge_signed_half_divisible_equationsumsecondrealdecode. (((ge_representation_real_code_divisible_equationsumsecond) = 2 * ge_signed_half_divisible_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumsecondreal) = 0) /\ (ge_balance_negative_divisible_equationsumsecondreal) = S ge_signed_half_divisible_equationsumsecondrealdecode))) /\ ((ge_second_rp_divisible_equationsum) + ge_balance_negative_divisible_equationsumsecondreal = (ge_second_rn_divisible_equationsum) + ge_balance_positive_divisible_equationsumsecondreal))) /\ (exists ge_balance_positive_divisible_equationsumsecondimaginary ge_balance_negative_divisible_equationsumsecondimaginary. (((((ge_representation_imaginary_code_divisible_equationsumsecond) = 2 * (ge_balance_positive_divisible_equationsumsecondimaginary) /\ (ge_balance_negative_divisible_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumsecond) = 2 * ge_signed_half_divisible_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumsecondimaginary) = S ge_signed_half_divisible_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_divisible_equationsum) + ge_balance_negative_divisible_equationsumsecondimaginary = (ge_second_in_divisible_equationsum) + ge_balance_positive_divisible_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_equationsumoutput ge_representation_imaginary_code_divisible_equationsumoutput. (((a) = ((ge_representation_real_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput)) * S ((ge_representation_real_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput)) + ((ge_representation_imaginary_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput))) /\ ((exists ge_balance_positive_divisible_equationsumoutputreal ge_balance_negative_divisible_equationsumoutputreal. (((((ge_representation_real_code_divisible_equationsumoutput) = 2 * (ge_balance_positive_divisible_equationsumoutputreal) /\ (ge_balance_negative_divisible_equationsumoutputreal) = 0) \/ exists ge_signed_half_divisible_equationsumoutputrealdecode. (((ge_representation_real_code_divisible_equationsumoutput) = 2 * ge_signed_half_divisible_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumoutputreal) = 0) /\ (ge_balance_negative_divisible_equationsumoutputreal) = S ge_signed_half_divisible_equationsumoutputrealdecode))) /\ ((((ge_first_rp_divisible_equationsum) + (ge_second_rp_divisible_equationsum))) + ge_balance_negative_divisible_equationsumoutputreal = (((ge_first_rn_divisible_equationsum) + (ge_second_rn_divisible_equationsum))) + ge_balance_positive_divisible_equationsumoutputreal))) /\ (exists ge_balance_positive_divisible_equationsumoutputimaginary ge_balance_negative_divisible_equationsumoutputimaginary. (((((ge_representation_imaginary_code_divisible_equationsumoutput) = 2 * (ge_balance_positive_divisible_equationsumoutputimaginary) /\ (ge_balance_negative_divisible_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumoutput) = 2 * ge_signed_half_divisible_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumoutputimaginary) = S ge_signed_half_divisible_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_divisible_equationsum) + (ge_second_ip_divisible_equationsum))) + ge_balance_negative_divisible_equationsumoutputimaginary = (((ge_first_in_divisible_equationsum) + (ge_second_in_divisible_equationsum))) + ge_balance_positive_divisible_equationsumoutputimaginary))))))))))) -> (exists ge_norm_rp_divisible_remainder_norm ge_norm_rn_divisible_remainder_norm ge_norm_ip_divisible_remainder_norm ge_norm_in_divisible_remainder_norm. ((exists ge_representation_real_code_divisible_remainder_normrepresentation ge_representation_imaginary_code_divisible_remainder_normrepresentation. (((r) = ((ge_representation_real_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation)) * S ((ge_representation_real_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation)) + ((ge_representation_imaginary_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation))) /\ ((exists ge_balance_positive_divisible_remainder_normrepresentationreal ge_balance_negative_divisible_remainder_normrepresentationreal. (((((ge_representation_real_code_divisible_remainder_normrepresentation) = 2 * (ge_balance_positive_divisible_remainder_normrepresentationreal) /\ (ge_balance_negative_divisible_remainder_normrepresentationreal) = 0) \/ exists ge_signed_half_divisible_remainder_normrepresentationrealdecode. (((ge_representation_real_code_divisible_remainder_normrepresentation) = 2 * ge_signed_half_divisible_remainder_normrepresentationrealdecode + 1 /\ (ge_balance_positive_divisible_remainder_normrepresentationreal) = 0) /\ (ge_balance_negative_divisible_remainder_normrepresentationreal) = S ge_signed_half_divisible_remainder_normrepresentationrealdecode))) /\ ((ge_norm_rp_divisible_remainder_norm) + ge_balance_negative_divisible_remainder_normrepresentationreal = (ge_norm_rn_divisible_remainder_norm) + ge_balance_positive_divisible_remainder_normrepresentationreal))) /\ (exists ge_balance_positive_divisible_remainder_normrepresentationimaginary ge_balance_negative_divisible_remainder_normrepresentationimaginary. (((((ge_representation_imaginary_code_divisible_remainder_normrepresentation) = 2 * (ge_balance_positive_divisible_remainder_normrepresentationimaginary) /\ (ge_balance_negative_divisible_remainder_normrepresentationimaginary) = 0) \/ exists ge_signed_half_divisible_remainder_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_divisible_remainder_normrepresentation) = 2 * ge_signed_half_divisible_remainder_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_divisible_remainder_normrepresentationimaginary) = 0) /\ (ge_balance_negative_divisible_remainder_normrepresentationimaginary) = S ge_signed_half_divisible_remainder_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_divisible_remainder_norm) + ge_balance_negative_divisible_remainder_normrepresentationimaginary = (ge_norm_in_divisible_remainder_norm) + ge_balance_positive_divisible_remainder_normrepresentationimaginary)))))) /\ (exists ge_real_square_divisible_remainder_normsquare ge_imaginary_square_divisible_remainder_normsquare. ((((((ge_norm_rp_divisible_remainder_norm) * (ge_norm_rp_divisible_remainder_norm))) + (((ge_norm_rn_divisible_remainder_norm) * (ge_norm_rn_divisible_remainder_norm)))) = ((ge_real_square_divisible_remainder_normsquare) + (((((ge_norm_rp_divisible_remainder_norm) * (ge_norm_rn_divisible_remainder_norm))) + (((ge_norm_rn_divisible_remainder_norm) * (ge_norm_rp_divisible_remainder_norm))))))) /\ ((((((ge_norm_ip_divisible_remainder_norm) * (ge_norm_ip_divisible_remainder_norm))) + (((ge_norm_in_divisible_remainder_norm) * (ge_norm_in_divisible_remainder_norm)))) = ((ge_imaginary_square_divisible_remainder_normsquare) + (((((ge_norm_ip_divisible_remainder_norm) * (ge_norm_in_divisible_remainder_norm))) + (((ge_norm_in_divisible_remainder_norm) * (ge_norm_ip_divisible_remainder_norm))))))) /\ ((U) = ge_real_square_divisible_remainder_normsquare + ge_imaginary_square_divisible_remainder_normsquare)))))) -> (exists ge_norm_rp_divisible_divisor_norm ge_norm_rn_divisible_divisor_norm ge_norm_ip_divisible_divisor_norm ge_norm_in_divisible_divisor_norm. ((exists ge_representation_real_code_divisible_divisor_normrepresentation ge_representation_imaginary_code_divisible_divisor_normrepresentation. (((b) = ((ge_representation_real_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation)) * S ((ge_representation_real_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation)) + ((ge_representation_imaginary_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation))) /\ ((exists ge_balance_positive_divisible_divisor_normrepresentationreal ge_balance_negative_divisible_divisor_normrepresentationreal. (((((ge_representation_real_code_divisible_divisor_normrepresentation) = 2 * (ge_balance_positive_divisible_divisor_normrepresentationreal) /\ (ge_balance_negative_divisible_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_divisible_divisor_normrepresentationrealdecode. (((ge_representation_real_code_divisible_divisor_normrepresentation) = 2 * ge_signed_half_divisible_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_divisible_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_divisible_divisor_normrepresentationreal) = S ge_signed_half_divisible_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_divisible_divisor_norm) + ge_balance_negative_divisible_divisor_normrepresentationreal = (ge_norm_rn_divisible_divisor_norm) + ge_balance_positive_divisible_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_divisible_divisor_normrepresentationimaginary ge_balance_negative_divisible_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_divisible_divisor_normrepresentation) = 2 * (ge_balance_positive_divisible_divisor_normrepresentationimaginary) /\ (ge_balance_negative_divisible_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_divisible_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_divisible_divisor_normrepresentation) = 2 * ge_signed_half_divisible_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_divisible_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_divisible_divisor_normrepresentationimaginary) = S ge_signed_half_divisible_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_divisible_divisor_norm) + ge_balance_negative_divisible_divisor_normrepresentationimaginary = (ge_norm_in_divisible_divisor_norm) + ge_balance_positive_divisible_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_divisible_divisor_normsquare ge_imaginary_square_divisible_divisor_normsquare. ((((((ge_norm_rp_divisible_divisor_norm) * (ge_norm_rp_divisible_divisor_norm))) + (((ge_norm_rn_divisible_divisor_norm) * (ge_norm_rn_divisible_divisor_norm)))) = ((ge_real_square_divisible_divisor_normsquare) + (((((ge_norm_rp_divisible_divisor_norm) * (ge_norm_rn_divisible_divisor_norm))) + (((ge_norm_rn_divisible_divisor_norm) * (ge_norm_rp_divisible_divisor_norm))))))) /\ ((((((ge_norm_ip_divisible_divisor_norm) * (ge_norm_ip_divisible_divisor_norm))) + (((ge_norm_in_divisible_divisor_norm) * (ge_norm_in_divisible_divisor_norm)))) = ((ge_imaginary_square_divisible_divisor_normsquare) + (((((ge_norm_ip_divisible_divisor_norm) * (ge_norm_in_divisible_divisor_norm))) + (((ge_norm_in_divisible_divisor_norm) * (ge_norm_ip_divisible_divisor_norm))))))) /\ ((V) = ge_real_square_divisible_divisor_normsquare + ge_imaginary_square_divisible_divisor_normsquare)))))) -> (exists ge_gap_divisible_strict. ge_gap_divisible_strict + S (U) = (V)) -> (exists gr_quotient_divisible_given. (exists ge_first_rp_divisible_givenproduct ge_first_rn_divisible_givenproduct ge_first_ip_divisible_givenproduct ge_first_in_divisible_givenproduct ge_second_rp_divisible_givenproduct ge_second_rn_divisible_givenproduct ge_second_ip_divisible_givenproduct ge_second_in_divisible_givenproduct. ((exists ge_representation_real_code_divisible_givenproductfirst ge_representation_imaginary_code_divisible_givenproductfirst. (((b) = ((ge_representation_real_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst)) * S ((ge_representation_real_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst)) + ((ge_representation_imaginary_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst))) /\ ((exists ge_balance_positive_divisible_givenproductfirstreal ge_balance_negative_divisible_givenproductfirstreal. (((((ge_representation_real_code_divisible_givenproductfirst) = 2 * (ge_balance_positive_divisible_givenproductfirstreal) /\ (ge_balance_negative_divisible_givenproductfirstreal) = 0) \/ exists ge_signed_half_divisible_givenproductfirstrealdecode. (((ge_representation_real_code_divisible_givenproductfirst) = 2 * ge_signed_half_divisible_givenproductfirstrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductfirstreal) = 0) /\ (ge_balance_negative_divisible_givenproductfirstreal) = S ge_signed_half_divisible_givenproductfirstrealdecode))) /\ ((ge_first_rp_divisible_givenproduct) + ge_balance_negative_divisible_givenproductfirstreal = (ge_first_rn_divisible_givenproduct) + ge_balance_positive_divisible_givenproductfirstreal))) /\ (exists ge_balance_positive_divisible_givenproductfirstimaginary ge_balance_negative_divisible_givenproductfirstimaginary. (((((ge_representation_imaginary_code_divisible_givenproductfirst) = 2 * (ge_balance_positive_divisible_givenproductfirstimaginary) /\ (ge_balance_negative_divisible_givenproductfirstimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductfirst) = 2 * ge_signed_half_divisible_givenproductfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductfirstimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductfirstimaginary) = S ge_signed_half_divisible_givenproductfirstimaginarydecode))) /\ ((ge_first_ip_divisible_givenproduct) + ge_balance_negative_divisible_givenproductfirstimaginary = (ge_first_in_divisible_givenproduct) + ge_balance_positive_divisible_givenproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_givenproductsecond ge_representation_imaginary_code_divisible_givenproductsecond. (((gr_quotient_divisible_given) = ((ge_representation_real_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond)) * S ((ge_representation_real_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond)) + ((ge_representation_imaginary_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond))) /\ ((exists ge_balance_positive_divisible_givenproductsecondreal ge_balance_negative_divisible_givenproductsecondreal. (((((ge_representation_real_code_divisible_givenproductsecond) = 2 * (ge_balance_positive_divisible_givenproductsecondreal) /\ (ge_balance_negative_divisible_givenproductsecondreal) = 0) \/ exists ge_signed_half_divisible_givenproductsecondrealdecode. (((ge_representation_real_code_divisible_givenproductsecond) = 2 * ge_signed_half_divisible_givenproductsecondrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductsecondreal) = 0) /\ (ge_balance_negative_divisible_givenproductsecondreal) = S ge_signed_half_divisible_givenproductsecondrealdecode))) /\ ((ge_second_rp_divisible_givenproduct) + ge_balance_negative_divisible_givenproductsecondreal = (ge_second_rn_divisible_givenproduct) + ge_balance_positive_divisible_givenproductsecondreal))) /\ (exists ge_balance_positive_divisible_givenproductsecondimaginary ge_balance_negative_divisible_givenproductsecondimaginary. (((((ge_representation_imaginary_code_divisible_givenproductsecond) = 2 * (ge_balance_positive_divisible_givenproductsecondimaginary) /\ (ge_balance_negative_divisible_givenproductsecondimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductsecond) = 2 * ge_signed_half_divisible_givenproductsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductsecondimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductsecondimaginary) = S ge_signed_half_divisible_givenproductsecondimaginarydecode))) /\ ((ge_second_ip_divisible_givenproduct) + ge_balance_negative_divisible_givenproductsecondimaginary = (ge_second_in_divisible_givenproduct) + ge_balance_positive_divisible_givenproductsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_givenproductoutput ge_representation_imaginary_code_divisible_givenproductoutput. (((a) = ((ge_representation_real_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput)) * S ((ge_representation_real_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput)) + ((ge_representation_imaginary_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput))) /\ ((exists ge_balance_positive_divisible_givenproductoutputreal ge_balance_negative_divisible_givenproductoutputreal. (((((ge_representation_real_code_divisible_givenproductoutput) = 2 * (ge_balance_positive_divisible_givenproductoutputreal) /\ (ge_balance_negative_divisible_givenproductoutputreal) = 0) \/ exists ge_signed_half_divisible_givenproductoutputrealdecode. (((ge_representation_real_code_divisible_givenproductoutput) = 2 * ge_signed_half_divisible_givenproductoutputrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductoutputreal) = 0) /\ (ge_balance_negative_divisible_givenproductoutputreal) = S ge_signed_half_divisible_givenproductoutputrealdecode))) /\ ((((((((ge_first_rp_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))))))) + ge_balance_negative_divisible_givenproductoutputreal = (((((((ge_first_rp_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))))))) + ge_balance_positive_divisible_givenproductoutputreal))) /\ (exists ge_balance_positive_divisible_givenproductoutputimaginary ge_balance_negative_divisible_givenproductoutputimaginary. (((((ge_representation_imaginary_code_divisible_givenproductoutput) = 2 * (ge_balance_positive_divisible_givenproductoutputimaginary) /\ (ge_balance_negative_divisible_givenproductoutputimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductoutput) = 2 * ge_signed_half_divisible_givenproductoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductoutputimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductoutputimaginary) = S ge_signed_half_divisible_givenproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))))))) + ge_balance_negative_divisible_givenproductoutputimaginary = (((((((ge_first_rp_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))))))) + ge_balance_positive_divisible_givenproductoutputimaginary)))))))))) -> r=0