gaussian_nonunit_factor_is_proper_norm_divisor

Exact expanded first-order arithmetic statement

forall z N a b. (exists ge_norm_rp_factor_target_norm ge_norm_rn_factor_target_norm ge_norm_ip_factor_target_norm ge_norm_in_factor_target_norm. ((exists ge_representation_real_code_factor_target_normrepresentation ge_representation_imaginary_code_factor_target_normrepresentation. (((z) = ((ge_representation_real_code_factor_target_normrepresentation) + (ge_representation_imaginary_code_factor_target_normrepresentation)) * S ((ge_representation_real_code_factor_target_normrepresentation) + (ge_representation_imaginary_code_factor_target_normrepresentation)) + ((ge_representation_imaginary_code_factor_target_normrepresentation) + (ge_representation_imaginary_code_factor_target_normrepresentation))) /\ ((exists ge_balance_positive_factor_target_normrepresentationreal ge_balance_negative_factor_target_normrepresentationreal. (((((ge_representation_real_code_factor_target_normrepresentation) = 2 * (ge_balance_positive_factor_target_normrepresentationreal) /\ (ge_balance_negative_factor_target_normrepresentationreal) = 0) \/ exists ge_signed_half_factor_target_normrepresentationrealdecode. (((ge_representation_real_code_factor_target_normrepresentation) = 2 * ge_signed_half_factor_target_normrepresentationrealdecode + 1 /\ (ge_balance_positive_factor_target_normrepresentationreal) = 0) /\ (ge_balance_negative_factor_target_normrepresentationreal) = S ge_signed_half_factor_target_normrepresentationrealdecode))) /\ ((ge_norm_rp_factor_target_norm) + ge_balance_negative_factor_target_normrepresentationreal = (ge_norm_rn_factor_target_norm) + ge_balance_positive_factor_target_normrepresentationreal))) /\ (exists ge_balance_positive_factor_target_normrepresentationimaginary ge_balance_negative_factor_target_normrepresentationimaginary. (((((ge_representation_imaginary_code_factor_target_normrepresentation) = 2 * (ge_balance_positive_factor_target_normrepresentationimaginary) /\ (ge_balance_negative_factor_target_normrepresentationimaginary) = 0) \/ exists ge_signed_half_factor_target_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_factor_target_normrepresentation) = 2 * ge_signed_half_factor_target_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_factor_target_normrepresentationimaginary) = 0) /\ (ge_balance_negative_factor_target_normrepresentationimaginary) = S ge_signed_half_factor_target_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_factor_target_norm) + ge_balance_negative_factor_target_normrepresentationimaginary = (ge_norm_in_factor_target_norm) + ge_balance_positive_factor_target_normrepresentationimaginary)))))) /\ (exists ge_real_square_factor_target_normsquare ge_imaginary_square_factor_target_normsquare. ((((((ge_norm_rp_factor_target_norm) * (ge_norm_rp_factor_target_norm))) + (((ge_norm_rn_factor_target_norm) * (ge_norm_rn_factor_target_norm)))) = ((ge_real_square_factor_target_normsquare) + (((((ge_norm_rp_factor_target_norm) * (ge_norm_rn_factor_target_norm))) + (((ge_norm_rn_factor_target_norm) * (ge_norm_rp_factor_target_norm))))))) /\ ((((((ge_norm_ip_factor_target_norm) * (ge_norm_ip_factor_target_norm))) + (((ge_norm_in_factor_target_norm) * (ge_norm_in_factor_target_norm)))) = ((ge_imaginary_square_factor_target_normsquare) + (((((ge_norm_ip_factor_target_norm) * (ge_norm_in_factor_target_norm))) + (((ge_norm_in_factor_target_norm) * (ge_norm_ip_factor_target_norm))))))) /\ ((N) = ge_real_square_factor_target_normsquare + ge_imaginary_square_factor_target_normsquare)))))) -> (exists ge_first_rp_factor_actual_product ge_first_rn_factor_actual_product ge_first_ip_factor_actual_product ge_first_in_factor_actual_product ge_second_rp_factor_actual_product ge_second_rn_factor_actual_product ge_second_ip_factor_actual_product ge_second_in_factor_actual_product. ((exists ge_representation_real_code_factor_actual_productfirst ge_representation_imaginary_code_factor_actual_productfirst. (((a) = ((ge_representation_real_code_factor_actual_productfirst) + (ge_representation_imaginary_code_factor_actual_productfirst)) * S ((ge_representation_real_code_factor_actual_productfirst) + (ge_representation_imaginary_code_factor_actual_productfirst)) + ((ge_representation_imaginary_code_factor_actual_productfirst) + (ge_representation_imaginary_code_factor_actual_productfirst))) /\ ((exists ge_balance_positive_factor_actual_productfirstreal ge_balance_negative_factor_actual_productfirstreal. (((((ge_representation_real_code_factor_actual_productfirst) = 2 * (ge_balance_positive_factor_actual_productfirstreal) /\ (ge_balance_negative_factor_actual_productfirstreal) = 0) \/ exists ge_signed_half_factor_actual_productfirstrealdecode. (((ge_representation_real_code_factor_actual_productfirst) = 2 * ge_signed_half_factor_actual_productfirstrealdecode + 1 /\ (ge_balance_positive_factor_actual_productfirstreal) = 0) /\ (ge_balance_negative_factor_actual_productfirstreal) = S ge_signed_half_factor_actual_productfirstrealdecode))) /\ ((ge_first_rp_factor_actual_product) + ge_balance_negative_factor_actual_productfirstreal = (ge_first_rn_factor_actual_product) + ge_balance_positive_factor_actual_productfirstreal))) /\ (exists ge_balance_positive_factor_actual_productfirstimaginary ge_balance_negative_factor_actual_productfirstimaginary. (((((ge_representation_imaginary_code_factor_actual_productfirst) = 2 * (ge_balance_positive_factor_actual_productfirstimaginary) /\ (ge_balance_negative_factor_actual_productfirstimaginary) = 0) \/ exists ge_signed_half_factor_actual_productfirstimaginarydecode. (((ge_representation_imaginary_code_factor_actual_productfirst) = 2 * ge_signed_half_factor_actual_productfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_actual_productfirstimaginary) = 0) /\ (ge_balance_negative_factor_actual_productfirstimaginary) = S ge_signed_half_factor_actual_productfirstimaginarydecode))) /\ ((ge_first_ip_factor_actual_product) + ge_balance_negative_factor_actual_productfirstimaginary = (ge_first_in_factor_actual_product) + ge_balance_positive_factor_actual_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_actual_productsecond ge_representation_imaginary_code_factor_actual_productsecond. (((b) = ((ge_representation_real_code_factor_actual_productsecond) + (ge_representation_imaginary_code_factor_actual_productsecond)) * S ((ge_representation_real_code_factor_actual_productsecond) + (ge_representation_imaginary_code_factor_actual_productsecond)) + ((ge_representation_imaginary_code_factor_actual_productsecond) + (ge_representation_imaginary_code_factor_actual_productsecond))) /\ ((exists ge_balance_positive_factor_actual_productsecondreal ge_balance_negative_factor_actual_productsecondreal. (((((ge_representation_real_code_factor_actual_productsecond) = 2 * (ge_balance_positive_factor_actual_productsecondreal) /\ (ge_balance_negative_factor_actual_productsecondreal) = 0) \/ exists ge_signed_half_factor_actual_productsecondrealdecode. (((ge_representation_real_code_factor_actual_productsecond) = 2 * ge_signed_half_factor_actual_productsecondrealdecode + 1 /\ (ge_balance_positive_factor_actual_productsecondreal) = 0) /\ (ge_balance_negative_factor_actual_productsecondreal) = S ge_signed_half_factor_actual_productsecondrealdecode))) /\ ((ge_second_rp_factor_actual_product) + ge_balance_negative_factor_actual_productsecondreal = (ge_second_rn_factor_actual_product) + ge_balance_positive_factor_actual_productsecondreal))) /\ (exists ge_balance_positive_factor_actual_productsecondimaginary ge_balance_negative_factor_actual_productsecondimaginary. (((((ge_representation_imaginary_code_factor_actual_productsecond) = 2 * (ge_balance_positive_factor_actual_productsecondimaginary) /\ (ge_balance_negative_factor_actual_productsecondimaginary) = 0) \/ exists ge_signed_half_factor_actual_productsecondimaginarydecode. (((ge_representation_imaginary_code_factor_actual_productsecond) = 2 * ge_signed_half_factor_actual_productsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_actual_productsecondimaginary) = 0) /\ (ge_balance_negative_factor_actual_productsecondimaginary) = S ge_signed_half_factor_actual_productsecondimaginarydecode))) /\ ((ge_second_ip_factor_actual_product) + ge_balance_negative_factor_actual_productsecondimaginary = (ge_second_in_factor_actual_product) + ge_balance_positive_factor_actual_productsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_actual_productoutput ge_representation_imaginary_code_factor_actual_productoutput. (((z) = ((ge_representation_real_code_factor_actual_productoutput) + (ge_representation_imaginary_code_factor_actual_productoutput)) * S ((ge_representation_real_code_factor_actual_productoutput) + (ge_representation_imaginary_code_factor_actual_productoutput)) + ((ge_representation_imaginary_code_factor_actual_productoutput) + (ge_representation_imaginary_code_factor_actual_productoutput))) /\ ((exists ge_balance_positive_factor_actual_productoutputreal ge_balance_negative_factor_actual_productoutputreal. (((((ge_representation_real_code_factor_actual_productoutput) = 2 * (ge_balance_positive_factor_actual_productoutputreal) /\ (ge_balance_negative_factor_actual_productoutputreal) = 0) \/ exists ge_signed_half_factor_actual_productoutputrealdecode. (((ge_representation_real_code_factor_actual_productoutput) = 2 * ge_signed_half_factor_actual_productoutputrealdecode + 1 /\ (ge_balance_positive_factor_actual_productoutputreal) = 0) /\ (ge_balance_negative_factor_actual_productoutputreal) = S ge_signed_half_factor_actual_productoutputrealdecode))) /\ ((((((((ge_first_rp_factor_actual_product) * (ge_second_rp_factor_actual_product))) + (((ge_first_rn_factor_actual_product) * (ge_second_rn_factor_actual_product))))) + (((((ge_first_ip_factor_actual_product) * (ge_second_in_factor_actual_product))) + (((ge_first_in_factor_actual_product) * (ge_second_ip_factor_actual_product))))))) + ge_balance_negative_factor_actual_productoutputreal = (((((((ge_first_rp_factor_actual_product) * (ge_second_rn_factor_actual_product))) + (((ge_first_rn_factor_actual_product) * (ge_second_rp_factor_actual_product))))) + (((((ge_first_ip_factor_actual_product) * (ge_second_ip_factor_actual_product))) + (((ge_first_in_factor_actual_product) * (ge_second_in_factor_actual_product))))))) + ge_balance_positive_factor_actual_productoutputreal))) /\ (exists ge_balance_positive_factor_actual_productoutputimaginary ge_balance_negative_factor_actual_productoutputimaginary. (((((ge_representation_imaginary_code_factor_actual_productoutput) = 2 * (ge_balance_positive_factor_actual_productoutputimaginary) /\ (ge_balance_negative_factor_actual_productoutputimaginary) = 0) \/ exists ge_signed_half_factor_actual_productoutputimaginarydecode. (((ge_representation_imaginary_code_factor_actual_productoutput) = 2 * ge_signed_half_factor_actual_productoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_actual_productoutputimaginary) = 0) /\ (ge_balance_negative_factor_actual_productoutputimaginary) = S ge_signed_half_factor_actual_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_actual_product) * (ge_second_ip_factor_actual_product))) + (((ge_first_rn_factor_actual_product) * (ge_second_in_factor_actual_product))))) + (((((ge_first_ip_factor_actual_product) * (ge_second_rp_factor_actual_product))) + (((ge_first_in_factor_actual_product) * (ge_second_rn_factor_actual_product))))))) + ge_balance_negative_factor_actual_productoutputimaginary = (((((((ge_first_rp_factor_actual_product) * (ge_second_in_factor_actual_product))) + (((ge_first_rn_factor_actual_product) * (ge_second_ip_factor_actual_product))))) + (((((ge_first_ip_factor_actual_product) * (ge_second_rn_factor_actual_product))) + (((ge_first_in_factor_actual_product) * (ge_second_rp_factor_actual_product))))))) + ge_balance_positive_factor_actual_productoutputimaginary))))))))) -> ~(z=0) -> ~(exists gr_inverse_factor_first_nonunit. (exists ge_first_rp_factor_first_nonunitidentity ge_first_rn_factor_first_nonunitidentity ge_first_ip_factor_first_nonunitidentity ge_first_in_factor_first_nonunitidentity ge_second_rp_factor_first_nonunitidentity ge_second_rn_factor_first_nonunitidentity ge_second_ip_factor_first_nonunitidentity ge_second_in_factor_first_nonunitidentity. ((exists ge_representation_real_code_factor_first_nonunitidentityfirst ge_representation_imaginary_code_factor_first_nonunitidentityfirst. (((a) = ((ge_representation_real_code_factor_first_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_first_nonunitidentityfirst)) * S ((ge_representation_real_code_factor_first_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_first_nonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_first_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_first_nonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_first_nonunitidentityfirstreal ge_balance_negative_factor_first_nonunitidentityfirstreal. (((((ge_representation_real_code_factor_first_nonunitidentityfirst) = 2 * (ge_balance_positive_factor_first_nonunitidentityfirstreal) /\ (ge_balance_negative_factor_first_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_first_nonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_first_nonunitidentityfirst) = 2 * ge_signed_half_factor_first_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_first_nonunitidentityfirstreal) = S ge_signed_half_factor_first_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_first_nonunitidentity) + ge_balance_negative_factor_first_nonunitidentityfirstreal = (ge_first_rn_factor_first_nonunitidentity) + ge_balance_positive_factor_first_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_first_nonunitidentityfirstimaginary ge_balance_negative_factor_first_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_first_nonunitidentityfirst) = 2 * (ge_balance_positive_factor_first_nonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_first_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_first_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_first_nonunitidentityfirst) = 2 * ge_signed_half_factor_first_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_first_nonunitidentityfirstimaginary) = S ge_signed_half_factor_first_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_first_nonunitidentity) + ge_balance_negative_factor_first_nonunitidentityfirstimaginary = (ge_first_in_factor_first_nonunitidentity) + ge_balance_positive_factor_first_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_first_nonunitidentitysecond ge_representation_imaginary_code_factor_first_nonunitidentitysecond. (((gr_inverse_factor_first_nonunit) = ((ge_representation_real_code_factor_first_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_first_nonunitidentitysecond)) * S ((ge_representation_real_code_factor_first_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_first_nonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_first_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_first_nonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_first_nonunitidentitysecondreal ge_balance_negative_factor_first_nonunitidentitysecondreal. (((((ge_representation_real_code_factor_first_nonunitidentitysecond) = 2 * (ge_balance_positive_factor_first_nonunitidentitysecondreal) /\ (ge_balance_negative_factor_first_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_first_nonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_first_nonunitidentitysecond) = 2 * ge_signed_half_factor_first_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_first_nonunitidentitysecondreal) = S ge_signed_half_factor_first_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_first_nonunitidentity) + ge_balance_negative_factor_first_nonunitidentitysecondreal = (ge_second_rn_factor_first_nonunitidentity) + ge_balance_positive_factor_first_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_first_nonunitidentitysecondimaginary ge_balance_negative_factor_first_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_first_nonunitidentitysecond) = 2 * (ge_balance_positive_factor_first_nonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_first_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_first_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_first_nonunitidentitysecond) = 2 * ge_signed_half_factor_first_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_first_nonunitidentitysecondimaginary) = S ge_signed_half_factor_first_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_first_nonunitidentity) + ge_balance_negative_factor_first_nonunitidentitysecondimaginary = (ge_second_in_factor_first_nonunitidentity) + ge_balance_positive_factor_first_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_first_nonunitidentityoutput ge_representation_imaginary_code_factor_first_nonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_first_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_first_nonunitidentityoutput)) * S ((ge_representation_real_code_factor_first_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_first_nonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_first_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_first_nonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_first_nonunitidentityoutputreal ge_balance_negative_factor_first_nonunitidentityoutputreal. (((((ge_representation_real_code_factor_first_nonunitidentityoutput) = 2 * (ge_balance_positive_factor_first_nonunitidentityoutputreal) /\ (ge_balance_negative_factor_first_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_first_nonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_first_nonunitidentityoutput) = 2 * ge_signed_half_factor_first_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_first_nonunitidentityoutputreal) = S ge_signed_half_factor_first_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_first_nonunitidentity) * (ge_second_rp_factor_first_nonunitidentity))) + (((ge_first_rn_factor_first_nonunitidentity) * (ge_second_rn_factor_first_nonunitidentity))))) + (((((ge_first_ip_factor_first_nonunitidentity) * (ge_second_in_factor_first_nonunitidentity))) + (((ge_first_in_factor_first_nonunitidentity) * (ge_second_ip_factor_first_nonunitidentity))))))) + ge_balance_negative_factor_first_nonunitidentityoutputreal = (((((((ge_first_rp_factor_first_nonunitidentity) * (ge_second_rn_factor_first_nonunitidentity))) + (((ge_first_rn_factor_first_nonunitidentity) * (ge_second_rp_factor_first_nonunitidentity))))) + (((((ge_first_ip_factor_first_nonunitidentity) * (ge_second_ip_factor_first_nonunitidentity))) + (((ge_first_in_factor_first_nonunitidentity) * (ge_second_in_factor_first_nonunitidentity))))))) + ge_balance_positive_factor_first_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_first_nonunitidentityoutputimaginary ge_balance_negative_factor_first_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_first_nonunitidentityoutput) = 2 * (ge_balance_positive_factor_first_nonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_first_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_first_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_first_nonunitidentityoutput) = 2 * ge_signed_half_factor_first_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_first_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_first_nonunitidentityoutputimaginary) = S ge_signed_half_factor_first_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_first_nonunitidentity) * (ge_second_ip_factor_first_nonunitidentity))) + (((ge_first_rn_factor_first_nonunitidentity) * (ge_second_in_factor_first_nonunitidentity))))) + (((((ge_first_ip_factor_first_nonunitidentity) * (ge_second_rp_factor_first_nonunitidentity))) + (((ge_first_in_factor_first_nonunitidentity) * (ge_second_rn_factor_first_nonunitidentity))))))) + ge_balance_negative_factor_first_nonunitidentityoutputimaginary = (((((((ge_first_rp_factor_first_nonunitidentity) * (ge_second_in_factor_first_nonunitidentity))) + (((ge_first_rn_factor_first_nonunitidentity) * (ge_second_ip_factor_first_nonunitidentity))))) + (((((ge_first_ip_factor_first_nonunitidentity) * (ge_second_rn_factor_first_nonunitidentity))) + (((ge_first_in_factor_first_nonunitidentity) * (ge_second_rp_factor_first_nonunitidentity))))))) + ge_balance_positive_factor_first_nonunitidentityoutputimaginary)))))))))) -> ~(exists gr_inverse_factor_second_nonunit. (exists ge_first_rp_factor_second_nonunitidentity ge_first_rn_factor_second_nonunitidentity ge_first_ip_factor_second_nonunitidentity ge_first_in_factor_second_nonunitidentity ge_second_rp_factor_second_nonunitidentity ge_second_rn_factor_second_nonunitidentity ge_second_ip_factor_second_nonunitidentity ge_second_in_factor_second_nonunitidentity. ((exists ge_representation_real_code_factor_second_nonunitidentityfirst ge_representation_imaginary_code_factor_second_nonunitidentityfirst. (((b) = ((ge_representation_real_code_factor_second_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_second_nonunitidentityfirst)) * S ((ge_representation_real_code_factor_second_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_second_nonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_second_nonunitidentityfirst) + (ge_representation_imaginary_code_factor_second_nonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_second_nonunitidentityfirstreal ge_balance_negative_factor_second_nonunitidentityfirstreal. (((((ge_representation_real_code_factor_second_nonunitidentityfirst) = 2 * (ge_balance_positive_factor_second_nonunitidentityfirstreal) /\ (ge_balance_negative_factor_second_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_second_nonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_second_nonunitidentityfirst) = 2 * ge_signed_half_factor_second_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_second_nonunitidentityfirstreal) = S ge_signed_half_factor_second_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_second_nonunitidentity) + ge_balance_negative_factor_second_nonunitidentityfirstreal = (ge_first_rn_factor_second_nonunitidentity) + ge_balance_positive_factor_second_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_second_nonunitidentityfirstimaginary ge_balance_negative_factor_second_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_second_nonunitidentityfirst) = 2 * (ge_balance_positive_factor_second_nonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_second_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_second_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_second_nonunitidentityfirst) = 2 * ge_signed_half_factor_second_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_second_nonunitidentityfirstimaginary) = S ge_signed_half_factor_second_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_second_nonunitidentity) + ge_balance_negative_factor_second_nonunitidentityfirstimaginary = (ge_first_in_factor_second_nonunitidentity) + ge_balance_positive_factor_second_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_second_nonunitidentitysecond ge_representation_imaginary_code_factor_second_nonunitidentitysecond. (((gr_inverse_factor_second_nonunit) = ((ge_representation_real_code_factor_second_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_second_nonunitidentitysecond)) * S ((ge_representation_real_code_factor_second_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_second_nonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_second_nonunitidentitysecond) + (ge_representation_imaginary_code_factor_second_nonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_second_nonunitidentitysecondreal ge_balance_negative_factor_second_nonunitidentitysecondreal. (((((ge_representation_real_code_factor_second_nonunitidentitysecond) = 2 * (ge_balance_positive_factor_second_nonunitidentitysecondreal) /\ (ge_balance_negative_factor_second_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_second_nonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_second_nonunitidentitysecond) = 2 * ge_signed_half_factor_second_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_second_nonunitidentitysecondreal) = S ge_signed_half_factor_second_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_second_nonunitidentity) + ge_balance_negative_factor_second_nonunitidentitysecondreal = (ge_second_rn_factor_second_nonunitidentity) + ge_balance_positive_factor_second_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_second_nonunitidentitysecondimaginary ge_balance_negative_factor_second_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_second_nonunitidentitysecond) = 2 * (ge_balance_positive_factor_second_nonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_second_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_second_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_second_nonunitidentitysecond) = 2 * ge_signed_half_factor_second_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_second_nonunitidentitysecondimaginary) = S ge_signed_half_factor_second_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_second_nonunitidentity) + ge_balance_negative_factor_second_nonunitidentitysecondimaginary = (ge_second_in_factor_second_nonunitidentity) + ge_balance_positive_factor_second_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_second_nonunitidentityoutput ge_representation_imaginary_code_factor_second_nonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_second_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_second_nonunitidentityoutput)) * S ((ge_representation_real_code_factor_second_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_second_nonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_second_nonunitidentityoutput) + (ge_representation_imaginary_code_factor_second_nonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_second_nonunitidentityoutputreal ge_balance_negative_factor_second_nonunitidentityoutputreal. (((((ge_representation_real_code_factor_second_nonunitidentityoutput) = 2 * (ge_balance_positive_factor_second_nonunitidentityoutputreal) /\ (ge_balance_negative_factor_second_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_second_nonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_second_nonunitidentityoutput) = 2 * ge_signed_half_factor_second_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_second_nonunitidentityoutputreal) = S ge_signed_half_factor_second_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_second_nonunitidentity) * (ge_second_rp_factor_second_nonunitidentity))) + (((ge_first_rn_factor_second_nonunitidentity) * (ge_second_rn_factor_second_nonunitidentity))))) + (((((ge_first_ip_factor_second_nonunitidentity) * (ge_second_in_factor_second_nonunitidentity))) + (((ge_first_in_factor_second_nonunitidentity) * (ge_second_ip_factor_second_nonunitidentity))))))) + ge_balance_negative_factor_second_nonunitidentityoutputreal = (((((((ge_first_rp_factor_second_nonunitidentity) * (ge_second_rn_factor_second_nonunitidentity))) + (((ge_first_rn_factor_second_nonunitidentity) * (ge_second_rp_factor_second_nonunitidentity))))) + (((((ge_first_ip_factor_second_nonunitidentity) * (ge_second_ip_factor_second_nonunitidentity))) + (((ge_first_in_factor_second_nonunitidentity) * (ge_second_in_factor_second_nonunitidentity))))))) + ge_balance_positive_factor_second_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_second_nonunitidentityoutputimaginary ge_balance_negative_factor_second_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_second_nonunitidentityoutput) = 2 * (ge_balance_positive_factor_second_nonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_second_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_second_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_second_nonunitidentityoutput) = 2 * ge_signed_half_factor_second_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_second_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_second_nonunitidentityoutputimaginary) = S ge_signed_half_factor_second_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_second_nonunitidentity) * (ge_second_ip_factor_second_nonunitidentity))) + (((ge_first_rn_factor_second_nonunitidentity) * (ge_second_in_factor_second_nonunitidentity))))) + (((((ge_first_ip_factor_second_nonunitidentity) * (ge_second_rp_factor_second_nonunitidentity))) + (((ge_first_in_factor_second_nonunitidentity) * (ge_second_rn_factor_second_nonunitidentity))))))) + ge_balance_negative_factor_second_nonunitidentityoutputimaginary = (((((((ge_first_rp_factor_second_nonunitidentity) * (ge_second_in_factor_second_nonunitidentity))) + (((ge_first_rn_factor_second_nonunitidentity) * (ge_second_ip_factor_second_nonunitidentity))))) + (((((ge_first_ip_factor_second_nonunitidentity) * (ge_second_rn_factor_second_nonunitidentity))) + (((ge_first_in_factor_second_nonunitidentity) * (ge_second_rp_factor_second_nonunitidentity))))))) + ge_balance_positive_factor_second_nonunitidentityoutputimaginary)))))))))) -> (((~(exists gr_inverse_factor_proper_divisornonunit. (exists ge_first_rp_factor_proper_divisornonunitidentity ge_first_rn_factor_proper_divisornonunitidentity ge_first_ip_factor_proper_divisornonunitidentity ge_first_in_factor_proper_divisornonunitidentity ge_second_rp_factor_proper_divisornonunitidentity ge_second_rn_factor_proper_divisornonunitidentity ge_second_ip_factor_proper_divisornonunitidentity ge_second_in_factor_proper_divisornonunitidentity. ((exists ge_representation_real_code_factor_proper_divisornonunitidentityfirst ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst. (((a) = ((ge_representation_real_code_factor_proper_divisornonunitidentityfirst) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst)) * S ((ge_representation_real_code_factor_proper_divisornonunitidentityfirst) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_proper_divisornonunitidentityfirstreal ge_balance_negative_factor_proper_divisornonunitidentityfirstreal. (((((ge_representation_real_code_factor_proper_divisornonunitidentityfirst) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentityfirstreal) /\ (ge_balance_negative_factor_proper_divisornonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_proper_divisornonunitidentityfirst) = 2 * ge_signed_half_factor_proper_divisornonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentityfirstreal) = S ge_signed_half_factor_proper_divisornonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_proper_divisornonunitidentity) + ge_balance_negative_factor_proper_divisornonunitidentityfirstreal = (ge_first_rn_factor_proper_divisornonunitidentity) + ge_balance_positive_factor_proper_divisornonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_proper_divisornonunitidentityfirstimaginary ge_balance_negative_factor_proper_divisornonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_proper_divisornonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisornonunitidentityfirst) = 2 * ge_signed_half_factor_proper_divisornonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentityfirstimaginary) = S ge_signed_half_factor_proper_divisornonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_proper_divisornonunitidentity) + ge_balance_negative_factor_proper_divisornonunitidentityfirstimaginary = (ge_first_in_factor_proper_divisornonunitidentity) + ge_balance_positive_factor_proper_divisornonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_proper_divisornonunitidentitysecond ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond. (((gr_inverse_factor_proper_divisornonunit) = ((ge_representation_real_code_factor_proper_divisornonunitidentitysecond) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond)) * S ((ge_representation_real_code_factor_proper_divisornonunitidentitysecond) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_proper_divisornonunitidentitysecondreal ge_balance_negative_factor_proper_divisornonunitidentitysecondreal. (((((ge_representation_real_code_factor_proper_divisornonunitidentitysecond) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentitysecondreal) /\ (ge_balance_negative_factor_proper_divisornonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_proper_divisornonunitidentitysecond) = 2 * ge_signed_half_factor_proper_divisornonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentitysecondreal) = S ge_signed_half_factor_proper_divisornonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_proper_divisornonunitidentity) + ge_balance_negative_factor_proper_divisornonunitidentitysecondreal = (ge_second_rn_factor_proper_divisornonunitidentity) + ge_balance_positive_factor_proper_divisornonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_proper_divisornonunitidentitysecondimaginary ge_balance_negative_factor_proper_divisornonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_proper_divisornonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisornonunitidentitysecond) = 2 * ge_signed_half_factor_proper_divisornonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentitysecondimaginary) = S ge_signed_half_factor_proper_divisornonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_proper_divisornonunitidentity) + ge_balance_negative_factor_proper_divisornonunitidentitysecondimaginary = (ge_second_in_factor_proper_divisornonunitidentity) + ge_balance_positive_factor_proper_divisornonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_proper_divisornonunitidentityoutput ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_proper_divisornonunitidentityoutput) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput)) * S ((ge_representation_real_code_factor_proper_divisornonunitidentityoutput) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput) + (ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_proper_divisornonunitidentityoutputreal ge_balance_negative_factor_proper_divisornonunitidentityoutputreal. (((((ge_representation_real_code_factor_proper_divisornonunitidentityoutput) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentityoutputreal) /\ (ge_balance_negative_factor_proper_divisornonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_proper_divisornonunitidentityoutput) = 2 * ge_signed_half_factor_proper_divisornonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentityoutputreal) = S ge_signed_half_factor_proper_divisornonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_proper_divisornonunitidentity) * (ge_second_rp_factor_proper_divisornonunitidentity))) + (((ge_first_rn_factor_proper_divisornonunitidentity) * (ge_second_rn_factor_proper_divisornonunitidentity))))) + (((((ge_first_ip_factor_proper_divisornonunitidentity) * (ge_second_in_factor_proper_divisornonunitidentity))) + (((ge_first_in_factor_proper_divisornonunitidentity) * (ge_second_ip_factor_proper_divisornonunitidentity))))))) + ge_balance_negative_factor_proper_divisornonunitidentityoutputreal = (((((((ge_first_rp_factor_proper_divisornonunitidentity) * (ge_second_rn_factor_proper_divisornonunitidentity))) + (((ge_first_rn_factor_proper_divisornonunitidentity) * (ge_second_rp_factor_proper_divisornonunitidentity))))) + (((((ge_first_ip_factor_proper_divisornonunitidentity) * (ge_second_ip_factor_proper_divisornonunitidentity))) + (((ge_first_in_factor_proper_divisornonunitidentity) * (ge_second_in_factor_proper_divisornonunitidentity))))))) + ge_balance_positive_factor_proper_divisornonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_proper_divisornonunitidentityoutputimaginary ge_balance_negative_factor_proper_divisornonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput) = 2 * (ge_balance_positive_factor_proper_divisornonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_proper_divisornonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisornonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisornonunitidentityoutput) = 2 * ge_signed_half_factor_proper_divisornonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisornonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisornonunitidentityoutputimaginary) = S ge_signed_half_factor_proper_divisornonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_proper_divisornonunitidentity) * (ge_second_ip_factor_proper_divisornonunitidentity))) + (((ge_first_rn_factor_proper_divisornonunitidentity) * (ge_second_in_factor_proper_divisornonunitidentity))))) + (((((ge_first_ip_factor_proper_divisornonunitidentity) * (ge_second_rp_factor_proper_divisornonunitidentity))) + (((ge_first_in_factor_proper_divisornonunitidentity) * (ge_second_rn_factor_proper_divisornonunitidentity))))))) + ge_balance_negative_factor_proper_divisornonunitidentityoutputimaginary = (((((((ge_first_rp_factor_proper_divisornonunitidentity) * (ge_second_in_factor_proper_divisornonunitidentity))) + (((ge_first_rn_factor_proper_divisornonunitidentity) * (ge_second_ip_factor_proper_divisornonunitidentity))))) + (((((ge_first_ip_factor_proper_divisornonunitidentity) * (ge_second_rn_factor_proper_divisornonunitidentity))) + (((ge_first_in_factor_proper_divisornonunitidentity) * (ge_second_rp_factor_proper_divisornonunitidentity))))))) + ge_balance_positive_factor_proper_divisornonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_factor_proper_divisorquotient. (exists ge_first_rp_factor_proper_divisorquotientproduct ge_first_rn_factor_proper_divisorquotientproduct ge_first_ip_factor_proper_divisorquotientproduct ge_first_in_factor_proper_divisorquotientproduct ge_second_rp_factor_proper_divisorquotientproduct ge_second_rn_factor_proper_divisorquotientproduct ge_second_ip_factor_proper_divisorquotientproduct ge_second_in_factor_proper_divisorquotientproduct. ((exists ge_representation_real_code_factor_proper_divisorquotientproductfirst ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst. (((a) = ((ge_representation_real_code_factor_proper_divisorquotientproductfirst) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst)) * S ((ge_representation_real_code_factor_proper_divisorquotientproductfirst) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst)) + ((ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst))) /\ ((exists ge_balance_positive_factor_proper_divisorquotientproductfirstreal ge_balance_negative_factor_proper_divisorquotientproductfirstreal. (((((ge_representation_real_code_factor_proper_divisorquotientproductfirst) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductfirstreal) /\ (ge_balance_negative_factor_proper_divisorquotientproductfirstreal) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductfirstrealdecode. (((ge_representation_real_code_factor_proper_divisorquotientproductfirst) = 2 * ge_signed_half_factor_proper_divisorquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductfirstreal) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductfirstreal) = S ge_signed_half_factor_proper_divisorquotientproductfirstrealdecode))) /\ ((ge_first_rp_factor_proper_divisorquotientproduct) + ge_balance_negative_factor_proper_divisorquotientproductfirstreal = (ge_first_rn_factor_proper_divisorquotientproduct) + ge_balance_positive_factor_proper_divisorquotientproductfirstreal))) /\ (exists ge_balance_positive_factor_proper_divisorquotientproductfirstimaginary ge_balance_negative_factor_proper_divisorquotientproductfirstimaginary. (((((ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductfirstimaginary) /\ (ge_balance_negative_factor_proper_divisorquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisorquotientproductfirst) = 2 * ge_signed_half_factor_proper_divisorquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductfirstimaginary) = S ge_signed_half_factor_proper_divisorquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_factor_proper_divisorquotientproduct) + ge_balance_negative_factor_proper_divisorquotientproductfirstimaginary = (ge_first_in_factor_proper_divisorquotientproduct) + ge_balance_positive_factor_proper_divisorquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_proper_divisorquotientproductsecond ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond. (((gr_quotient_factor_proper_divisorquotient) = ((ge_representation_real_code_factor_proper_divisorquotientproductsecond) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond)) * S ((ge_representation_real_code_factor_proper_divisorquotientproductsecond) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond)) + ((ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond))) /\ ((exists ge_balance_positive_factor_proper_divisorquotientproductsecondreal ge_balance_negative_factor_proper_divisorquotientproductsecondreal. (((((ge_representation_real_code_factor_proper_divisorquotientproductsecond) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductsecondreal) /\ (ge_balance_negative_factor_proper_divisorquotientproductsecondreal) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductsecondrealdecode. (((ge_representation_real_code_factor_proper_divisorquotientproductsecond) = 2 * ge_signed_half_factor_proper_divisorquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductsecondreal) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductsecondreal) = S ge_signed_half_factor_proper_divisorquotientproductsecondrealdecode))) /\ ((ge_second_rp_factor_proper_divisorquotientproduct) + ge_balance_negative_factor_proper_divisorquotientproductsecondreal = (ge_second_rn_factor_proper_divisorquotientproduct) + ge_balance_positive_factor_proper_divisorquotientproductsecondreal))) /\ (exists ge_balance_positive_factor_proper_divisorquotientproductsecondimaginary ge_balance_negative_factor_proper_divisorquotientproductsecondimaginary. (((((ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductsecondimaginary) /\ (ge_balance_negative_factor_proper_divisorquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisorquotientproductsecond) = 2 * ge_signed_half_factor_proper_divisorquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductsecondimaginary) = S ge_signed_half_factor_proper_divisorquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_factor_proper_divisorquotientproduct) + ge_balance_negative_factor_proper_divisorquotientproductsecondimaginary = (ge_second_in_factor_proper_divisorquotientproduct) + ge_balance_positive_factor_proper_divisorquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_proper_divisorquotientproductoutput ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput. (((z) = ((ge_representation_real_code_factor_proper_divisorquotientproductoutput) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput)) * S ((ge_representation_real_code_factor_proper_divisorquotientproductoutput) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput)) + ((ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput) + (ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput))) /\ ((exists ge_balance_positive_factor_proper_divisorquotientproductoutputreal ge_balance_negative_factor_proper_divisorquotientproductoutputreal. (((((ge_representation_real_code_factor_proper_divisorquotientproductoutput) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductoutputreal) /\ (ge_balance_negative_factor_proper_divisorquotientproductoutputreal) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductoutputrealdecode. (((ge_representation_real_code_factor_proper_divisorquotientproductoutput) = 2 * ge_signed_half_factor_proper_divisorquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductoutputreal) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductoutputreal) = S ge_signed_half_factor_proper_divisorquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_factor_proper_divisorquotientproduct) * (ge_second_rp_factor_proper_divisorquotientproduct))) + (((ge_first_rn_factor_proper_divisorquotientproduct) * (ge_second_rn_factor_proper_divisorquotientproduct))))) + (((((ge_first_ip_factor_proper_divisorquotientproduct) * (ge_second_in_factor_proper_divisorquotientproduct))) + (((ge_first_in_factor_proper_divisorquotientproduct) * (ge_second_ip_factor_proper_divisorquotientproduct))))))) + ge_balance_negative_factor_proper_divisorquotientproductoutputreal = (((((((ge_first_rp_factor_proper_divisorquotientproduct) * (ge_second_rn_factor_proper_divisorquotientproduct))) + (((ge_first_rn_factor_proper_divisorquotientproduct) * (ge_second_rp_factor_proper_divisorquotientproduct))))) + (((((ge_first_ip_factor_proper_divisorquotientproduct) * (ge_second_ip_factor_proper_divisorquotientproduct))) + (((ge_first_in_factor_proper_divisorquotientproduct) * (ge_second_in_factor_proper_divisorquotientproduct))))))) + ge_balance_positive_factor_proper_divisorquotientproductoutputreal))) /\ (exists ge_balance_positive_factor_proper_divisorquotientproductoutputimaginary ge_balance_negative_factor_proper_divisorquotientproductoutputimaginary. (((((ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput) = 2 * (ge_balance_positive_factor_proper_divisorquotientproductoutputimaginary) /\ (ge_balance_negative_factor_proper_divisorquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisorquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisorquotientproductoutput) = 2 * ge_signed_half_factor_proper_divisorquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisorquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisorquotientproductoutputimaginary) = S ge_signed_half_factor_proper_divisorquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_proper_divisorquotientproduct) * (ge_second_ip_factor_proper_divisorquotientproduct))) + (((ge_first_rn_factor_proper_divisorquotientproduct) * (ge_second_in_factor_proper_divisorquotientproduct))))) + (((((ge_first_ip_factor_proper_divisorquotientproduct) * (ge_second_rp_factor_proper_divisorquotientproduct))) + (((ge_first_in_factor_proper_divisorquotientproduct) * (ge_second_rn_factor_proper_divisorquotientproduct))))))) + ge_balance_negative_factor_proper_divisorquotientproductoutputimaginary = (((((((ge_first_rp_factor_proper_divisorquotientproduct) * (ge_second_in_factor_proper_divisorquotientproduct))) + (((ge_first_rn_factor_proper_divisorquotientproduct) * (ge_second_ip_factor_proper_divisorquotientproduct))))) + (((((ge_first_ip_factor_proper_divisorquotientproduct) * (ge_second_rn_factor_proper_divisorquotientproduct))) + (((ge_first_in_factor_proper_divisorquotientproduct) * (ge_second_rp_factor_proper_divisorquotientproduct))))))) + ge_balance_positive_factor_proper_divisorquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_factor_proper_divisor. ((exists ge_norm_rp_factor_proper_divisornorm ge_norm_rn_factor_proper_divisornorm ge_norm_ip_factor_proper_divisornorm ge_norm_in_factor_proper_divisornorm. ((exists ge_representation_real_code_factor_proper_divisornormrepresentation ge_representation_imaginary_code_factor_proper_divisornormrepresentation. (((a) = ((ge_representation_real_code_factor_proper_divisornormrepresentation) + (ge_representation_imaginary_code_factor_proper_divisornormrepresentation)) * S ((ge_representation_real_code_factor_proper_divisornormrepresentation) + (ge_representation_imaginary_code_factor_proper_divisornormrepresentation)) + ((ge_representation_imaginary_code_factor_proper_divisornormrepresentation) + (ge_representation_imaginary_code_factor_proper_divisornormrepresentation))) /\ ((exists ge_balance_positive_factor_proper_divisornormrepresentationreal ge_balance_negative_factor_proper_divisornormrepresentationreal. (((((ge_representation_real_code_factor_proper_divisornormrepresentation) = 2 * (ge_balance_positive_factor_proper_divisornormrepresentationreal) /\ (ge_balance_negative_factor_proper_divisornormrepresentationreal) = 0) \/ exists ge_signed_half_factor_proper_divisornormrepresentationrealdecode. (((ge_representation_real_code_factor_proper_divisornormrepresentation) = 2 * ge_signed_half_factor_proper_divisornormrepresentationrealdecode + 1 /\ (ge_balance_positive_factor_proper_divisornormrepresentationreal) = 0) /\ (ge_balance_negative_factor_proper_divisornormrepresentationreal) = S ge_signed_half_factor_proper_divisornormrepresentationrealdecode))) /\ ((ge_norm_rp_factor_proper_divisornorm) + ge_balance_negative_factor_proper_divisornormrepresentationreal = (ge_norm_rn_factor_proper_divisornorm) + ge_balance_positive_factor_proper_divisornormrepresentationreal))) /\ (exists ge_balance_positive_factor_proper_divisornormrepresentationimaginary ge_balance_negative_factor_proper_divisornormrepresentationimaginary. (((((ge_representation_imaginary_code_factor_proper_divisornormrepresentation) = 2 * (ge_balance_positive_factor_proper_divisornormrepresentationimaginary) /\ (ge_balance_negative_factor_proper_divisornormrepresentationimaginary) = 0) \/ exists ge_signed_half_factor_proper_divisornormrepresentationimaginarydecode. (((ge_representation_imaginary_code_factor_proper_divisornormrepresentation) = 2 * ge_signed_half_factor_proper_divisornormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_factor_proper_divisornormrepresentationimaginary) = 0) /\ (ge_balance_negative_factor_proper_divisornormrepresentationimaginary) = S ge_signed_half_factor_proper_divisornormrepresentationimaginarydecode))) /\ ((ge_norm_ip_factor_proper_divisornorm) + ge_balance_negative_factor_proper_divisornormrepresentationimaginary = (ge_norm_in_factor_proper_divisornorm) + ge_balance_positive_factor_proper_divisornormrepresentationimaginary)))))) /\ (exists ge_real_square_factor_proper_divisornormsquare ge_imaginary_square_factor_proper_divisornormsquare. ((((((ge_norm_rp_factor_proper_divisornorm) * (ge_norm_rp_factor_proper_divisornorm))) + (((ge_norm_rn_factor_proper_divisornorm) * (ge_norm_rn_factor_proper_divisornorm)))) = ((ge_real_square_factor_proper_divisornormsquare) + (((((ge_norm_rp_factor_proper_divisornorm) * (ge_norm_rn_factor_proper_divisornorm))) + (((ge_norm_rn_factor_proper_divisornorm) * (ge_norm_rp_factor_proper_divisornorm))))))) /\ ((((((ge_norm_ip_factor_proper_divisornorm) * (ge_norm_ip_factor_proper_divisornorm))) + (((ge_norm_in_factor_proper_divisornorm) * (ge_norm_in_factor_proper_divisornorm)))) = ((ge_imaginary_square_factor_proper_divisornormsquare) + (((((ge_norm_ip_factor_proper_divisornorm) * (ge_norm_in_factor_proper_divisornorm))) + (((ge_norm_in_factor_proper_divisornorm) * (ge_norm_ip_factor_proper_divisornorm))))))) /\ ((gr_proper_divisor_norm_factor_proper_divisor) = ge_real_square_factor_proper_divisornormsquare + ge_imaginary_square_factor_proper_divisornormsquare)))))) /\ (exists ge_gap_factor_proper_divisorstrict. ge_gap_factor_proper_divisorstrict + S (gr_proper_divisor_norm_factor_proper_divisor) = (N)))))))