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
Prime(p)Exact expansion
~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1This 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
none
Used by definitions
Used by theorem statements or local proof propositions
BT0025 prime_two BT003F prime_or_composite BT003G prime_nonzero BT003H prime_decidable BT003K prime_divisor_exists_up_to BT003L prime_divisor_exists BT003M prime_divisor_eq_one_or_self BT003N euclid_prime_dvd_product BT006N prime_three BT008Q prime_coprime_or_divides BT008R prime_not_divides_coprime BT008S distinct_primes_coprime BT00AW prime_is_succ_succ BT00PR prime_strictly_above_decidable BT00PS bounded_prime_interval_search BT00QD prime_two_le BT00QF prime_power_exponent_le BT00QG prime_power_divides_exponent_le_value BT00QH power_valuation_successor_not_divides BT00QI power_valuation_selected_and_successor_not_divides BT00QN prime_power_successor_cancel_cofactor BT00QO prime_nondivisor_mul BT00QP power_valuation_exact_cofactor BT00QQ power_valuation_mul_successor_not_divides BT00QR power_valuation_mul_lower BT00QS power_valuation_mul_upper BT00QT prime_power_valuation_mul BT00RL prime_power_valuation_one_zero BT00RO prime_factorial_valuation_zero BT00RP prime_factorial_valuation_succ BT00S0 prime_power_quotient_prefix_exists BT00S2 prime_legendre_sum_exists BT00SA prime_power_quotient_tail_zero BT00SB prime_power_divides_exponent_le_valuation BT00SI valuation_threshold_bit_decides_power_divides BT00SK power_quotient_successor_pointwise_add BT00SS prime_power_quotient_prefix_last_zero BT00ST legendre_sum_zero_extended_prefix BT00SV prime_legendre_sum_succ BT00T0 factorial_legendre_successor_agreement BT00T1 prime_factorial_valuation_eq_legendre_sum BT00U5 primorial_factor_choice_exists BT00U6 primorial_factor_choice_functional BT00U7 primorial_factor_prefix_extend BT00U8 primorial_factor_prefix_exists BT00UA primorial_exists BT00UD primorial_succ_decompose BT00UE primorial_positive BT00UR primorial_interval_factor_prefix_extend BT00US primorial_interval_factor_prefix_exists BT00UW primorial_interval_factor_prefix_shift BT00UX primorial_factor_prefix_restrict_add BT00UY primorial_prefix_interval_split BT00VA factorial_prime_divides_of_le BT00VB factorial_prime_le_of_divides BT00VC choose_prime_divides_between BT00VE primorial_interval_pairwise_coprime BT00VF primorial_interval_divides_choose_between BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00VI primorial_even_interval_le_central BT00VJ primorial_odd_interval_le_middle BT00VQ primorial_one BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00VX central_binom_prime_divisor_le_double BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00XM central_binom_factorial_valuation_balance BT00XN central_binom_legendre_valuation_balance BT00XO prime_power_quotient_zero_of_exponent_gt BT00XP power_quotient_prefix_tail_entry_zero BT00XQ power_quotient_prefix_sum_extend_zero BT00XR legendre_sum_extended_prefix_exists BT00Y4 central_binom_carry_bit_count 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 BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients BT00YE central_binom_prime_valuation_zero_two_thirds_range BT00YG central_binom_prime_valuation_zero_above_third_quotient BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YJ no_bertrand_central_nonzero_valuation_live_ranges BT00YK no_bertrand_central_nonzero_valuation_factor_ranges 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 BT00YW prime_contribution_prefix_pairwise_coprime BT00YX prime_contribution_factor_divides BT00YY prime_contribution_product_divides BT0100 prime_contribution_selected_entry 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 BT0116 fixed_nontrivial_factor_not_prime BT0118 nonprime_has_small_prime_divisor_below_square BT0119 prime_of_no_small_prime_divisor_below_square BT011A prime_le_twenty_two_cases BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one BT011Q bertrand_covering_interval BT0124 bertrand_small_closed_upper BT0125 bertrand_closed_upper BT0126 bertrand_upper_endpoint_factorization BT0127 bertrand_strict