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) ∧ (¬e = 0 ∧ (∃ x. ∃ y. ∃ z. p = S x ∧ (e = S y ∧ (Pow(p,y,z) ∧ c = z · x))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~((p)=1) /\ forall eutps_a_prioritylayer_prime eutps_b_prioritylayer_prime. (p)=eutps_a_prioritylayer_prime*eutps_b_prioritylayer_prime -> eutps_a_prioritylayer_prime=1 \/ eutps_b_prioritylayer_prime=1) /\ (((~((e)=0)) /\ (exists eutprod_prime_predecessor_prioritylayer eutprod_exponent_predecessor_prioritylayer eutprod_previous_power_prioritylayer. (p)=S eutprod_prime_predecessor_prioritylayer /\ ((e)=S eutprod_exponent_predecessor_prioritylayer /\ ((exists pa_b_euta_prioritylayer_power pa_c_euta_prioritylayer_power. ((forall pa_i_euta_prioritylayer_power_repeat. (exists pa_lt_euta_prioritylayer_power_repeat_bound. pa_lt_euta_prioritylayer_power_repeat_bound + S pa_i_euta_prioritylayer_power_repeat = eutprod_exponent_predecessor_prioritylayer) -> (((exists pa_h_euta_prioritylayer_power_repeat_decoded. pa_h_euta_prioritylayer_power_repeat_decoded + S (p) = S ((S (pa_i_euta_prioritylayer_power_repeat)) * pa_c_euta_prioritylayer_power)) /\ exists pa_q_euta_prioritylayer_power_repeat_decoded. pa_b_euta_prioritylayer_power = pa_q_euta_prioritylayer_power_repeat_decoded * S ((S (pa_i_euta_prioritylayer_power_repeat)) * pa_c_euta_prioritylayer_power) + (p)))) /\ (exists pa_u_euta_prioritylayer_power_product pa_v_euta_prioritylayer_power_product. ((((exists pa_h_euta_prioritylayer_power_product_start. pa_h_euta_prioritylayer_power_product_start + S (1) = S ((S (0)) * pa_v_euta_prioritylayer_power_product)) /\ exists pa_q_euta_prioritylayer_power_product_start. pa_u_euta_prioritylayer_power_product = pa_q_euta_prioritylayer_power_product_start * S ((S (0)) * pa_v_euta_prioritylayer_power_product) + (1))) /\ ((((exists pa_h_euta_prioritylayer_power_product_terminal. pa_h_euta_prioritylayer_power_product_terminal + S (eutprod_previous_power_prioritylayer) = S ((S (eutprod_exponent_predecessor_prioritylayer)) * pa_v_euta_prioritylayer_power_product)) /\ exists pa_q_euta_prioritylayer_power_product_terminal. pa_u_euta_prioritylayer_power_product = pa_q_euta_prioritylayer_power_product_terminal * S ((S (eutprod_exponent_predecessor_prioritylayer)) * pa_v_euta_prioritylayer_power_product) + (eutprod_previous_power_prioritylayer))) /\ forall pa_i_euta_prioritylayer_power_product. (exists pa_lt_euta_prioritylayer_power_product_bound. pa_lt_euta_prioritylayer_power_product_bound + S pa_i_euta_prioritylayer_power_product = eutprod_exponent_predecessor_prioritylayer) -> exists pa_p_euta_prioritylayer_power_product pa_r_euta_prioritylayer_power_product pa_s_euta_prioritylayer_power_product. ((((exists pa_h_euta_prioritylayer_power_product_factor. pa_h_euta_prioritylayer_power_product_factor + S (pa_p_euta_prioritylayer_power_product) = S ((S (pa_i_euta_prioritylayer_power_product)) * pa_c_euta_prioritylayer_power)) /\ exists pa_q_euta_prioritylayer_power_product_factor. pa_b_euta_prioritylayer_power = pa_q_euta_prioritylayer_power_product_factor * S ((S (pa_i_euta_prioritylayer_power_product)) * pa_c_euta_prioritylayer_power) + (pa_p_euta_prioritylayer_power_product))) /\ ((((exists pa_h_euta_prioritylayer_power_product_partial. pa_h_euta_prioritylayer_power_product_partial + S (pa_r_euta_prioritylayer_power_product) = S ((S (pa_i_euta_prioritylayer_power_product)) * pa_v_euta_prioritylayer_power_product)) /\ exists pa_q_euta_prioritylayer_power_product_partial. pa_u_euta_prioritylayer_power_product = pa_q_euta_prioritylayer_power_product_partial * S ((S (pa_i_euta_prioritylayer_power_product)) * pa_v_euta_prioritylayer_power_product) + (pa_r_euta_prioritylayer_power_product))) /\ ((((exists pa_h_euta_prioritylayer_power_product_successor. pa_h_euta_prioritylayer_power_product_successor + S (pa_s_euta_prioritylayer_power_product) = S ((S (S pa_i_euta_prioritylayer_power_product)) * pa_v_euta_prioritylayer_power_product)) /\ exists pa_q_euta_prioritylayer_power_product_successor. pa_u_euta_prioritylayer_power_product = pa_q_euta_prioritylayer_power_product_successor * S ((S (S pa_i_euta_prioritylayer_power_product)) * pa_v_euta_prioritylayer_power_product) + (pa_s_euta_prioritylayer_power_product))) /\ pa_s_euta_prioritylayer_power_product = pa_r_euta_prioritylayer_power_product * pa_p_euta_prioritylayer_power_product)))))))) /\ (c)=eutprod_previous_power_prioritylayer*eutprod_prime_predecessor_prioritylayer))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.