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
Prime(p) ∧ (Lt(a,p) ∧ (∀ x. Prime(x) → Lt(a,x) → Le(p,x)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(p = 1) /\ forall bpr_left_pc_pen_lowerlayer_prime bpr_right_pc_pen_lowerlayer_prime. p = bpr_left_pc_pen_lowerlayer_prime * bpr_right_pc_pen_lowerlayer_prime -> bpr_left_pc_pen_lowerlayer_prime = 1 \/ bpr_right_pc_pen_lowerlayer_prime = 1)) /\ ((exists pc_lt_pen_lowerlayer_greater. pc_lt_pen_lowerlayer_greater + S (a) = (p)) /\ forall pen_comparison_lowerlayer. ((~(pen_comparison_lowerlayer = 1) /\ forall bpr_left_pc_pen_lowerlayer_comparison bpr_right_pc_pen_lowerlayer_comparison. pen_comparison_lowerlayer = bpr_left_pc_pen_lowerlayer_comparison * bpr_right_pc_pen_lowerlayer_comparison -> bpr_left_pc_pen_lowerlayer_comparison = 1 \/ bpr_right_pc_pen_lowerlayer_comparison = 1)) -> (exists pc_lt_pen_lowerlayer_above. pc_lt_pen_lowerlayer_above + S (a) = (pen_comparison_lowerlayer)) -> (exists pc_le_pen_lowerlayer_minimal. pc_le_pen_lowerlayer_minimal + (p) = (pen_comparison_lowerlayer)))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
PE0002 · least_prime_above_finite_scanPE0003 · least_prime_above_existsPE0004 · least_prime_above_uniquePE0005 · least_prime_above_bertrand_boundPE0006 · least_prime_above_exists_uniquePE0008 · initial_prime_chain_prefix_extendPE000A · initial_prime_chain_terminal_is_primePE000B · initial_prime_chain_bounded_existsPE000D · initial_prime_chain_strict_orderPE000E · initial_prime_chain_exhausts_primes