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
∀ gfull_index_secondwave. ∀ gfull_modulus_secondwave. ∀ gfull_gcd_secondwave. Lt(gfull_index_secondwave,l) → BetaAt(b,c,gfull_index_secondwave,gfull_modulus_secondwave) → IsGCD(gfull_gcd_secondwave,gfull_modulus_secondwave,m) → ModEq(gfull_gcd_secondwave,u,v)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall gfull_index_secondwave gfull_modulus_secondwave gfull_gcd_secondwave. (exists ff_lt_gcrt_gfull_secondwave_bound. ff_lt_gcrt_gfull_secondwave_bound + S gfull_index_secondwave = l) -> (((exists ff_h_gcrt_gfull_secondwave_entry. ff_h_gcrt_gfull_secondwave_entry + S (gfull_modulus_secondwave) = S ((S (gfull_index_secondwave)) * c)) /\ exists ff_q_gcrt_gfull_secondwave_entry. b = ff_q_gcrt_gfull_secondwave_entry * S ((S (gfull_index_secondwave)) * c) + (gfull_modulus_secondwave))) -> ((((exists ec_gcd_left_gfull_secondwave_gcd. gfull_modulus_secondwave = gfull_gcd_secondwave * ec_gcd_left_gfull_secondwave_gcd) /\ (exists ec_gcd_right_gfull_secondwave_gcd. m = gfull_gcd_secondwave * ec_gcd_right_gfull_secondwave_gcd)) /\ forall ec_gcd_common_gfull_secondwave_gcd. (exists ec_gcd_common_left_gfull_secondwave_gcd. gfull_modulus_secondwave = ec_gcd_common_gfull_secondwave_gcd * ec_gcd_common_left_gfull_secondwave_gcd) -> (exists ec_gcd_common_right_gfull_secondwave_gcd. m = ec_gcd_common_gfull_secondwave_gcd * ec_gcd_common_right_gfull_secondwave_gcd) -> exists ec_gcd_greatest_gfull_secondwave_gcd. gfull_gcd_secondwave = ec_gcd_common_gfull_secondwave_gcd * ec_gcd_greatest_gfull_secondwave_gcd)) -> (exists hgcrt_mod_left_gfull_secondwave_mod hgcrt_mod_right_gfull_secondwave_mod. u + gfull_gcd_secondwave * hgcrt_mod_left_gfull_secondwave_mod = v + gfull_gcd_secondwave * hgcrt_mod_right_gfull_secondwave_mod)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
none