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
Dvd(d,n)Exact expansion
exists k. n = d * kThis 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
BT001V zero_remainder_implies_multiple BT001W multiple_has_zero_remainder BT0026 multiple_zero BT0027 one_multiple BT0028 multiple_refl BT002A multiple_mul_right BT002B multiple_mul_left BT002C multiple_trans BT002D divisor_le_nonzero BT002E divisor_one BT002F multiple_antisymm BT002G factor_difference BT002H divides_remainder BT002I divides_linear_step BT0031 is_gcd_one_to_coprime BT0037 common_divisor_divides_balanced_result BT0039 gauss_coprime_cancel BT003B multiple_decidable_nonzero BT003C multiple_decidable BT003E factor_search_up_to BT003K prime_divisor_exists_up_to BT003L prime_divisor_exists BT003M prime_divisor_eq_one_or_self BT003N euclid_prime_dvd_product BT0046 dvd_to_mod_zero BT004I beta_modulus_coprime_base BT004J common_divisor_beta_moduli_divides_gap_times_c BT004K beta_moduli_coprime_of_gap_dvd BT004M bounded_common_multiple_step BT004N bounded_common_multiple_exists BT004O beta_moduli_coprime_of_lt_bounded_common_multiple BT004P beta_moduli_pairwise_coprime_bounded BT004R coprime_mul_left BT004T mod_eq_of_mod_eq_multiple BT004U binary_crt_fold_step BT004V right_factor_divides_product BT0056 scaled_bounded_common_multiple BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005B beta_exclusive_recode_invariant_step BT005C bounded_beta_exclusive_recode_invariant BT005D beta_prefix_extend BT0069 beta_factor_divides_product BT008Q prime_coprime_or_divides BT008R prime_not_divides_coprime BT008S distinct_primes_coprime BT00BG coprime_product_is_lcm BT00Q3 power_divides_decidable BT00QM power_divides_successor_of_cofactor BT00QN prime_power_successor_cancel_cofactor BT00QO prime_nondivisor_mul BT00QP power_valuation_exact_cofactor BT00QQ power_valuation_mul_successor_not_divides BT00RD mul_le_cancel_left_nonzero BT00SH division_successor_quotient_by_bit BT00SK power_quotient_successor_pointwise_add BT00VA factorial_prime_divides_of_le BT00VB factorial_prime_le_of_divides BT00VC choose_prime_divides_between BT00VD beta_pairwise_coprime_product_divides_common_multiple 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 BT00VX central_binom_prime_divisor_le_double BT00VY no_bertrand_central_prime_divisor_le BT00W0 power_valuation_nonzero_exponent_divides_base BT00W2 no_bertrand_central_prime_divisor_ranges BT00YJ no_bertrand_central_nonzero_valuation_live_ranges 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 BT0118 nonprime_has_small_prime_divisor_below_square BT0119 prime_of_no_small_prime_divisor_below_square BT011B nonzero_remainder_not_multiple