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.
Definition in prerequisite notation
∃ gr_quotient_gaussianfactorization. GMul(d,gr_quotient_gaussianfactorization,z)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists gr_quotient_gaussianfactorization. (exists ge_first_rp_gaussianfactorizationproduct ge_first_rn_gaussianfactorizationproduct ge_first_ip_gaussianfactorizationproduct ge_first_in_gaussianfactorizationproduct ge_second_rp_gaussianfactorizationproduct ge_second_rn_gaussianfactorizationproduct ge_second_ip_gaussianfactorizationproduct ge_second_in_gaussianfactorizationproduct. ((exists ge_representation_real_code_gaussianfactorizationproductfirst ge_representation_imaginary_code_gaussianfactorizationproductfirst. ((((d)) = ((ge_representation_real_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationproductfirstreal ge_balance_negative_gaussianfactorizationproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationproductfirst) = 2 * ge_signed_half_gaussianfactorizationproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductfirstreal) = S ge_signed_half_gaussianfactorizationproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductfirstreal = (ge_first_rn_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductfirstimaginary ge_balance_negative_gaussianfactorizationproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductfirst) = 2 * ge_signed_half_gaussianfactorizationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductfirstimaginary) = S ge_signed_half_gaussianfactorizationproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductfirstimaginary = (ge_first_in_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationproductsecond ge_representation_imaginary_code_gaussianfactorizationproductsecond. (((gr_quotient_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationproductsecondreal ge_balance_negative_gaussianfactorizationproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationproductsecond) = 2 * ge_signed_half_gaussianfactorizationproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductsecondreal) = S ge_signed_half_gaussianfactorizationproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductsecondreal = (ge_second_rn_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductsecondimaginary ge_balance_negative_gaussianfactorizationproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductsecond) = 2 * ge_signed_half_gaussianfactorizationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductsecondimaginary) = S ge_signed_half_gaussianfactorizationproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductsecondimaginary = (ge_second_in_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationproductoutput ge_representation_imaginary_code_gaussianfactorizationproductoutput. ((((z)) = ((ge_representation_real_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationproductoutputreal ge_balance_negative_gaussianfactorizationproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationproductoutput) = 2 * ge_signed_half_gaussianfactorizationproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductoutputreal) = S ge_signed_half_gaussianfactorizationproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))))))) + ge_balance_negative_gaussianfactorizationproductoutputreal = (((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))))))) + ge_balance_positive_gaussianfactorizationproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductoutputimaginary ge_balance_negative_gaussianfactorizationproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductoutput) = 2 * ge_signed_half_gaussianfactorizationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductoutputimaginary) = S ge_signed_half_gaussianfactorizationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))))))) + ge_balance_negative_gaussianfactorizationproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))))))) + ge_balance_positive_gaussianfactorizationproductoutputimaginary)))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
GF0042 · gaussian_divides_input_validGF0043 · gaussian_divides_value_validGF0044 · gaussian_divides_reflexiveGF0045 · gaussian_divides_zeroGF0046 · gaussian_one_dividesGF0047 · gaussian_zero_divides_only_zeroGF0048 · gaussian_divides_transitiveGF0049 · gaussian_divides_product_leftGF004A · gaussian_divides_product_rightGF004B · gaussian_common_divisor_addGF004C · gaussian_common_divisor_subtractGF004D · gaussian_unit_dividesGF004E · gaussian_divisor_of_unit_is_unitGF004F · gaussian_common_divisor_euclidean_forwardGF0050 · gaussian_common_divisor_euclidean_backwardGF0051 · gaussian_division_zero_remainder_dividesGF0052 · gaussian_division_divisible_remainder_zeroGF0053 · gaussian_divides_decidableGF0058 · gaussian_associate_dividesGF005A · gaussian_mutual_divisibility_associateGF005B · gaussian_divisor_norm_factorGF005C · gaussian_divisor_norm_boundGF005D · gaussian_nonunit_divisor_of_irreducible_is_associateGF005E · gaussian_irreducible_divides_irreducible_associateGF0061 · gaussian_common_divisor_of_bezoutGF0067 · gaussian_bezout_unit_divisor_cancelGF0068 · gaussian_nonzero_product_divisor_unit_cofactorGF0069 · gaussian_irreducible_dvd_productGF006B · gaussian_prime_is_irreducibleGF0074 · gaussian_proper_norm_divisor_decidableGF007C · gaussian_search_divisor_of_nonzero_nonzeroGF0080 · gaussian_irreducible_divisor_bounded_normGF0081 · gaussian_irreducible_divisor_existsGF0082 · gaussian_nonunit_divisor_strict_quotientGF0083 · gaussian_irreducible_factor_reductionGF009F · gaussian_irreducible_divisor_product_memberGF00AF · gaussian_irreducible_products_associate_unique