Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ z. ZPairValid(z) → ¬z = 0 → ∃ x. ∃ y. ∃ n. ∃ m. GPrimeFactorization(z,x,y,n,m)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z. (exists ge_real_positive_prime_factorization_domain ge_real_negative_prime_factorization_domain ge_imaginary_positive_prime_factorization_domain ge_imaginary_negative_prime_factorization_domain. (exists ge_real_code_prime_factorization_domaindecode ge_imaginary_code_prime_factorization_domaindecode. (((z) = ((ge_real_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode)) * S ((ge_real_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode)) + ((ge_imaginary_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode))) /\ (((((ge_real_code_prime_factorization_domaindecode) = 2 * (ge_real_positive_prime_factorization_domain) /\ (ge_real_negative_prime_factorization_domain) = 0) \/ exists ge_signed_half_ge_prime_factorization_domaindecode_real. (((ge_real_code_prime_factorization_domaindecode) = 2 * ge_signed_half_ge_prime_factorization_domaindecode_real + 1 /\ (ge_real_positive_prime_factorization_domain) = 0) /\ (ge_real_negative_prime_factorization_domain) = S ge_signed_half_ge_prime_factorization_domaindecode_real))) /\ ((((ge_imaginary_code_prime_factorization_domaindecode) = 2 * (ge_imaginary_positive_prime_factorization_domain) /\ (ge_imaginary_negative_prime_factorization_domain) = 0) \/ exists ge_signed_half_ge_prime_factorization_domaindecode_imaginary. (((ge_imaginary_code_prime_factorization_domaindecode) = 2 * ge_signed_half_ge_prime_factorization_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_domain) = 0) /\ (ge_imaginary_negative_prime_factorization_domain) = S ge_signed_half_ge_prime_factorization_domaindecode_imaginary))))))) -> ~(z=0) -> exists u b c l. (((exists gr_inverse_prime_factorization_existsunit. (exists ge_first_rp_prime_factorization_existsunitidentity ge_first_rn_prime_factorization_existsunitidentity ge_first_ip_prime_factorization_existsunitidentity ge_first_in_prime_factorization_existsunitidentity ge_second_rp_prime_factorization_existsunitidentity ge_second_rn_prime_factorization_existsunitidentity ge_second_ip_prime_factorization_existsunitidentity ge_second_in_prime_factorization_existsunitidentity. ((exists ge_representation_real_code_prime_factorization_existsunitidentityfirst ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst. (((u) = ((ge_representation_real_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentityfirstreal ge_balance_negative_prime_factorization_existsunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstreal) = S ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentityfirstreal = (ge_first_rn_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary = (ge_first_in_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsunitidentitysecond ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond. (((gr_inverse_prime_factorization_existsunit) = ((ge_representation_real_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentitysecondreal ge_balance_negative_prime_factorization_existsunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondreal) = S ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentitysecondreal = (ge_second_rn_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary = (ge_second_in_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsunitidentityoutput ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentityoutputreal ge_balance_negative_prime_factorization_existsunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputreal) = S ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))))))) + ge_balance_negative_prime_factorization_existsunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))))))) + ge_balance_positive_prime_factorization_existsunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))))))) + ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))))))) + ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_prime_factorization_existsprimes gr_prime_factor_value_prime_factorization_existsprimes. (exists ge_gap_prime_factorization_existsprimesindex. ge_gap_prime_factorization_existsprimesindex + S (gr_prime_factor_index_prime_factorization_existsprimes) = (l)) -> (((exists ff_h_gprod_prime_factorization_existsprimesentry. ff_h_gprod_prime_factorization_existsprimesentry + S (gr_prime_factor_value_prime_factorization_existsprimes) = S ((S (gr_prime_factor_index_prime_factorization_existsprimes)) * c)) /\ exists ff_q_gprod_prime_factorization_existsprimesentry. b = ff_q_gprod_prime_factorization_existsprimesentry * S ((S (gr_prime_factor_index_prime_factorization_existsprimes)) * c) + (gr_prime_factor_value_prime_factorization_existsprimes))) -> (((exists ge_real_positive_prime_factorization_existsprimesprimecarrier ge_real_negative_prime_factorization_existsprimesprimecarrier ge_imaginary_positive_prime_factorization_existsprimesprimecarrier ge_imaginary_negative_prime_factorization_existsprimesprimecarrier. (exists ge_real_code_prime_factorization_existsprimesprimecarrierdecode ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode)) * S ((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode)) + ((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode))) /\ (((((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * (ge_real_positive_prime_factorization_existsprimesprimecarrier) /\ (ge_real_negative_prime_factorization_existsprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real. (((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_prime_factorization_existsprimesprimecarrier) = 0) /\ (ge_real_negative_prime_factorization_existsprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_prime_factorization_existsprimesprimecarrier) /\ (ge_imaginary_negative_prime_factorization_existsprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_existsprimesprimecarrier) = 0) /\ (ge_imaginary_negative_prime_factorization_existsprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_prime_factorization_existsprimes)=0)) /\ ((~(exists gr_inverse_prime_factorization_existsprimesprimenonunit. (exists ge_first_rp_prime_factorization_existsprimesprimenonunitidentity ge_first_rn_prime_factorization_existsprimesprimenonunitidentity ge_first_ip_prime_factorization_existsprimesprimenonunitidentity ge_first_in_prime_factorization_existsprimesprimenonunitidentity ge_second_rp_prime_factorization_existsprimesprimenonunitidentity ge_second_rn_prime_factorization_existsprimesprimenonunitidentity ge_second_ip_prime_factorization_existsprimesprimenonunitidentity ge_second_in_prime_factorization_existsprimesprimenonunitidentity. ((exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal = (ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond. (((gr_inverse_prime_factorization_existsprimesprimenonunit) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal = (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary = (ge_second_in_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_factorization_existsprimesprime gr_second_factor_prime_factorization_existsprimesprime gr_product_prime_factorization_existsprimesprime. (exists ge_first_rp_prime_factorization_existsprimesprimeproduct ge_first_rn_prime_factorization_existsprimesprimeproduct ge_first_ip_prime_factorization_existsprimesprimeproduct ge_first_in_prime_factorization_existsprimesprimeproduct ge_second_rp_prime_factorization_existsprimesprimeproduct ge_second_rn_prime_factorization_existsprimesprimeproduct ge_second_ip_prime_factorization_existsprimesprimeproduct ge_second_in_prime_factorization_existsprimesprimeproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst. (((gr_first_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond. (((gr_second_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput. (((gr_product_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_prime_factorization_existsprimesprimedivisor. (exists ge_first_rp_prime_factorization_existsprimesprimedivisorproduct ge_first_rn_prime_factorization_existsprimesprimedivisorproduct ge_first_ip_prime_factorization_existsprimesprimedivisorproduct ge_first_in_prime_factorization_existsprimesprimedivisorproduct ge_second_rp_prime_factorization_existsprimesprimedivisorproduct ge_second_rn_prime_factorization_existsprimesprimedivisorproduct ge_second_ip_prime_factorization_existsprimesprimedivisorproduct ge_second_in_prime_factorization_existsprimesprimedivisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimedivisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput. (((gr_product_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_factorization_existsprimesprimefirst_divisor. (exists ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimefirst_divisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput. (((gr_first_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_factorization_existsprimesprimesecond_divisor. (exists ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimesecond_divisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput. (((gr_second_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_prime_factorization_exists. ((exists gr_product_trace_prime_factorization_existstrace gr_product_scale_prime_factorization_existstrace. ((((exists ff_h_gprod_prime_factorization_existstracestart. ff_h_gprod_prime_factorization_existstracestart + S (6) = S ((S (0)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestart. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestart * S ((S (0)) * gr_product_scale_prime_factorization_existstrace) + (6))) /\ ((((exists ff_h_gprod_prime_factorization_existstraceend. ff_h_gprod_prime_factorization_existstraceend + S (gr_prime_factor_product_prime_factorization_exists) = S ((S (l)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstraceend. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstraceend * S ((S (l)) * gr_product_scale_prime_factorization_existstrace) + (gr_prime_factor_product_prime_factorization_exists))) /\ (forall gr_product_index_prime_factorization_existstracesteps. (exists ge_gap_prime_factorization_existstracestepsindex_bound. ge_gap_prime_factorization_existstracestepsindex_bound + S (gr_product_index_prime_factorization_existstracesteps) = (l)) -> exists gr_product_factor_prime_factorization_existstracesteps gr_product_before_prime_factorization_existstracesteps gr_product_after_prime_factorization_existstracesteps. ((((exists ff_h_gprod_prime_factorization_existstracestepsfactor. ff_h_gprod_prime_factorization_existstracestepsfactor + S (gr_product_factor_prime_factorization_existstracesteps) = S ((S (gr_product_index_prime_factorization_existstracesteps)) * c)) /\ exists ff_q_gprod_prime_factorization_existstracestepsfactor. b = ff_q_gprod_prime_factorization_existstracestepsfactor * S ((S (gr_product_index_prime_factorization_existstracesteps)) * c) + (gr_product_factor_prime_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_existstracestepsbefore. ff_h_gprod_prime_factorization_existstracestepsbefore + S (gr_product_before_prime_factorization_existstracesteps) = S ((S (gr_product_index_prime_factorization_existstracesteps)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestepsbefore. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestepsbefore * S ((S (gr_product_index_prime_factorization_existstracesteps)) * gr_product_scale_prime_factorization_existstrace) + (gr_product_before_prime_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_existstracestepsafter. ff_h_gprod_prime_factorization_existstracestepsafter + S (gr_product_after_prime_factorization_existstracesteps) = S ((S (S (gr_product_index_prime_factorization_existstracesteps))) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestepsafter. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestepsafter * S ((S (S (gr_product_index_prime_factorization_existstracesteps))) * gr_product_scale_prime_factorization_existstrace) + (gr_product_after_prime_factorization_existstracesteps))) /\ (exists ge_first_rp_prime_factorization_existstracestepsmultiply ge_first_rn_prime_factorization_existstracestepsmultiply ge_first_ip_prime_factorization_existstracestepsmultiply ge_first_in_prime_factorization_existstracestepsmultiply ge_second_rp_prime_factorization_existstracestepsmultiply ge_second_rn_prime_factorization_existstracestepsmultiply ge_second_ip_prime_factorization_existstracestepsmultiply ge_second_in_prime_factorization_existstracestepsmultiply. ((exists ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst. (((gr_product_before_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal = (ge_first_rn_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary = (ge_first_in_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond. (((gr_product_factor_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal = (ge_second_rn_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary = (ge_second_in_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput. (((gr_product_after_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))))))) + ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal = (((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))))))) + ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))))))) + ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary = (((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))))))) + ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_prime_factorization_existsreconstruct ge_first_rn_prime_factorization_existsreconstruct ge_first_ip_prime_factorization_existsreconstruct ge_first_in_prime_factorization_existsreconstruct ge_second_rp_prime_factorization_existsreconstruct ge_second_rn_prime_factorization_existsreconstruct ge_second_ip_prime_factorization_existsreconstruct ge_second_in_prime_factorization_existsreconstruct. ((exists ge_representation_real_code_prime_factorization_existsreconstructfirst ge_representation_imaginary_code_prime_factorization_existsreconstructfirst. (((u) = ((ge_representation_real_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst)) * S ((ge_representation_real_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructfirstreal ge_balance_negative_prime_factorization_existsreconstructfirstreal. (((((ge_representation_real_code_prime_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_existsreconstructfirstreal) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructfirst) = 2 * ge_signed_half_prime_factorization_existsreconstructfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstreal) = S ge_signed_half_prime_factorization_existsreconstructfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructfirstreal = (ge_first_rn_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructfirstimaginary ge_balance_negative_prime_factorization_existsreconstructfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_existsreconstructfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) = 2 * ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstimaginary) = S ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructfirstimaginary = (ge_first_in_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsreconstructsecond ge_representation_imaginary_code_prime_factorization_existsreconstructsecond. (((gr_prime_factor_product_prime_factorization_exists) = ((ge_representation_real_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond)) * S ((ge_representation_real_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructsecondreal ge_balance_negative_prime_factorization_existsreconstructsecondreal. (((((ge_representation_real_code_prime_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_existsreconstructsecondreal) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructsecond) = 2 * ge_signed_half_prime_factorization_existsreconstructsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondreal) = S ge_signed_half_prime_factorization_existsreconstructsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructsecondreal = (ge_second_rn_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructsecondimaginary ge_balance_negative_prime_factorization_existsreconstructsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_existsreconstructsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) = 2 * ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondimaginary) = S ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructsecondimaginary = (ge_second_in_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsreconstructoutput ge_representation_imaginary_code_prime_factorization_existsreconstructoutput. (((z) = ((ge_representation_real_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput)) * S ((ge_representation_real_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructoutputreal ge_balance_negative_prime_factorization_existsreconstructoutputreal. (((((ge_representation_real_code_prime_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_existsreconstructoutputreal) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructoutput) = 2 * ge_signed_half_prime_factorization_existsreconstructoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputreal) = S ge_signed_half_prime_factorization_existsreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))))))) + ge_balance_negative_prime_factorization_existsreconstructoutputreal = (((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))))))) + ge_balance_positive_prime_factorization_existsreconstructoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructoutputimaginary ge_balance_negative_prime_factorization_existsreconstructoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_existsreconstructoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) = 2 * ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputimaginary) = S ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))))))) + ge_balance_negative_prime_factorization_existsreconstructoutputimaginary = (((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))))))) + ge_balance_positive_prime_factorization_existsreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 23 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
23 script commands · 5 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–3
02Establish hfL4–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian irreducible factorization exists.
- L4
have hf : ∃ u. ∃ b. ∃ c. ∃ l. GIrreducibleFactorization(z,u,b,c,l)Definitions: GIrreducibleFactorization(z,u,b,c,l)Original native command in the exact edition - L5
specialize gaussian_irreducible_factorization_exists (z) - L6
apply gaussian_irreducible_factorization_exists - L7
exact hv - L8
exact hz
03Separate the logical casesL9–12
04Construct an explicit witnessL13–16
05Use earlier factsL17–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
specialize gaussian_irreducible_factorization_is_prime (z) - L18
specialize gaussian_irreducible_factorization_is_prime (x) - L19
specialize gaussian_irreducible_factorization_is_prime (x1) - L20
specialize gaussian_irreducible_factorization_is_prime (x2) - L21
specialize gaussian_irreducible_factorization_is_prime (x3) - L22
apply gaussian_irreducible_factorization_is_prime - L23
exact hf_witness_witness_witness_witness
Original defined command ledger · 23 lines
- 0001
intro z - 0002
intro hv - 0003
intro hz - 0004
have hf : ∃ u. ∃ b. ∃ c. ∃ l. GIrreducibleFactorization(z,u,b,c,l) - 0005
specialize gaussian_irreducible_factorization_exists (z) - 0006
apply gaussian_irreducible_factorization_exists - 0007
exact hv - 0008
exact hz - 0009
cases hf - 0010
cases hf_witness - 0011
cases hf_witness_witness - 0012
cases hf_witness_witness_witness - 0013
exists (x) - 0014
exists (x1) - 0015
exists (x2) - 0016
exists (x3) - 0017
specialize gaussian_irreducible_factorization_is_prime (z) - 0018
specialize gaussian_irreducible_factorization_is_prime (x) - 0019
specialize gaussian_irreducible_factorization_is_prime (x1) - 0020
specialize gaussian_irreducible_factorization_is_prime (x2) - 0021
specialize gaussian_irreducible_factorization_is_prime (x3) - 0022
apply gaussian_irreducible_factorization_is_prime - 0023
exact hf_witness_witness_witness_witness