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
∀ gcrt_solution_index_research. ∀ gcrt_solution_residue_research. ∀ gcrt_solution_modulus_research. Lt(gcrt_solution_index_research,l) → Beta(r,s,gcrt_solution_index_research,gcrt_solution_residue_research) → Beta(b,c,gcrt_solution_index_research,gcrt_solution_modulus_research) → ModEq(gcrt_solution_modulus_research,x,gcrt_solution_residue_research)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall gcrt_solution_index_research gcrt_solution_residue_research gcrt_solution_modulus_research. (exists ff_lt_gcrt_research_bound. ff_lt_gcrt_research_bound + S gcrt_solution_index_research = l) -> (((exists ff_h_gcrt_research_residue. ff_h_gcrt_research_residue + S (gcrt_solution_residue_research) = S ((S (gcrt_solution_index_research)) * s)) /\ exists ff_q_gcrt_research_residue. r = ff_q_gcrt_research_residue * S ((S (gcrt_solution_index_research)) * s) + (gcrt_solution_residue_research))) -> (((exists ff_h_gcrt_research_modulus. ff_h_gcrt_research_modulus + S (gcrt_solution_modulus_research) = S ((S (gcrt_solution_index_research)) * c)) /\ exists ff_q_gcrt_research_modulus. b = ff_q_gcrt_research_modulus * S ((S (gcrt_solution_index_research)) * c) + (gcrt_solution_modulus_research))) -> (exists hgcrt_mod_left_gcrt_research_congruence hgcrt_mod_right_gcrt_research_congruence. x + gcrt_solution_modulus_research * hgcrt_mod_left_gcrt_research_congruence = gcrt_solution_residue_research + gcrt_solution_modulus_research * hgcrt_mod_right_gcrt_research_congruence)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
FC000C · crt_pairwise_compatible_prefix_induces_gcd_congruencesFC000D · crt_pairwise_compatible_prefix_implies_merge_compatibleFC000E · crt_pairwise_compatible_prefix_solution_existsFC000F · crt_pairwise_compatible_prefix_canonical_exists_uniqueFC0010 · crt_canonical_prefix_solution_implies_normalizedFC0012 · crt_prefix_solution_normalized_existsFC0013 · crt_pairwise_compatible_prefix_normalized_exists_uniqueFC0014 · crt_pairwise_compatible_prefix_solvable_iffFC0015 · crt_pairwise_compatible_prefix_merge_iffFC0016 · crt_normalized_prefix_solution_class_iff_lcmFC0017 · crt_normalized_zero_lcm_all_solutions_uniqueFC0018 · crt_positive_normalized_prefix_iff_canonical