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
∀ d. ∀ a. ∀ b. ∀ c. GDvd(d,a) → GMul(a,b,c) → GDvd(d,c)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall d a b c. (exists gr_quotient_product_divisor. (exists ge_first_rp_product_divisorproduct ge_first_rn_product_divisorproduct ge_first_ip_product_divisorproduct ge_first_in_product_divisorproduct ge_second_rp_product_divisorproduct ge_second_rn_product_divisorproduct ge_second_ip_product_divisorproduct ge_second_in_product_divisorproduct. ((exists ge_representation_real_code_product_divisorproductfirst ge_representation_imaginary_code_product_divisorproductfirst. (((d) = ((ge_representation_real_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst)) * S ((ge_representation_real_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst)) + ((ge_representation_imaginary_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst))) /\ ((exists ge_balance_positive_product_divisorproductfirstreal ge_balance_negative_product_divisorproductfirstreal. (((((ge_representation_real_code_product_divisorproductfirst) = 2 * (ge_balance_positive_product_divisorproductfirstreal) /\ (ge_balance_negative_product_divisorproductfirstreal) = 0) \/ exists ge_signed_half_product_divisorproductfirstrealdecode. (((ge_representation_real_code_product_divisorproductfirst) = 2 * ge_signed_half_product_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_product_divisorproductfirstreal) = 0) /\ (ge_balance_negative_product_divisorproductfirstreal) = S ge_signed_half_product_divisorproductfirstrealdecode))) /\ ((ge_first_rp_product_divisorproduct) + ge_balance_negative_product_divisorproductfirstreal = (ge_first_rn_product_divisorproduct) + ge_balance_positive_product_divisorproductfirstreal))) /\ (exists ge_balance_positive_product_divisorproductfirstimaginary ge_balance_negative_product_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_product_divisorproductfirst) = 2 * (ge_balance_positive_product_divisorproductfirstimaginary) /\ (ge_balance_negative_product_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_product_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductfirst) = 2 * ge_signed_half_product_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_product_divisorproductfirstimaginary) = S ge_signed_half_product_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_product_divisorproduct) + ge_balance_negative_product_divisorproductfirstimaginary = (ge_first_in_product_divisorproduct) + ge_balance_positive_product_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_divisorproductsecond ge_representation_imaginary_code_product_divisorproductsecond. (((gr_quotient_product_divisor) = ((ge_representation_real_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond)) * S ((ge_representation_real_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond)) + ((ge_representation_imaginary_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond))) /\ ((exists ge_balance_positive_product_divisorproductsecondreal ge_balance_negative_product_divisorproductsecondreal. (((((ge_representation_real_code_product_divisorproductsecond) = 2 * (ge_balance_positive_product_divisorproductsecondreal) /\ (ge_balance_negative_product_divisorproductsecondreal) = 0) \/ exists ge_signed_half_product_divisorproductsecondrealdecode. (((ge_representation_real_code_product_divisorproductsecond) = 2 * ge_signed_half_product_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_product_divisorproductsecondreal) = 0) /\ (ge_balance_negative_product_divisorproductsecondreal) = S ge_signed_half_product_divisorproductsecondrealdecode))) /\ ((ge_second_rp_product_divisorproduct) + ge_balance_negative_product_divisorproductsecondreal = (ge_second_rn_product_divisorproduct) + ge_balance_positive_product_divisorproductsecondreal))) /\ (exists ge_balance_positive_product_divisorproductsecondimaginary ge_balance_negative_product_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_product_divisorproductsecond) = 2 * (ge_balance_positive_product_divisorproductsecondimaginary) /\ (ge_balance_negative_product_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_product_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductsecond) = 2 * ge_signed_half_product_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_product_divisorproductsecondimaginary) = S ge_signed_half_product_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_product_divisorproduct) + ge_balance_negative_product_divisorproductsecondimaginary = (ge_second_in_product_divisorproduct) + ge_balance_positive_product_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_divisorproductoutput ge_representation_imaginary_code_product_divisorproductoutput. (((a) = ((ge_representation_real_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput)) * S ((ge_representation_real_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput)) + ((ge_representation_imaginary_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput))) /\ ((exists ge_balance_positive_product_divisorproductoutputreal ge_balance_negative_product_divisorproductoutputreal. (((((ge_representation_real_code_product_divisorproductoutput) = 2 * (ge_balance_positive_product_divisorproductoutputreal) /\ (ge_balance_negative_product_divisorproductoutputreal) = 0) \/ exists ge_signed_half_product_divisorproductoutputrealdecode. (((ge_representation_real_code_product_divisorproductoutput) = 2 * ge_signed_half_product_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_product_divisorproductoutputreal) = 0) /\ (ge_balance_negative_product_divisorproductoutputreal) = S ge_signed_half_product_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_divisorproduct) * (ge_second_rp_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_rn_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_in_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_ip_product_divisorproduct))))))) + ge_balance_negative_product_divisorproductoutputreal = (((((((ge_first_rp_product_divisorproduct) * (ge_second_rn_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_rp_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_ip_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_in_product_divisorproduct))))))) + ge_balance_positive_product_divisorproductoutputreal))) /\ (exists ge_balance_positive_product_divisorproductoutputimaginary ge_balance_negative_product_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_product_divisorproductoutput) = 2 * (ge_balance_positive_product_divisorproductoutputimaginary) /\ (ge_balance_negative_product_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_product_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductoutput) = 2 * ge_signed_half_product_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_product_divisorproductoutputimaginary) = S ge_signed_half_product_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_divisorproduct) * (ge_second_ip_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_in_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_rp_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_rn_product_divisorproduct))))))) + ge_balance_negative_product_divisorproductoutputimaginary = (((((((ge_first_rp_product_divisorproduct) * (ge_second_in_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_ip_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_rn_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_rp_product_divisorproduct))))))) + ge_balance_positive_product_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_product_multiple ge_first_rn_product_multiple ge_first_ip_product_multiple ge_first_in_product_multiple ge_second_rp_product_multiple ge_second_rn_product_multiple ge_second_ip_product_multiple ge_second_in_product_multiple. ((exists ge_representation_real_code_product_multiplefirst ge_representation_imaginary_code_product_multiplefirst. (((a) = ((ge_representation_real_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst)) * S ((ge_representation_real_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst)) + ((ge_representation_imaginary_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst))) /\ ((exists ge_balance_positive_product_multiplefirstreal ge_balance_negative_product_multiplefirstreal. (((((ge_representation_real_code_product_multiplefirst) = 2 * (ge_balance_positive_product_multiplefirstreal) /\ (ge_balance_negative_product_multiplefirstreal) = 0) \/ exists ge_signed_half_product_multiplefirstrealdecode. (((ge_representation_real_code_product_multiplefirst) = 2 * ge_signed_half_product_multiplefirstrealdecode + 1 /\ (ge_balance_positive_product_multiplefirstreal) = 0) /\ (ge_balance_negative_product_multiplefirstreal) = S ge_signed_half_product_multiplefirstrealdecode))) /\ ((ge_first_rp_product_multiple) + ge_balance_negative_product_multiplefirstreal = (ge_first_rn_product_multiple) + ge_balance_positive_product_multiplefirstreal))) /\ (exists ge_balance_positive_product_multiplefirstimaginary ge_balance_negative_product_multiplefirstimaginary. (((((ge_representation_imaginary_code_product_multiplefirst) = 2 * (ge_balance_positive_product_multiplefirstimaginary) /\ (ge_balance_negative_product_multiplefirstimaginary) = 0) \/ exists ge_signed_half_product_multiplefirstimaginarydecode. (((ge_representation_imaginary_code_product_multiplefirst) = 2 * ge_signed_half_product_multiplefirstimaginarydecode + 1 /\ (ge_balance_positive_product_multiplefirstimaginary) = 0) /\ (ge_balance_negative_product_multiplefirstimaginary) = S ge_signed_half_product_multiplefirstimaginarydecode))) /\ ((ge_first_ip_product_multiple) + ge_balance_negative_product_multiplefirstimaginary = (ge_first_in_product_multiple) + ge_balance_positive_product_multiplefirstimaginary)))))) /\ ((exists ge_representation_real_code_product_multiplesecond ge_representation_imaginary_code_product_multiplesecond. (((b) = ((ge_representation_real_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond)) * S ((ge_representation_real_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond)) + ((ge_representation_imaginary_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond))) /\ ((exists ge_balance_positive_product_multiplesecondreal ge_balance_negative_product_multiplesecondreal. (((((ge_representation_real_code_product_multiplesecond) = 2 * (ge_balance_positive_product_multiplesecondreal) /\ (ge_balance_negative_product_multiplesecondreal) = 0) \/ exists ge_signed_half_product_multiplesecondrealdecode. (((ge_representation_real_code_product_multiplesecond) = 2 * ge_signed_half_product_multiplesecondrealdecode + 1 /\ (ge_balance_positive_product_multiplesecondreal) = 0) /\ (ge_balance_negative_product_multiplesecondreal) = S ge_signed_half_product_multiplesecondrealdecode))) /\ ((ge_second_rp_product_multiple) + ge_balance_negative_product_multiplesecondreal = (ge_second_rn_product_multiple) + ge_balance_positive_product_multiplesecondreal))) /\ (exists ge_balance_positive_product_multiplesecondimaginary ge_balance_negative_product_multiplesecondimaginary. (((((ge_representation_imaginary_code_product_multiplesecond) = 2 * (ge_balance_positive_product_multiplesecondimaginary) /\ (ge_balance_negative_product_multiplesecondimaginary) = 0) \/ exists ge_signed_half_product_multiplesecondimaginarydecode. (((ge_representation_imaginary_code_product_multiplesecond) = 2 * ge_signed_half_product_multiplesecondimaginarydecode + 1 /\ (ge_balance_positive_product_multiplesecondimaginary) = 0) /\ (ge_balance_negative_product_multiplesecondimaginary) = S ge_signed_half_product_multiplesecondimaginarydecode))) /\ ((ge_second_ip_product_multiple) + ge_balance_negative_product_multiplesecondimaginary = (ge_second_in_product_multiple) + ge_balance_positive_product_multiplesecondimaginary)))))) /\ (exists ge_representation_real_code_product_multipleoutput ge_representation_imaginary_code_product_multipleoutput. (((c) = ((ge_representation_real_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput)) * S ((ge_representation_real_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput)) + ((ge_representation_imaginary_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput))) /\ ((exists ge_balance_positive_product_multipleoutputreal ge_balance_negative_product_multipleoutputreal. (((((ge_representation_real_code_product_multipleoutput) = 2 * (ge_balance_positive_product_multipleoutputreal) /\ (ge_balance_negative_product_multipleoutputreal) = 0) \/ exists ge_signed_half_product_multipleoutputrealdecode. (((ge_representation_real_code_product_multipleoutput) = 2 * ge_signed_half_product_multipleoutputrealdecode + 1 /\ (ge_balance_positive_product_multipleoutputreal) = 0) /\ (ge_balance_negative_product_multipleoutputreal) = S ge_signed_half_product_multipleoutputrealdecode))) /\ ((((((((ge_first_rp_product_multiple) * (ge_second_rp_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_rn_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_in_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_ip_product_multiple))))))) + ge_balance_negative_product_multipleoutputreal = (((((((ge_first_rp_product_multiple) * (ge_second_rn_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_rp_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_ip_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_in_product_multiple))))))) + ge_balance_positive_product_multipleoutputreal))) /\ (exists ge_balance_positive_product_multipleoutputimaginary ge_balance_negative_product_multipleoutputimaginary. (((((ge_representation_imaginary_code_product_multipleoutput) = 2 * (ge_balance_positive_product_multipleoutputimaginary) /\ (ge_balance_negative_product_multipleoutputimaginary) = 0) \/ exists ge_signed_half_product_multipleoutputimaginarydecode. (((ge_representation_imaginary_code_product_multipleoutput) = 2 * ge_signed_half_product_multipleoutputimaginarydecode + 1 /\ (ge_balance_positive_product_multipleoutputimaginary) = 0) /\ (ge_balance_negative_product_multipleoutputimaginary) = S ge_signed_half_product_multipleoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_multiple) * (ge_second_ip_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_in_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_rp_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_rn_product_multiple))))))) + ge_balance_negative_product_multipleoutputimaginary = (((((((ge_first_rp_product_multiple) * (ge_second_in_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_ip_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_rn_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_rp_product_multiple))))))) + ge_balance_positive_product_multipleoutputimaginary))))))))) -> (exists gr_quotient_product_divides. (exists ge_first_rp_product_dividesproduct ge_first_rn_product_dividesproduct ge_first_ip_product_dividesproduct ge_first_in_product_dividesproduct ge_second_rp_product_dividesproduct ge_second_rn_product_dividesproduct ge_second_ip_product_dividesproduct ge_second_in_product_dividesproduct. ((exists ge_representation_real_code_product_dividesproductfirst ge_representation_imaginary_code_product_dividesproductfirst. (((d) = ((ge_representation_real_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst)) * S ((ge_representation_real_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst)) + ((ge_representation_imaginary_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst))) /\ ((exists ge_balance_positive_product_dividesproductfirstreal ge_balance_negative_product_dividesproductfirstreal. (((((ge_representation_real_code_product_dividesproductfirst) = 2 * (ge_balance_positive_product_dividesproductfirstreal) /\ (ge_balance_negative_product_dividesproductfirstreal) = 0) \/ exists ge_signed_half_product_dividesproductfirstrealdecode. (((ge_representation_real_code_product_dividesproductfirst) = 2 * ge_signed_half_product_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_product_dividesproductfirstreal) = 0) /\ (ge_balance_negative_product_dividesproductfirstreal) = S ge_signed_half_product_dividesproductfirstrealdecode))) /\ ((ge_first_rp_product_dividesproduct) + ge_balance_negative_product_dividesproductfirstreal = (ge_first_rn_product_dividesproduct) + ge_balance_positive_product_dividesproductfirstreal))) /\ (exists ge_balance_positive_product_dividesproductfirstimaginary ge_balance_negative_product_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_product_dividesproductfirst) = 2 * (ge_balance_positive_product_dividesproductfirstimaginary) /\ (ge_balance_negative_product_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_product_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductfirst) = 2 * ge_signed_half_product_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_product_dividesproductfirstimaginary) = S ge_signed_half_product_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_product_dividesproduct) + ge_balance_negative_product_dividesproductfirstimaginary = (ge_first_in_product_dividesproduct) + ge_balance_positive_product_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_dividesproductsecond ge_representation_imaginary_code_product_dividesproductsecond. (((gr_quotient_product_divides) = ((ge_representation_real_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond)) * S ((ge_representation_real_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond)) + ((ge_representation_imaginary_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond))) /\ ((exists ge_balance_positive_product_dividesproductsecondreal ge_balance_negative_product_dividesproductsecondreal. (((((ge_representation_real_code_product_dividesproductsecond) = 2 * (ge_balance_positive_product_dividesproductsecondreal) /\ (ge_balance_negative_product_dividesproductsecondreal) = 0) \/ exists ge_signed_half_product_dividesproductsecondrealdecode. (((ge_representation_real_code_product_dividesproductsecond) = 2 * ge_signed_half_product_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_product_dividesproductsecondreal) = 0) /\ (ge_balance_negative_product_dividesproductsecondreal) = S ge_signed_half_product_dividesproductsecondrealdecode))) /\ ((ge_second_rp_product_dividesproduct) + ge_balance_negative_product_dividesproductsecondreal = (ge_second_rn_product_dividesproduct) + ge_balance_positive_product_dividesproductsecondreal))) /\ (exists ge_balance_positive_product_dividesproductsecondimaginary ge_balance_negative_product_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_product_dividesproductsecond) = 2 * (ge_balance_positive_product_dividesproductsecondimaginary) /\ (ge_balance_negative_product_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_product_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductsecond) = 2 * ge_signed_half_product_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_product_dividesproductsecondimaginary) = S ge_signed_half_product_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_product_dividesproduct) + ge_balance_negative_product_dividesproductsecondimaginary = (ge_second_in_product_dividesproduct) + ge_balance_positive_product_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_dividesproductoutput ge_representation_imaginary_code_product_dividesproductoutput. (((c) = ((ge_representation_real_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput)) * S ((ge_representation_real_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput)) + ((ge_representation_imaginary_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput))) /\ ((exists ge_balance_positive_product_dividesproductoutputreal ge_balance_negative_product_dividesproductoutputreal. (((((ge_representation_real_code_product_dividesproductoutput) = 2 * (ge_balance_positive_product_dividesproductoutputreal) /\ (ge_balance_negative_product_dividesproductoutputreal) = 0) \/ exists ge_signed_half_product_dividesproductoutputrealdecode. (((ge_representation_real_code_product_dividesproductoutput) = 2 * ge_signed_half_product_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_product_dividesproductoutputreal) = 0) /\ (ge_balance_negative_product_dividesproductoutputreal) = S ge_signed_half_product_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_dividesproduct) * (ge_second_rp_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_rn_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_in_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_ip_product_dividesproduct))))))) + ge_balance_negative_product_dividesproductoutputreal = (((((((ge_first_rp_product_dividesproduct) * (ge_second_rn_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_rp_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_ip_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_in_product_dividesproduct))))))) + ge_balance_positive_product_dividesproductoutputreal))) /\ (exists ge_balance_positive_product_dividesproductoutputimaginary ge_balance_negative_product_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_product_dividesproductoutput) = 2 * (ge_balance_positive_product_dividesproductoutputimaginary) /\ (ge_balance_negative_product_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_product_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductoutput) = 2 * ge_signed_half_product_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_product_dividesproductoutputimaginary) = S ge_signed_half_product_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_dividesproduct) * (ge_second_ip_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_in_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_rp_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_rn_product_dividesproduct))))))) + ge_balance_negative_product_dividesproductoutputimaginary = (((((((ge_first_rp_product_dividesproduct) * (ge_second_in_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_ip_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_rn_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_rp_product_dividesproduct))))))) + ge_balance_positive_product_dividesproductoutputimaginary))))))))))Complete tactic proof in conservative notation
All 13 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
13 script commands · 4 reading checkpoints · 0 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 (1)
01Fix variables and assumptionsL1–6
02Use earlier factsL7–11
03Construct an explicit witnessL12–12
Supply the displayed value, then prove that it has the required property.
- L12
exists (b)
04Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hprod
Original defined command ledger · 13 lines
- 0001
intro d - 0002
intro a - 0003
intro b - 0004
intro c - 0005
intro hd - 0006
intro hprod - 0007
specialize gaussian_divides_transitive (d) - 0008
specialize gaussian_divides_transitive (a) - 0009
specialize gaussian_divides_transitive (c) - 0010
apply gaussian_divides_transitive - 0011
exact hd - 0012
exists (b) - 0013
exact hprod