Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∀ dvi_index_lowercontinuation. Lt(dvi_index_lowercontinuation,l) → ∃ x. BetaAt(b,c,dvi_index_lowercontinuation,x) ∧ DivisorComplement(n,dvi_index_lowercontinuation,x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall dvi_index_lowercontinuation. (exists pvs_gap_lowercontinuationdomain. pvs_gap_lowercontinuationdomain + S (dvi_index_lowercontinuation) = ((l))) -> exists dvi_value_lowercontinuation. ((((exists ff_h_pvs_lowercontinuationentry. ff_h_pvs_lowercontinuationentry + S (dvi_value_lowercontinuation) = S ((S (dvi_index_lowercontinuation)) * (c))) /\ exists ff_q_pvs_lowercontinuationentry. (b) = ff_q_pvs_lowercontinuationentry * S ((S (dvi_index_lowercontinuation)) * (c)) + (dvi_value_lowercontinuation))) /\ ((((~((dvi_index_lowercontinuation)=0)) /\ (((n))=(dvi_index_lowercontinuation)*(dvi_value_lowercontinuation)))) \/ ((((dvi_index_lowercontinuation)=0 \/ ~(exists pvs_factor_lowercontinuationgraphnondivisor. ((n)) = (dvi_index_lowercontinuation) * pvs_factor_lowercontinuationgraphnondivisor)) /\ ((dvi_value_lowercontinuation)=(dvi_index_lowercontinuation))))))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