gaussian_nonunit_divisor_strict_quotient

Exact expanded first-order arithmetic statement

forall d z D N. (exists gr_quotient_quotient_divisor. (exists ge_first_rp_quotient_divisorproduct ge_first_rn_quotient_divisorproduct ge_first_ip_quotient_divisorproduct ge_first_in_quotient_divisorproduct ge_second_rp_quotient_divisorproduct ge_second_rn_quotient_divisorproduct ge_second_ip_quotient_divisorproduct ge_second_in_quotient_divisorproduct. ((exists ge_representation_real_code_quotient_divisorproductfirst ge_representation_imaginary_code_quotient_divisorproductfirst. (((d) = ((ge_representation_real_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst)) * S ((ge_representation_real_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst)) + ((ge_representation_imaginary_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst))) /\ ((exists ge_balance_positive_quotient_divisorproductfirstreal ge_balance_negative_quotient_divisorproductfirstreal. (((((ge_representation_real_code_quotient_divisorproductfirst) = 2 * (ge_balance_positive_quotient_divisorproductfirstreal) /\ (ge_balance_negative_quotient_divisorproductfirstreal) = 0) \/ exists ge_signed_half_quotient_divisorproductfirstrealdecode. (((ge_representation_real_code_quotient_divisorproductfirst) = 2 * ge_signed_half_quotient_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductfirstreal) = 0) /\ (ge_balance_negative_quotient_divisorproductfirstreal) = S ge_signed_half_quotient_divisorproductfirstrealdecode))) /\ ((ge_first_rp_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductfirstreal = (ge_first_rn_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductfirstreal))) /\ (exists ge_balance_positive_quotient_divisorproductfirstimaginary ge_balance_negative_quotient_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductfirst) = 2 * (ge_balance_positive_quotient_divisorproductfirstimaginary) /\ (ge_balance_negative_quotient_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductfirst) = 2 * ge_signed_half_quotient_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductfirstimaginary) = S ge_signed_half_quotient_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductfirstimaginary = (ge_first_in_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_divisorproductsecond ge_representation_imaginary_code_quotient_divisorproductsecond. (((gr_quotient_quotient_divisor) = ((ge_representation_real_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond)) * S ((ge_representation_real_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond)) + ((ge_representation_imaginary_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond))) /\ ((exists ge_balance_positive_quotient_divisorproductsecondreal ge_balance_negative_quotient_divisorproductsecondreal. (((((ge_representation_real_code_quotient_divisorproductsecond) = 2 * (ge_balance_positive_quotient_divisorproductsecondreal) /\ (ge_balance_negative_quotient_divisorproductsecondreal) = 0) \/ exists ge_signed_half_quotient_divisorproductsecondrealdecode. (((ge_representation_real_code_quotient_divisorproductsecond) = 2 * ge_signed_half_quotient_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductsecondreal) = 0) /\ (ge_balance_negative_quotient_divisorproductsecondreal) = S ge_signed_half_quotient_divisorproductsecondrealdecode))) /\ ((ge_second_rp_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductsecondreal = (ge_second_rn_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductsecondreal))) /\ (exists ge_balance_positive_quotient_divisorproductsecondimaginary ge_balance_negative_quotient_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductsecond) = 2 * (ge_balance_positive_quotient_divisorproductsecondimaginary) /\ (ge_balance_negative_quotient_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductsecond) = 2 * ge_signed_half_quotient_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductsecondimaginary) = S ge_signed_half_quotient_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductsecondimaginary = (ge_second_in_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_divisorproductoutput ge_representation_imaginary_code_quotient_divisorproductoutput. (((z) = ((ge_representation_real_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput)) * S ((ge_representation_real_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput)) + ((ge_representation_imaginary_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput))) /\ ((exists ge_balance_positive_quotient_divisorproductoutputreal ge_balance_negative_quotient_divisorproductoutputreal. (((((ge_representation_real_code_quotient_divisorproductoutput) = 2 * (ge_balance_positive_quotient_divisorproductoutputreal) /\ (ge_balance_negative_quotient_divisorproductoutputreal) = 0) \/ exists ge_signed_half_quotient_divisorproductoutputrealdecode. (((ge_representation_real_code_quotient_divisorproductoutput) = 2 * ge_signed_half_quotient_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductoutputreal) = 0) /\ (ge_balance_negative_quotient_divisorproductoutputreal) = S ge_signed_half_quotient_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))))))) + ge_balance_negative_quotient_divisorproductoutputreal = (((((((ge_first_rp_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))))))) + ge_balance_positive_quotient_divisorproductoutputreal))) /\ (exists ge_balance_positive_quotient_divisorproductoutputimaginary ge_balance_negative_quotient_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductoutput) = 2 * (ge_balance_positive_quotient_divisorproductoutputimaginary) /\ (ge_balance_negative_quotient_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductoutput) = 2 * ge_signed_half_quotient_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductoutputimaginary) = S ge_signed_half_quotient_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))))))) + ge_balance_negative_quotient_divisorproductoutputimaginary = (((((((ge_first_rp_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))))))) + ge_balance_positive_quotient_divisorproductoutputimaginary)))))))))) -> (exists ge_norm_rp_quotient_divisor_norm ge_norm_rn_quotient_divisor_norm ge_norm_ip_quotient_divisor_norm ge_norm_in_quotient_divisor_norm. ((exists ge_representation_real_code_quotient_divisor_normrepresentation ge_representation_imaginary_code_quotient_divisor_normrepresentation. (((d) = ((ge_representation_real_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation)) * S ((ge_representation_real_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation)) + ((ge_representation_imaginary_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation))) /\ ((exists ge_balance_positive_quotient_divisor_normrepresentationreal ge_balance_negative_quotient_divisor_normrepresentationreal. (((((ge_representation_real_code_quotient_divisor_normrepresentation) = 2 * (ge_balance_positive_quotient_divisor_normrepresentationreal) /\ (ge_balance_negative_quotient_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_divisor_normrepresentationrealdecode. (((ge_representation_real_code_quotient_divisor_normrepresentation) = 2 * ge_signed_half_quotient_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_divisor_normrepresentationreal) = S ge_signed_half_quotient_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_divisor_norm) + ge_balance_negative_quotient_divisor_normrepresentationreal = (ge_norm_rn_quotient_divisor_norm) + ge_balance_positive_quotient_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_divisor_normrepresentationimaginary ge_balance_negative_quotient_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_divisor_normrepresentation) = 2 * (ge_balance_positive_quotient_divisor_normrepresentationimaginary) /\ (ge_balance_negative_quotient_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_divisor_normrepresentation) = 2 * ge_signed_half_quotient_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_divisor_normrepresentationimaginary) = S ge_signed_half_quotient_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_divisor_norm) + ge_balance_negative_quotient_divisor_normrepresentationimaginary = (ge_norm_in_quotient_divisor_norm) + ge_balance_positive_quotient_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_divisor_normsquare ge_imaginary_square_quotient_divisor_normsquare. ((((((ge_norm_rp_quotient_divisor_norm) * (ge_norm_rp_quotient_divisor_norm))) + (((ge_norm_rn_quotient_divisor_norm) * (ge_norm_rn_quotient_divisor_norm)))) = ((ge_real_square_quotient_divisor_normsquare) + (((((ge_norm_rp_quotient_divisor_norm) * (ge_norm_rn_quotient_divisor_norm))) + (((ge_norm_rn_quotient_divisor_norm) * (ge_norm_rp_quotient_divisor_norm))))))) /\ ((((((ge_norm_ip_quotient_divisor_norm) * (ge_norm_ip_quotient_divisor_norm))) + (((ge_norm_in_quotient_divisor_norm) * (ge_norm_in_quotient_divisor_norm)))) = ((ge_imaginary_square_quotient_divisor_normsquare) + (((((ge_norm_ip_quotient_divisor_norm) * (ge_norm_in_quotient_divisor_norm))) + (((ge_norm_in_quotient_divisor_norm) * (ge_norm_ip_quotient_divisor_norm))))))) /\ ((D) = ge_real_square_quotient_divisor_normsquare + ge_imaginary_square_quotient_divisor_normsquare)))))) -> (exists ge_norm_rp_quotient_total_norm ge_norm_rn_quotient_total_norm ge_norm_ip_quotient_total_norm ge_norm_in_quotient_total_norm. ((exists ge_representation_real_code_quotient_total_normrepresentation ge_representation_imaginary_code_quotient_total_normrepresentation. (((z) = ((ge_representation_real_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation)) * S ((ge_representation_real_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation)) + ((ge_representation_imaginary_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation))) /\ ((exists ge_balance_positive_quotient_total_normrepresentationreal ge_balance_negative_quotient_total_normrepresentationreal. (((((ge_representation_real_code_quotient_total_normrepresentation) = 2 * (ge_balance_positive_quotient_total_normrepresentationreal) /\ (ge_balance_negative_quotient_total_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_total_normrepresentationrealdecode. (((ge_representation_real_code_quotient_total_normrepresentation) = 2 * ge_signed_half_quotient_total_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_total_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_total_normrepresentationreal) = S ge_signed_half_quotient_total_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_total_norm) + ge_balance_negative_quotient_total_normrepresentationreal = (ge_norm_rn_quotient_total_norm) + ge_balance_positive_quotient_total_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_total_normrepresentationimaginary ge_balance_negative_quotient_total_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_total_normrepresentation) = 2 * (ge_balance_positive_quotient_total_normrepresentationimaginary) /\ (ge_balance_negative_quotient_total_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_total_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_total_normrepresentation) = 2 * ge_signed_half_quotient_total_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_total_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_total_normrepresentationimaginary) = S ge_signed_half_quotient_total_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_total_norm) + ge_balance_negative_quotient_total_normrepresentationimaginary = (ge_norm_in_quotient_total_norm) + ge_balance_positive_quotient_total_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_total_normsquare ge_imaginary_square_quotient_total_normsquare. ((((((ge_norm_rp_quotient_total_norm) * (ge_norm_rp_quotient_total_norm))) + (((ge_norm_rn_quotient_total_norm) * (ge_norm_rn_quotient_total_norm)))) = ((ge_real_square_quotient_total_normsquare) + (((((ge_norm_rp_quotient_total_norm) * (ge_norm_rn_quotient_total_norm))) + (((ge_norm_rn_quotient_total_norm) * (ge_norm_rp_quotient_total_norm))))))) /\ ((((((ge_norm_ip_quotient_total_norm) * (ge_norm_ip_quotient_total_norm))) + (((ge_norm_in_quotient_total_norm) * (ge_norm_in_quotient_total_norm)))) = ((ge_imaginary_square_quotient_total_normsquare) + (((((ge_norm_ip_quotient_total_norm) * (ge_norm_in_quotient_total_norm))) + (((ge_norm_in_quotient_total_norm) * (ge_norm_ip_quotient_total_norm))))))) /\ ((N) = ge_real_square_quotient_total_normsquare + ge_imaginary_square_quotient_total_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_quotient_nonunit. (exists ge_first_rp_quotient_nonunitidentity ge_first_rn_quotient_nonunitidentity ge_first_ip_quotient_nonunitidentity ge_first_in_quotient_nonunitidentity ge_second_rp_quotient_nonunitidentity ge_second_rn_quotient_nonunitidentity ge_second_ip_quotient_nonunitidentity ge_second_in_quotient_nonunitidentity. ((exists ge_representation_real_code_quotient_nonunitidentityfirst ge_representation_imaginary_code_quotient_nonunitidentityfirst. (((d) = ((ge_representation_real_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst)) * S ((ge_representation_real_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst)) + ((ge_representation_imaginary_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst))) /\ ((exists ge_balance_positive_quotient_nonunitidentityfirstreal ge_balance_negative_quotient_nonunitidentityfirstreal. (((((ge_representation_real_code_quotient_nonunitidentityfirst) = 2 * (ge_balance_positive_quotient_nonunitidentityfirstreal) /\ (ge_balance_negative_quotient_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentityfirstrealdecode. (((ge_representation_real_code_quotient_nonunitidentityfirst) = 2 * ge_signed_half_quotient_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentityfirstreal) = S ge_signed_half_quotient_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentityfirstreal = (ge_first_rn_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_quotient_nonunitidentityfirstimaginary ge_balance_negative_quotient_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentityfirst) = 2 * (ge_balance_positive_quotient_nonunitidentityfirstimaginary) /\ (ge_balance_negative_quotient_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentityfirst) = 2 * ge_signed_half_quotient_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentityfirstimaginary) = S ge_signed_half_quotient_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentityfirstimaginary = (ge_first_in_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_nonunitidentitysecond ge_representation_imaginary_code_quotient_nonunitidentitysecond. (((gr_inverse_quotient_nonunit) = ((ge_representation_real_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond)) * S ((ge_representation_real_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond)) + ((ge_representation_imaginary_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond))) /\ ((exists ge_balance_positive_quotient_nonunitidentitysecondreal ge_balance_negative_quotient_nonunitidentitysecondreal. (((((ge_representation_real_code_quotient_nonunitidentitysecond) = 2 * (ge_balance_positive_quotient_nonunitidentitysecondreal) /\ (ge_balance_negative_quotient_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentitysecondrealdecode. (((ge_representation_real_code_quotient_nonunitidentitysecond) = 2 * ge_signed_half_quotient_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentitysecondreal) = S ge_signed_half_quotient_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentitysecondreal = (ge_second_rn_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_quotient_nonunitidentitysecondimaginary ge_balance_negative_quotient_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentitysecond) = 2 * (ge_balance_positive_quotient_nonunitidentitysecondimaginary) /\ (ge_balance_negative_quotient_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentitysecond) = 2 * ge_signed_half_quotient_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentitysecondimaginary) = S ge_signed_half_quotient_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentitysecondimaginary = (ge_second_in_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_nonunitidentityoutput ge_representation_imaginary_code_quotient_nonunitidentityoutput. (((6) = ((ge_representation_real_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput)) * S ((ge_representation_real_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput)) + ((ge_representation_imaginary_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput))) /\ ((exists ge_balance_positive_quotient_nonunitidentityoutputreal ge_balance_negative_quotient_nonunitidentityoutputreal. (((((ge_representation_real_code_quotient_nonunitidentityoutput) = 2 * (ge_balance_positive_quotient_nonunitidentityoutputreal) /\ (ge_balance_negative_quotient_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentityoutputrealdecode. (((ge_representation_real_code_quotient_nonunitidentityoutput) = 2 * ge_signed_half_quotient_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentityoutputreal) = S ge_signed_half_quotient_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))))))) + ge_balance_negative_quotient_nonunitidentityoutputreal = (((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))))))) + ge_balance_positive_quotient_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_quotient_nonunitidentityoutputimaginary ge_balance_negative_quotient_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentityoutput) = 2 * (ge_balance_positive_quotient_nonunitidentityoutputimaginary) /\ (ge_balance_negative_quotient_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentityoutput) = 2 * ge_signed_half_quotient_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentityoutputimaginary) = S ge_signed_half_quotient_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))))))) + ge_balance_negative_quotient_nonunitidentityoutputimaginary = (((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))))))) + ge_balance_positive_quotient_nonunitidentityoutputimaginary)))))))))) -> exists q Q. ((exists ge_first_rp_quotient_product ge_first_rn_quotient_product ge_first_ip_quotient_product ge_first_in_quotient_product ge_second_rp_quotient_product ge_second_rn_quotient_product ge_second_ip_quotient_product ge_second_in_quotient_product. ((exists ge_representation_real_code_quotient_productfirst ge_representation_imaginary_code_quotient_productfirst. (((d) = ((ge_representation_real_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst)) * S ((ge_representation_real_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst)) + ((ge_representation_imaginary_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst))) /\ ((exists ge_balance_positive_quotient_productfirstreal ge_balance_negative_quotient_productfirstreal. (((((ge_representation_real_code_quotient_productfirst) = 2 * (ge_balance_positive_quotient_productfirstreal) /\ (ge_balance_negative_quotient_productfirstreal) = 0) \/ exists ge_signed_half_quotient_productfirstrealdecode. (((ge_representation_real_code_quotient_productfirst) = 2 * ge_signed_half_quotient_productfirstrealdecode + 1 /\ (ge_balance_positive_quotient_productfirstreal) = 0) /\ (ge_balance_negative_quotient_productfirstreal) = S ge_signed_half_quotient_productfirstrealdecode))) /\ ((ge_first_rp_quotient_product) + ge_balance_negative_quotient_productfirstreal = (ge_first_rn_quotient_product) + ge_balance_positive_quotient_productfirstreal))) /\ (exists ge_balance_positive_quotient_productfirstimaginary ge_balance_negative_quotient_productfirstimaginary. (((((ge_representation_imaginary_code_quotient_productfirst) = 2 * (ge_balance_positive_quotient_productfirstimaginary) /\ (ge_balance_negative_quotient_productfirstimaginary) = 0) \/ exists ge_signed_half_quotient_productfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_productfirst) = 2 * ge_signed_half_quotient_productfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_productfirstimaginary) = 0) /\ (ge_balance_negative_quotient_productfirstimaginary) = S ge_signed_half_quotient_productfirstimaginarydecode))) /\ ((ge_first_ip_quotient_product) + ge_balance_negative_quotient_productfirstimaginary = (ge_first_in_quotient_product) + ge_balance_positive_quotient_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_productsecond ge_representation_imaginary_code_quotient_productsecond. (((q) = ((ge_representation_real_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond)) * S ((ge_representation_real_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond)) + ((ge_representation_imaginary_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond))) /\ ((exists ge_balance_positive_quotient_productsecondreal ge_balance_negative_quotient_productsecondreal. (((((ge_representation_real_code_quotient_productsecond) = 2 * (ge_balance_positive_quotient_productsecondreal) /\ (ge_balance_negative_quotient_productsecondreal) = 0) \/ exists ge_signed_half_quotient_productsecondrealdecode. (((ge_representation_real_code_quotient_productsecond) = 2 * ge_signed_half_quotient_productsecondrealdecode + 1 /\ (ge_balance_positive_quotient_productsecondreal) = 0) /\ (ge_balance_negative_quotient_productsecondreal) = S ge_signed_half_quotient_productsecondrealdecode))) /\ ((ge_second_rp_quotient_product) + ge_balance_negative_quotient_productsecondreal = (ge_second_rn_quotient_product) + ge_balance_positive_quotient_productsecondreal))) /\ (exists ge_balance_positive_quotient_productsecondimaginary ge_balance_negative_quotient_productsecondimaginary. (((((ge_representation_imaginary_code_quotient_productsecond) = 2 * (ge_balance_positive_quotient_productsecondimaginary) /\ (ge_balance_negative_quotient_productsecondimaginary) = 0) \/ exists ge_signed_half_quotient_productsecondimaginarydecode. (((ge_representation_imaginary_code_quotient_productsecond) = 2 * ge_signed_half_quotient_productsecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_productsecondimaginary) = 0) /\ (ge_balance_negative_quotient_productsecondimaginary) = S ge_signed_half_quotient_productsecondimaginarydecode))) /\ ((ge_second_ip_quotient_product) + ge_balance_negative_quotient_productsecondimaginary = (ge_second_in_quotient_product) + ge_balance_positive_quotient_productsecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_productoutput ge_representation_imaginary_code_quotient_productoutput. (((z) = ((ge_representation_real_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput)) * S ((ge_representation_real_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput)) + ((ge_representation_imaginary_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput))) /\ ((exists ge_balance_positive_quotient_productoutputreal ge_balance_negative_quotient_productoutputreal. (((((ge_representation_real_code_quotient_productoutput) = 2 * (ge_balance_positive_quotient_productoutputreal) /\ (ge_balance_negative_quotient_productoutputreal) = 0) \/ exists ge_signed_half_quotient_productoutputrealdecode. (((ge_representation_real_code_quotient_productoutput) = 2 * ge_signed_half_quotient_productoutputrealdecode + 1 /\ (ge_balance_positive_quotient_productoutputreal) = 0) /\ (ge_balance_negative_quotient_productoutputreal) = S ge_signed_half_quotient_productoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_product) * (ge_second_rp_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_rn_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_in_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_ip_quotient_product))))))) + ge_balance_negative_quotient_productoutputreal = (((((((ge_first_rp_quotient_product) * (ge_second_rn_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_rp_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_ip_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_in_quotient_product))))))) + ge_balance_positive_quotient_productoutputreal))) /\ (exists ge_balance_positive_quotient_productoutputimaginary ge_balance_negative_quotient_productoutputimaginary. (((((ge_representation_imaginary_code_quotient_productoutput) = 2 * (ge_balance_positive_quotient_productoutputimaginary) /\ (ge_balance_negative_quotient_productoutputimaginary) = 0) \/ exists ge_signed_half_quotient_productoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_productoutput) = 2 * ge_signed_half_quotient_productoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_productoutputimaginary) = 0) /\ (ge_balance_negative_quotient_productoutputimaginary) = S ge_signed_half_quotient_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_product) * (ge_second_ip_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_in_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_rp_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_rn_quotient_product))))))) + ge_balance_negative_quotient_productoutputimaginary = (((((((ge_first_rp_quotient_product) * (ge_second_in_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_ip_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_rn_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_rp_quotient_product))))))) + ge_balance_positive_quotient_productoutputimaginary))))))))) /\ ((exists ge_norm_rp_quotient_norm ge_norm_rn_quotient_norm ge_norm_ip_quotient_norm ge_norm_in_quotient_norm. ((exists ge_representation_real_code_quotient_normrepresentation ge_representation_imaginary_code_quotient_normrepresentation. (((q) = ((ge_representation_real_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation)) * S ((ge_representation_real_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation)) + ((ge_representation_imaginary_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation))) /\ ((exists ge_balance_positive_quotient_normrepresentationreal ge_balance_negative_quotient_normrepresentationreal. (((((ge_representation_real_code_quotient_normrepresentation) = 2 * (ge_balance_positive_quotient_normrepresentationreal) /\ (ge_balance_negative_quotient_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_normrepresentationrealdecode. (((ge_representation_real_code_quotient_normrepresentation) = 2 * ge_signed_half_quotient_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_normrepresentationreal) = S ge_signed_half_quotient_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_norm) + ge_balance_negative_quotient_normrepresentationreal = (ge_norm_rn_quotient_norm) + ge_balance_positive_quotient_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_normrepresentationimaginary ge_balance_negative_quotient_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_normrepresentation) = 2 * (ge_balance_positive_quotient_normrepresentationimaginary) /\ (ge_balance_negative_quotient_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_normrepresentation) = 2 * ge_signed_half_quotient_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_normrepresentationimaginary) = S ge_signed_half_quotient_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_norm) + ge_balance_negative_quotient_normrepresentationimaginary = (ge_norm_in_quotient_norm) + ge_balance_positive_quotient_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_normsquare ge_imaginary_square_quotient_normsquare. ((((((ge_norm_rp_quotient_norm) * (ge_norm_rp_quotient_norm))) + (((ge_norm_rn_quotient_norm) * (ge_norm_rn_quotient_norm)))) = ((ge_real_square_quotient_normsquare) + (((((ge_norm_rp_quotient_norm) * (ge_norm_rn_quotient_norm))) + (((ge_norm_rn_quotient_norm) * (ge_norm_rp_quotient_norm))))))) /\ ((((((ge_norm_ip_quotient_norm) * (ge_norm_ip_quotient_norm))) + (((ge_norm_in_quotient_norm) * (ge_norm_in_quotient_norm)))) = ((ge_imaginary_square_quotient_normsquare) + (((((ge_norm_ip_quotient_norm) * (ge_norm_in_quotient_norm))) + (((ge_norm_in_quotient_norm) * (ge_norm_ip_quotient_norm))))))) /\ ((Q) = ge_real_square_quotient_normsquare + ge_imaginary_square_quotient_normsquare)))))) /\ ((exists ge_gap_quotient_strict. ge_gap_quotient_strict + S (Q) = (N)) /\ (~(q=0)))))