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) ∧ DivisorPrimeToggle(n,p,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)) /\ (((exists pvs_factor_lowercontinuationgraphdivisor. ((n)) = (dvi_index_lowercontinuation) * pvs_factor_lowercontinuationgraphdivisor) /\ ((((~(exists pvs_factor_lowercontinuationgraphtogglefresh_input. (dvi_index_lowercontinuation) = ((p)) * pvs_factor_lowercontinuationgraphtogglefresh_input)) /\ ((dvi_value_lowercontinuation)=((p))*(dvi_index_lowercontinuation)))) \/ (((((dvi_index_lowercontinuation)=((p))*(dvi_value_lowercontinuation)) /\ (~(exists pvs_factor_lowercontinuationgraphtogglefresh_output. (dvi_value_lowercontinuation) = ((p)) * pvs_factor_lowercontinuationgraphtogglefresh_output)))) \/ (((exists pvs_factor_lowercontinuationgraphtogglesquare. (dvi_index_lowercontinuation) = (((p))*((p))) * pvs_factor_lowercontinuationgraphtogglesquare) /\ ((dvi_value_lowercontinuation)=(dvi_index_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