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
∀ eutprod_index_prioritylayer. Lt(eutprod_index_prioritylayer,l) → ∃ x. ∃ y. ∃ z. BetaAt(pb,pc,eutprod_index_prioritylayer,x) ∧ (BetaAt(eb,ec,eutprod_index_prioritylayer,y) ∧ (BetaAt(fb,fc,eutprod_index_prioritylayer,z) ∧ EulerPrimePowerFactor(x,y,z)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall eutprod_index_prioritylayer. (exists eut_gap_prioritylayer_bound. eut_gap_prioritylayer_bound + S (eutprod_index_prioritylayer) = (l)) -> exists eutprod_prime_prioritylayer eutprod_exponent_prioritylayer eutprod_factor_prioritylayer. (((((exists fs_h_prioritylayer_prime. fs_h_prioritylayer_prime + S (eutprod_prime_prioritylayer) = S ((S (eutprod_index_prioritylayer)) * pc)) /\ exists fs_q_prioritylayer_prime. pb = fs_q_prioritylayer_prime * S ((S (eutprod_index_prioritylayer)) * pc) + (eutprod_prime_prioritylayer))) /\ (((((exists fs_h_prioritylayer_exponent. fs_h_prioritylayer_exponent + S (eutprod_exponent_prioritylayer) = S ((S (eutprod_index_prioritylayer)) * ec)) /\ exists fs_q_prioritylayer_exponent. eb = fs_q_prioritylayer_exponent * S ((S (eutprod_index_prioritylayer)) * ec) + (eutprod_exponent_prioritylayer))) /\ (((((exists fs_h_prioritylayer_factor. fs_h_prioritylayer_factor + S (eutprod_factor_prioritylayer) = S ((S (eutprod_index_prioritylayer)) * fc)) /\ exists fs_q_prioritylayer_factor. fb = fs_q_prioritylayer_factor * S ((S (eutprod_index_prioritylayer)) * fc) + (eutprod_factor_prioritylayer))) /\ (((~((eutprod_prime_prioritylayer)=1) /\ forall eutps_a_prioritylayer_arithmetic_prime eutps_b_prioritylayer_arithmetic_prime. (eutprod_prime_prioritylayer)=eutps_a_prioritylayer_arithmetic_prime*eutps_b_prioritylayer_arithmetic_prime -> eutps_a_prioritylayer_arithmetic_prime=1 \/ eutps_b_prioritylayer_arithmetic_prime=1) /\ (((~((eutprod_exponent_prioritylayer)=0)) /\ (exists eutprod_prime_predecessor_prioritylayer_arithmetic eutprod_exponent_predecessor_prioritylayer_arithmetic eutprod_previous_power_prioritylayer_arithmetic. (eutprod_prime_prioritylayer)=S eutprod_prime_predecessor_prioritylayer_arithmetic /\ ((eutprod_exponent_prioritylayer)=S eutprod_exponent_predecessor_prioritylayer_arithmetic /\ ((exists pa_b_euta_prioritylayer_arithmetic_power pa_c_euta_prioritylayer_arithmetic_power. ((forall pa_i_euta_prioritylayer_arithmetic_power_repeat. (exists pa_lt_euta_prioritylayer_arithmetic_power_repeat_bound. pa_lt_euta_prioritylayer_arithmetic_power_repeat_bound + S pa_i_euta_prioritylayer_arithmetic_power_repeat = eutprod_exponent_predecessor_prioritylayer_arithmetic) -> (((exists pa_h_euta_prioritylayer_arithmetic_power_repeat_decoded. pa_h_euta_prioritylayer_arithmetic_power_repeat_decoded + S (eutprod_prime_prioritylayer) = S ((S (pa_i_euta_prioritylayer_arithmetic_power_repeat)) * pa_c_euta_prioritylayer_arithmetic_power)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_repeat_decoded. pa_b_euta_prioritylayer_arithmetic_power = pa_q_euta_prioritylayer_arithmetic_power_repeat_decoded * S ((S (pa_i_euta_prioritylayer_arithmetic_power_repeat)) * pa_c_euta_prioritylayer_arithmetic_power) + (eutprod_prime_prioritylayer)))) /\ (exists pa_u_euta_prioritylayer_arithmetic_power_product pa_v_euta_prioritylayer_arithmetic_power_product. ((((exists pa_h_euta_prioritylayer_arithmetic_power_product_start. pa_h_euta_prioritylayer_arithmetic_power_product_start + S (1) = S ((S (0)) * pa_v_euta_prioritylayer_arithmetic_power_product)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_product_start. pa_u_euta_prioritylayer_arithmetic_power_product = pa_q_euta_prioritylayer_arithmetic_power_product_start * S ((S (0)) * pa_v_euta_prioritylayer_arithmetic_power_product) + (1))) /\ ((((exists pa_h_euta_prioritylayer_arithmetic_power_product_terminal. pa_h_euta_prioritylayer_arithmetic_power_product_terminal + S (eutprod_previous_power_prioritylayer_arithmetic) = S ((S (eutprod_exponent_predecessor_prioritylayer_arithmetic)) * pa_v_euta_prioritylayer_arithmetic_power_product)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_product_terminal. pa_u_euta_prioritylayer_arithmetic_power_product = pa_q_euta_prioritylayer_arithmetic_power_product_terminal * S ((S (eutprod_exponent_predecessor_prioritylayer_arithmetic)) * pa_v_euta_prioritylayer_arithmetic_power_product) + (eutprod_previous_power_prioritylayer_arithmetic))) /\ forall pa_i_euta_prioritylayer_arithmetic_power_product. (exists pa_lt_euta_prioritylayer_arithmetic_power_product_bound. pa_lt_euta_prioritylayer_arithmetic_power_product_bound + S pa_i_euta_prioritylayer_arithmetic_power_product = eutprod_exponent_predecessor_prioritylayer_arithmetic) -> exists pa_p_euta_prioritylayer_arithmetic_power_product pa_r_euta_prioritylayer_arithmetic_power_product pa_s_euta_prioritylayer_arithmetic_power_product. ((((exists pa_h_euta_prioritylayer_arithmetic_power_product_factor. pa_h_euta_prioritylayer_arithmetic_power_product_factor + S (pa_p_euta_prioritylayer_arithmetic_power_product) = S ((S (pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_c_euta_prioritylayer_arithmetic_power)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_product_factor. pa_b_euta_prioritylayer_arithmetic_power = pa_q_euta_prioritylayer_arithmetic_power_product_factor * S ((S (pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_c_euta_prioritylayer_arithmetic_power) + (pa_p_euta_prioritylayer_arithmetic_power_product))) /\ ((((exists pa_h_euta_prioritylayer_arithmetic_power_product_partial. pa_h_euta_prioritylayer_arithmetic_power_product_partial + S (pa_r_euta_prioritylayer_arithmetic_power_product) = S ((S (pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_v_euta_prioritylayer_arithmetic_power_product)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_product_partial. pa_u_euta_prioritylayer_arithmetic_power_product = pa_q_euta_prioritylayer_arithmetic_power_product_partial * S ((S (pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_v_euta_prioritylayer_arithmetic_power_product) + (pa_r_euta_prioritylayer_arithmetic_power_product))) /\ ((((exists pa_h_euta_prioritylayer_arithmetic_power_product_successor. pa_h_euta_prioritylayer_arithmetic_power_product_successor + S (pa_s_euta_prioritylayer_arithmetic_power_product) = S ((S (S pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_v_euta_prioritylayer_arithmetic_power_product)) /\ exists pa_q_euta_prioritylayer_arithmetic_power_product_successor. pa_u_euta_prioritylayer_arithmetic_power_product = pa_q_euta_prioritylayer_arithmetic_power_product_successor * S ((S (S pa_i_euta_prioritylayer_arithmetic_power_product)) * pa_v_euta_prioritylayer_arithmetic_power_product) + (pa_s_euta_prioritylayer_arithmetic_power_product))) /\ pa_s_euta_prioritylayer_arithmetic_power_product = pa_r_euta_prioritylayer_arithmetic_power_product * pa_p_euta_prioritylayer_arithmetic_power_product)))))))) /\ (eutprod_factor_prioritylayer)=eutprod_previous_power_prioritylayer_arithmetic*eutprod_prime_predecessor_prioritylayer_arithmetic)))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.