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
(∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Dvd(y,M)) ∧ (∀ x. (∀ y. ∀ z. Lt(y,l) → Beta(b,c,y,z) → Dvd(z,x)) → Dvd(M,x))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((forall gcrt_common_index_research_own gcrt_common_modulus_research_own. (exists ff_lt_gcrt_research_own_bound. ff_lt_gcrt_research_own_bound + S gcrt_common_index_research_own = l) -> (((exists ff_h_gcrt_research_own_entry. ff_h_gcrt_research_own_entry + S (gcrt_common_modulus_research_own) = S ((S (gcrt_common_index_research_own)) * c)) /\ exists ff_q_gcrt_research_own_entry. b = ff_q_gcrt_research_own_entry * S ((S (gcrt_common_index_research_own)) * c) + (gcrt_common_modulus_research_own))) -> exists gcrt_common_quotient_research_own. M = gcrt_common_modulus_research_own * gcrt_common_quotient_research_own) /\ forall gcrt_lcm_common_research. (forall gcrt_common_index_research_other gcrt_common_modulus_research_other. (exists ff_lt_gcrt_research_other_bound. ff_lt_gcrt_research_other_bound + S gcrt_common_index_research_other = l) -> (((exists ff_h_gcrt_research_other_entry. ff_h_gcrt_research_other_entry + S (gcrt_common_modulus_research_other) = S ((S (gcrt_common_index_research_other)) * c)) /\ exists ff_q_gcrt_research_other_entry. b = ff_q_gcrt_research_other_entry * S ((S (gcrt_common_index_research_other)) * c) + (gcrt_common_modulus_research_other))) -> exists gcrt_common_quotient_research_other. gcrt_lcm_common_research = gcrt_common_modulus_research_other * gcrt_common_quotient_research_other) -> exists gcrt_lcm_quotient_research. gcrt_lcm_common_research = M * gcrt_lcm_quotient_research)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
FC000B · crt_prefix_gcd_congruences_lcmFC000D · crt_pairwise_compatible_prefix_implies_merge_compatibleFC000F · crt_pairwise_compatible_prefix_canonical_exists_uniqueFC0010 · crt_canonical_prefix_solution_implies_normalizedFC0012 · crt_prefix_solution_normalized_existsFC0015 · crt_pairwise_compatible_prefix_merge_iffFC0018 · crt_positive_normalized_prefix_iff_canonical