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
∀ ppf_table_degree_prioritylayer. ¬ppf_table_degree_prioritylayer = 0 → Dvd(ppf_table_degree_prioritylayer,g) → ∃ x. BetaAt(b,c,ppf_table_degree_prioritylayer,x) ∧ Pow(x,ppf_table_degree_prioritylayer,n)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall ppf_table_degree_prioritylayer. ~(ppf_table_degree_prioritylayer = 0) -> (exists pvs_factor_prioritylayerdivisor. ((g)) = (ppf_table_degree_prioritylayer) * pvs_factor_prioritylayerdivisor) -> exists ppf_table_root_prioritylayer. (((exists ff_h_pvs_prioritylayerentry. ff_h_pvs_prioritylayerentry + S (ppf_table_root_prioritylayer) = S ((S (ppf_table_degree_prioritylayer)) * (c))) /\ exists ff_q_pvs_prioritylayerentry. (b) = ff_q_pvs_prioritylayerentry * S ((S (ppf_table_degree_prioritylayer)) * (c)) + (ppf_table_root_prioritylayer))) /\ (exists pa_b_pvs_prioritylayerpower pa_c_pvs_prioritylayerpower. ((forall pa_i_pvs_prioritylayerpower_repeat. (exists pa_lt_pvs_prioritylayerpower_repeat_bound. pa_lt_pvs_prioritylayerpower_repeat_bound + S pa_i_pvs_prioritylayerpower_repeat = ppf_table_degree_prioritylayer) -> (((exists pa_h_pvs_prioritylayerpower_repeat_decoded. pa_h_pvs_prioritylayerpower_repeat_decoded + S (ppf_table_root_prioritylayer) = S ((S (pa_i_pvs_prioritylayerpower_repeat)) * pa_c_pvs_prioritylayerpower)) /\ exists pa_q_pvs_prioritylayerpower_repeat_decoded. pa_b_pvs_prioritylayerpower = pa_q_pvs_prioritylayerpower_repeat_decoded * S ((S (pa_i_pvs_prioritylayerpower_repeat)) * pa_c_pvs_prioritylayerpower) + (ppf_table_root_prioritylayer)))) /\ (exists pa_u_pvs_prioritylayerpower_product pa_v_pvs_prioritylayerpower_product. ((((exists pa_h_pvs_prioritylayerpower_product_start. pa_h_pvs_prioritylayerpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayerpower_product)) /\ exists pa_q_pvs_prioritylayerpower_product_start. pa_u_pvs_prioritylayerpower_product = pa_q_pvs_prioritylayerpower_product_start * S ((S (0)) * pa_v_pvs_prioritylayerpower_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayerpower_product_terminal. pa_h_pvs_prioritylayerpower_product_terminal + S ((n)) = S ((S (ppf_table_degree_prioritylayer)) * pa_v_pvs_prioritylayerpower_product)) /\ exists pa_q_pvs_prioritylayerpower_product_terminal. pa_u_pvs_prioritylayerpower_product = pa_q_pvs_prioritylayerpower_product_terminal * S ((S (ppf_table_degree_prioritylayer)) * pa_v_pvs_prioritylayerpower_product) + ((n)))) /\ forall pa_i_pvs_prioritylayerpower_product. (exists pa_lt_pvs_prioritylayerpower_product_bound. pa_lt_pvs_prioritylayerpower_product_bound + S pa_i_pvs_prioritylayerpower_product = ppf_table_degree_prioritylayer) -> exists pa_p_pvs_prioritylayerpower_product pa_r_pvs_prioritylayerpower_product pa_s_pvs_prioritylayerpower_product. ((((exists pa_h_pvs_prioritylayerpower_product_factor. pa_h_pvs_prioritylayerpower_product_factor + S (pa_p_pvs_prioritylayerpower_product) = S ((S (pa_i_pvs_prioritylayerpower_product)) * pa_c_pvs_prioritylayerpower)) /\ exists pa_q_pvs_prioritylayerpower_product_factor. pa_b_pvs_prioritylayerpower = pa_q_pvs_prioritylayerpower_product_factor * S ((S (pa_i_pvs_prioritylayerpower_product)) * pa_c_pvs_prioritylayerpower) + (pa_p_pvs_prioritylayerpower_product))) /\ ((((exists pa_h_pvs_prioritylayerpower_product_partial. pa_h_pvs_prioritylayerpower_product_partial + S (pa_r_pvs_prioritylayerpower_product) = S ((S (pa_i_pvs_prioritylayerpower_product)) * pa_v_pvs_prioritylayerpower_product)) /\ exists pa_q_pvs_prioritylayerpower_product_partial. pa_u_pvs_prioritylayerpower_product = pa_q_pvs_prioritylayerpower_product_partial * S ((S (pa_i_pvs_prioritylayerpower_product)) * pa_v_pvs_prioritylayerpower_product) + (pa_r_pvs_prioritylayerpower_product))) /\ ((((exists pa_h_pvs_prioritylayerpower_product_successor. pa_h_pvs_prioritylayerpower_product_successor + S (pa_s_pvs_prioritylayerpower_product) = S ((S (S pa_i_pvs_prioritylayerpower_product)) * pa_v_pvs_prioritylayerpower_product)) /\ exists pa_q_pvs_prioritylayerpower_product_successor. pa_u_pvs_prioritylayerpower_product = pa_q_pvs_prioritylayerpower_product_successor * S ((S (S pa_i_pvs_prioritylayerpower_product)) * pa_v_pvs_prioritylayerpower_product) + (pa_s_pvs_prioritylayerpower_product))) /\ pa_s_pvs_prioritylayerpower_product = pa_r_pvs_prioritylayerpower_product * pa_p_pvs_prioritylayerpower_product))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.