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.
Readable signature
Pow(a,e,z)Exact expansion
exists ff_b_defined_power ff_c_defined_power. ((forall ff_i_defined_power_repeat. (exists ff_lt_defined_power_repeat_bound. ff_lt_defined_power_repeat_bound + S ff_i_defined_power_repeat = e) -> (((exists ff_h_defined_power_repeat_decoded. ff_h_defined_power_repeat_decoded + S (a) = S ((S (ff_i_defined_power_repeat)) * ff_c_defined_power)) /\ exists ff_q_defined_power_repeat_decoded. ff_b_defined_power = ff_q_defined_power_repeat_decoded * S ((S (ff_i_defined_power_repeat)) * ff_c_defined_power) + (a)))) /\ (exists ff_u_defined_power_product ff_v_defined_power_product. ((((exists ff_h_defined_power_product_start. ff_h_defined_power_product_start + S (1) = S ((S (0)) * ff_v_defined_power_product)) /\ exists ff_q_defined_power_product_start. ff_u_defined_power_product = ff_q_defined_power_product_start * S ((S (0)) * ff_v_defined_power_product) + (1))) /\ ((((exists ff_h_defined_power_product_terminal. ff_h_defined_power_product_terminal + S (z) = S ((S (e)) * ff_v_defined_power_product)) /\ exists ff_q_defined_power_product_terminal. ff_u_defined_power_product = ff_q_defined_power_product_terminal * S ((S (e)) * ff_v_defined_power_product) + (z))) /\ forall ff_i_defined_power_product. (exists ff_lt_defined_power_product_bound. ff_lt_defined_power_product_bound + S ff_i_defined_power_product = e) -> exists ff_p_defined_power_product ff_r_defined_power_product ff_s_defined_power_product. ((((exists ff_h_defined_power_product_factor. ff_h_defined_power_product_factor + S (ff_p_defined_power_product) = S ((S (ff_i_defined_power_product)) * ff_c_defined_power)) /\ exists ff_q_defined_power_product_factor. ff_b_defined_power = ff_q_defined_power_product_factor * S ((S (ff_i_defined_power_product)) * ff_c_defined_power) + (ff_p_defined_power_product))) /\ ((((exists ff_h_defined_power_product_partial. ff_h_defined_power_product_partial + S (ff_r_defined_power_product) = S ((S (ff_i_defined_power_product)) * ff_v_defined_power_product)) /\ exists ff_q_defined_power_product_partial. ff_u_defined_power_product = ff_q_defined_power_product_partial * S ((S (ff_i_defined_power_product)) * ff_v_defined_power_product) + (ff_r_defined_power_product))) /\ ((((exists ff_h_defined_power_product_successor. ff_h_defined_power_product_successor + S (ff_s_defined_power_product) = S ((S (S ff_i_defined_power_product)) * ff_v_defined_power_product)) /\ exists ff_q_defined_power_product_successor. ff_u_defined_power_product = ff_q_defined_power_product_successor * S ((S (S ff_i_defined_power_product)) * ff_v_defined_power_product) + (ff_s_defined_power_product))) /\ ff_s_defined_power_product = ff_r_defined_power_product * ff_p_defined_power_product)))))))This node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
Used by theorem statements or local proof propositions
BT0080 pow_exists BT0081 pow_zero BT0082 pow_functional BT0083 pow_successor_decompose BT0093 pow_one_from_zero_successor BT0094 pow_one BT0095 pow_successor_pair_mul BT009V pow_two_from_one_successor BT009W pow_two BT009X pow_add BT00PY pow_base_monotone BT00Q0 one_le_pow BT00Q1 pow_nonzero_of_one_le BT00Q3 power_divides_decidable BT00Q4 power_divides_zero BT00QF prime_power_exponent_le BT00QK power_divides_exponent_antitone BT00QL power_divides_add_mul BT00QM power_divides_successor_of_cofactor BT00QN prime_power_successor_cancel_cofactor BT00QP power_valuation_exact_cofactor BT00QQ power_valuation_mul_successor_not_divides BT00QV pow_mul_base BT00QW pow_two_base_two_value_four BT00RL prime_power_valuation_one_zero BT00S0 prime_power_quotient_prefix_exists BT00S1 power_quotient_prefix_transport BT00S5 pow_successor_compose BT00SA prime_power_quotient_tail_zero BT00SJ power_quotient_prefix_decoded_divrem BT00SK power_quotient_successor_pointwise_add BT00SL pow_successor_compose_from_total BT00SM pow_mul_exp_from_total BT00SN pow_exponent_monotone_from_total BT00SO pow_two_seed_bundle_from_total BT00SS prime_power_quotient_prefix_last_zero BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00SY bertrand_hj_six_step_from_total BT00U1 pow_four_four_exact BT00U3 four_pow_central_seed_package BT00U4 four_pow_lt_mul_central_binom BT00VM central_binom_strong_upper_of_laws BT00VO central_binom_strong_upper BT00VP central_binom_odd_middle_le_four_pow BT00VT central_binom_nonzero_strong_upper BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00VW primorial_le_four_pow BT00W3 pow_block_bound_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WI pow_two_double_eq_pow_four_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WK pow_eleven_double_block_le_pow_two_seven_block_from_total BT00WL pow_eleven_double_block_le_pow_four_even_from_total BT00WM pow_eleven_double_block_le_pow_four_odd_from_total BT00WN pow_six_ten_block_le_pow_four_thirteen_block_from_total BT00WO pow_thirty_six_double_block_eq_pow_six_four_block_from_total BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00WW bertrand_hj_base_window_thirty_two_from_total BT00X2 bertrand_hj_six_block_iterate_from_total BT00X3 bertrand_hj_envelope_thirty_two BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT00X6 bertrand_main_inequality_factorized_from_total BT00X7 bertrand_main_inequality_factorized BT00X8 bertrand_main_inequality_nat BT00XA beta_product_uniform_le_pow BT00XJ pow_le_pow_of_exponent_le BT00XK pow_tail_strict_of_square BT00XO prime_power_quotient_zero_of_exponent_gt BT00XP power_quotient_prefix_tail_entry_zero BT00XV double_quotient_carry_choice BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00Y7 central_binom_prime_square_tail_valuation_le_one BT00YA prime_square_tail_of_two_three_range BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients BT00YE central_binom_prime_valuation_zero_two_thirds_range BT00YH floor_sqrt_above_root_power_two_strict BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT00YM no_bertrand_central_prime_contribution_ranges BT00YN prime_contribution_choice_exists BT00YO prime_contribution_choice_functional BT00YP prime_contribution_prefix_extend BT00YQ prime_contribution_prefix_exists BT00YS prime_contribution_product_exists BT00YU coprime_power_right BT00YV coprime_powers BT00YW prime_contribution_prefix_pairwise_coprime BT00YX prime_contribution_factor_divides BT00YY prime_contribution_product_divides BT0100 prime_contribution_selected_entry BT0101 prime_contribution_selected_successor_divides BT0102 prime_contribution_cofactor_prime_contradiction BT0103 prime_contribution_cofactor_eq_one BT0104 prime_contribution_reverse_divides BT0105 prime_contribution_product_eq BT0106 prime_contribution_complete_exists BT0107 central_binom_prime_contribution_product_exists BT0108 no_bertrand_central_contribution_choice_ranges BT010K prime_contribution_interval_prefix_extend BT010L prime_contribution_interval_prefix_exists BT010P prime_contribution_interval_prefix_shift BT010Q prime_contribution_prefix_restrict_add BT010R prime_contribution_prefix_interval_split BT010S prime_contribution_product_length_eq_transport BT010V no_bertrand_small_contribution_choice_le_double BT010W no_bertrand_middle_contribution_choice_le_selector BT010X no_bertrand_high_contribution_choice_eq_one BT010Y no_bertrand_small_contribution_product_le_power BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0112 no_bertrand_high_contribution_interval_eq_one BT0113 central_binom_factorization_small BT0114 central_binom_le_of_no_bertrand_prime BT0115 bertrand_eventually_closed_upper