Structure primeTheory
signature primeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val coprimes_by_def : thm
val divisors_def : thm
val gcd_matches_def : thm
val halves_def_primitive : thm
val lcm_fun_def : thm
val multiples_upto_def : thm
val perfect_power_def : thm
val phi_def : thm
val power_free_def : thm
val power_free_test_def : thm
val power_free_upto_def : thm
val prime_divisors_def : thm
val prime_factors_def : thm
val prime_power_divisors_def : thm
val prime_power_index_def : thm
val prime_powers_upto_def : thm
val prime_test_def : thm
val primes_upto_def : thm
val rec_phi_def_primitive : thm
val square_def : thm
val square_free_def : thm
val ulog_def : thm
(* Theorems *)
val Gauss_little_thm : thm
val LOG2_BY_HALF : thm
val LOG2_DIV_EXP : thm
val LOG2_HALF : thm
val LOG2_SUC_TIMES_SQ_DIV_2_POS : thm
val LOG2_compute : thm
val LOG_SUC : thm
val ROOT_EQN : thm
val SQRT_LE_IMP : thm
val SQRT_LE_SELF : thm
val SQRT_MULT_LE : thm
val SQRT_SQ : thm
val SQ_SQRT_LE : thm
val SQ_SQRT_LE_alt : thm
val SQ_SQRT_LT : thm
val SQ_SQRT_LT_alt : thm
val basic_prime_factorisation : thm
val common_prime_divisors_element : thm
val common_prime_divisors_finite : thm
val common_prime_divisors_min_image_pairwise_coprime : thm
val common_prime_divisors_pairwise_coprime : thm
val coprimes_by_0 : thm
val coprimes_by_by_0 : thm
val coprimes_by_by_1 : thm
val coprimes_by_by_divisor : thm
val coprimes_by_by_last : thm
val coprimes_by_divisors_card : thm
val coprimes_by_element : thm
val coprimes_by_eq_empty : thm
val coprimes_by_finite : thm
val coprimes_by_with_card : thm
val coprimes_eq_Euler : thm
val coprimes_from_not_1_inj : thm
val coprimes_map_cross_inj : thm
val coprimes_mult_by_image : thm
val coprimes_prime : thm
val coprimes_prime_power : thm
val coprimes_thm : thm
val count_up_def : thm
val count_up_exit : thm
val count_up_exit_eqn : thm
val count_up_ind : thm
val count_up_suc : thm
val count_up_suc_eqn : thm
val divisor_gt_cofactor_le : thm
val divisor_le_cofactor_ge : thm
val divisor_prime_factorisation : thm
val divisors_0 : thm
val divisors_1 : thm
val divisors_card_upper : thm
val divisors_cofactor_inj : thm
val divisors_delete_last : thm
val divisors_divisors_bij : thm
val divisors_element : thm
val divisors_element_alt : thm
val divisors_eq_empty : thm
val divisors_eq_gcd_image : thm
val divisors_eq_image_gcd_count : thm
val divisors_eq_image_gcd_natural : thm
val divisors_eq_image_gcd_upto : thm
val divisors_eqn : thm
val divisors_finite : thm
val divisors_has_1 : thm
val divisors_has_cofactor : thm
val divisors_has_element : thm
val divisors_has_factor : thm
val divisors_has_last : thm
val divisors_nonzero : thm
val divisors_not_empty : thm
val divisors_subset_natural : thm
val even_sq_free_element : thm
val even_sq_free_finite : thm
val even_sq_free_subset : thm
val exp_to_ulog : thm
val factor_seek_bound : thm
val factor_seek_def : thm
val factor_seek_ind : thm
val factor_seek_thm : thm
val gcd_eq_count_partition_by_divisors : thm
val gcd_eq_equiv_class : thm
val gcd_eq_equiv_class_fun : thm
val gcd_eq_equiv_on_count : thm
val gcd_eq_equiv_on_natural : thm
val gcd_eq_equiv_on_upto : thm
val gcd_eq_natural_partition_by_divisors : thm
val gcd_eq_partition_by_divisors : thm
val gcd_eq_upto_partition_by_divisors : thm
val gcd_matches_0 : thm
val gcd_matches_1 : thm
val gcd_matches_alt : thm
val gcd_matches_and_coprimes_by_same_size : thm
val gcd_matches_bij_coprimes : thm
val gcd_matches_bij_coprimes_by : thm
val gcd_matches_divisor_element : thm
val gcd_matches_element : thm
val gcd_matches_element_divides : thm
val gcd_matches_eq_empty : thm
val gcd_matches_finite : thm
val gcd_matches_from_divisors_inj : thm
val gcd_matches_has_divisor : thm
val gcd_matches_subset : thm
val gcd_matches_with_0 : thm
val gcd_park_decompose : thm
val gcd_park_decomposition : thm
val gcd_prime_factorisation : thm
val gcd_prime_power_cofactor_coprime : thm
val gcd_prime_power_divisibility : thm
val gcd_prime_power_factor : thm
val gcd_prime_power_factor_divides_gcd : thm
val gcd_prime_power_index : thm
val halves_0 : thm
val halves_1 : thm
val halves_2 : thm
val halves_alt : thm
val halves_by_LOG2 : thm
val halves_def : thm
val halves_eq_0 : thm
val halves_eq_1 : thm
val halves_ind : thm
val halves_le : thm
val halves_pos : thm
val lcm_fun_0 : thm
val lcm_fun_1 : thm
val lcm_fun_2 : thm
val lcm_fun_SUC : thm
val lcm_fun_compute : thm
val lcm_fun_lower_bound : thm
val lcm_fun_lower_bound_alt : thm
val lcm_fun_suc_none : thm
val lcm_fun_suc_some : thm
val lcm_gcd_park_decompose : thm
val lcm_park_decompose : thm
val lcm_park_decomposition : thm
val lcm_prime_factorisation : thm
val lcm_prime_power_cofactor_coprime : thm
val lcm_prime_power_divisibility : thm
val lcm_prime_power_factor : thm
val lcm_prime_power_factor_divides_lcm : thm
val lcm_prime_power_index : thm
val lcm_run_eq_prod_set_prime_powers : thm
val lcm_run_eq_set_lcm_prime_powers : thm
val lcm_run_lower_by_primes_count : thm
val lcm_run_lower_by_primes_product : thm
val lcm_run_upper_by_primes_count : thm
val lcm_special_for_coprime_factors : thm
val lcm_special_for_prime_power : thm
val less_divisors_0 : thm
val less_divisors_1 : thm
val less_divisors_element : thm
val less_divisors_finite : thm
val less_divisors_has_1 : thm
val less_divisors_has_cofactor : thm
val less_divisors_max : thm
val less_divisors_min : thm
val less_divisors_nonzero : thm
val less_divisors_prime : thm
val less_divisors_subset_divisors : thm
val less_divisors_subset_natural : thm
val list_lcm_by_last_non_prime_power : thm
val list_lcm_by_last_prime_power : thm
val list_lcm_eq_lcm_fun : thm
val list_lcm_option_last_non_prime_power : thm
val list_lcm_option_last_prime_power : thm
val list_lcm_option_recurrence : thm
val list_lcm_prime_power_divisibility : thm
val list_lcm_prime_power_factor_divides : thm
val list_lcm_prime_power_factor_member : thm
val list_lcm_prime_power_index : thm
val list_lcm_prime_power_index_lower : thm
val list_lcm_recurrence : thm
val list_lcm_with_last_non_prime_power : thm
val list_lcm_with_last_prime_power : thm
val multiples_upto_0_n : thm
val multiples_upto_1_n : thm
val multiples_upto_alt : thm
val multiples_upto_card : thm
val multiples_upto_element : thm
val multiples_upto_element_alt : thm
val multiples_upto_eqn : thm
val multiples_upto_finite : thm
val multiples_upto_m_0 : thm
val multiples_upto_m_1 : thm
val multiples_upto_subset : thm
val multiples_upto_thm : thm
val non_prime_power_coprime_factors : thm
val non_sq_free_element : thm
val non_sq_free_finite : thm
val non_sq_free_subset : thm
val odd_sq_free_element : thm
val odd_sq_free_finite : thm
val odd_sq_free_subset : thm
val odd_square_lt : thm
val pairwise_coprime_for_prime_powers : thm
val park_off_alt : thm
val park_off_element : thm
val park_off_image_has_not_1 : thm
val park_off_subset_common : thm
val park_off_subset_total : thm
val park_on_element : thm
val park_on_off_common_image_partition : thm
val park_on_off_partition : thm
val park_on_off_total_image_partition : thm
val park_on_subset_common : thm
val park_on_subset_total : thm
val perfect_power_0_m : thm
val perfect_power_1_m : thm
val perfect_power_2_odd : thm
val perfect_power_bound_LOG2 : thm
val perfect_power_bound_ulog : thm
val perfect_power_cofactor : thm
val perfect_power_cofactor_alt : thm
val perfect_power_condition : thm
val perfect_power_half_inequality_1 : thm
val perfect_power_half_inequality_2 : thm
val perfect_power_mod_eq_0 : thm
val perfect_power_mod_ne_0 : thm
val perfect_power_n_0 : thm
val perfect_power_n_1 : thm
val perfect_power_not_suc : thm
val perfect_power_self : thm
val perfect_power_special_inequality : thm
val perfect_power_suc : thm
val perfect_power_test : thm
val phi_0 : thm
val phi_1 : thm
val phi_2 : thm
val phi_eq_0 : thm
val phi_eq_totient : thm
val phi_fun : thm
val phi_gt_1 : thm
val phi_le : thm
val phi_lt : thm
val phi_mult : thm
val phi_pos : thm
val phi_prime : thm
val phi_prime_power : thm
val phi_prime_sq : thm
val phi_primes : thm
val phi_primes_distinct : thm
val phi_thm : thm
val power_free_0 : thm
val power_free_1 : thm
val power_free_2 : thm
val power_free_3 : thm
val power_free_alt : thm
val power_free_by_power_index_LOG2 : thm
val power_free_by_power_index_ulog : thm
val power_free_check_all : thm
val power_free_check_upto : thm
val power_free_check_upto_LOG2 : thm
val power_free_check_upto_ulog : thm
val power_free_gt_1 : thm
val power_free_perfect_power : thm
val power_free_property : thm
val power_free_test_eqn : thm
val power_free_test_upto_LOG2 : thm
val power_free_test_upto_ulog : thm
val power_free_upto_0 : thm
val power_free_upto_1 : thm
val power_free_upto_suc : thm
val power_index_0 : thm
val power_index_1 : thm
val power_index_def : thm
val power_index_eqn : thm
val power_index_equal : thm
val power_index_exact_root : thm
val power_index_ind : thm
val power_index_lower : thm
val power_index_no_exact_roots : thm
val power_index_not_exact_root : thm
val power_index_of_1 : thm
val power_index_pos : thm
val power_index_property : thm
val power_index_root : thm
val power_index_upper : thm
val prime_by_sqrt_factors : thm
val prime_divisors_0 : thm
val prime_divisors_0_not_sing : thm
val prime_divisors_1 : thm
val prime_divisors_common_divisor : thm
val prime_divisors_common_multiple : thm
val prime_divisors_divisor_subset : thm
val prime_divisors_element : thm
val prime_divisors_empty_iff : thm
val prime_divisors_finite : thm
val prime_divisors_nonempty : thm
val prime_divisors_prime : thm
val prime_divisors_prime_power : thm
val prime_divisors_sing : thm
val prime_divisors_sing_alt : thm
val prime_divisors_sing_property : thm
val prime_divisors_subset_natural : thm
val prime_divisors_subset_prime : thm
val prime_factor_estimate : thm
val prime_factorisation : thm
val prime_factors_element : thm
val prime_factors_finite : thm
val prime_factors_subset : thm
val prime_is_power_free : thm
val prime_non_square : thm
val prime_power_cofactor_coprime : thm
val prime_power_divisibility : thm
val prime_power_divisors_1 : thm
val prime_power_divisors_element : thm
val prime_power_divisors_element_alt : thm
val prime_power_divisors_finite : thm
val prime_power_divisors_pairwise_coprime : thm
val prime_power_eqn : thm
val prime_power_factor_divides : thm
val prime_power_index_1 : thm
val prime_power_index_common_divisor : thm
val prime_power_index_common_multiple : thm
val prime_power_index_eq_0 : thm
val prime_power_index_eqn : thm
val prime_power_index_exists : thm
val prime_power_index_le_log_index : thm
val prime_power_index_maximal : thm
val prime_power_index_of_divisor : thm
val prime_power_index_pos : thm
val prime_power_index_prime : thm
val prime_power_index_prime_power : thm
val prime_power_index_suc_property : thm
val prime_power_index_suc_special : thm
val prime_power_index_test : thm
val prime_power_or_coprime_factors : thm
val prime_powers_upto_0 : thm
val prime_powers_upto_1 : thm
val prime_powers_upto_element : thm
val prime_powers_upto_element_alt : thm
val prime_powers_upto_finite : thm
val prime_powers_upto_lcm_divisor : thm
val prime_powers_upto_lcm_prime_divisor : thm
val prime_powers_upto_lcm_prime_to_log_divisor : thm
val prime_powers_upto_lcm_prime_to_power_divisor : thm
val prime_powers_upto_list_mem : thm
val prime_powers_upto_pairwise_coprime : thm
val prime_powers_upto_prod_set_ge : thm
val prime_powers_upto_prod_set_le : thm
val prime_powers_upto_prod_set_mix_ge : thm
val prime_test_thm : thm
val primes_count_0 : thm
val primes_count_1 : thm
val primes_count_upper_by_lcm_run : thm
val primes_count_upper_by_product : thm
val primes_upto_0 : thm
val primes_upto_1 : thm
val primes_upto_element : thm
val primes_upto_finite : thm
val primes_upto_pairwise_coprime : thm
val primes_upto_subset_natural : thm
val proper_divisors_0 : thm
val proper_divisors_1 : thm
val proper_divisors_by_less_divisors : thm
val proper_divisors_element : thm
val proper_divisors_finite : thm
val proper_divisors_has_cofactor : thm
val proper_divisors_max_min : thm
val proper_divisors_min_gt_1 : thm
val proper_divisors_not_1 : thm
val proper_divisors_prime : thm
val proper_divisors_subset : thm
val rec_phi_0 : thm
val rec_phi_1 : thm
val rec_phi_def : thm
val rec_phi_eq_phi : thm
val rec_phi_ind : thm
val self_to_log_index_member : thm
val set_lcm_prime_powers_upto_eqn : thm
val sigma_eq_perfect_power_bounds_1 : thm
val sigma_eq_perfect_power_bounds_2 : thm
val sq_free_disjoint : thm
val sq_free_disjoint_even_odd : thm
val sq_free_element : thm
val sq_free_finite : thm
val sq_free_inter : thm
val sq_free_inter_even_odd : thm
val sq_free_split : thm
val sq_free_split_even_odd : thm
val sq_free_subset : thm
val sq_free_union : thm
val sq_free_union_even_odd : thm
val sqrt_upper : thm
val square_0 : thm
val square_1 : thm
val square_alt : thm
val square_eqn : thm
val square_free_1 : thm
val square_free_prime : thm
val sum_image_divisors_cong : thm
val sum_over_count_by_divisors : thm
val sum_over_count_by_gcd_partition : thm
val sum_over_natural_by_divisors : thm
val sum_over_natural_by_gcd_partition : thm
val sum_over_natural_by_preimage_divisors : thm
val sum_over_upto_by_divisors : thm
val sum_over_upto_by_gcd_partition : thm
val total_prime_divisors_element : thm
val total_prime_divisors_finite : thm
val total_prime_divisors_max_image_pairwise_coprime : thm
val total_prime_divisors_pairwise_coprime : thm
val two_factors_property : thm
val two_factors_property_1 : thm
val two_factors_property_2 : thm
val ulog_0 : thm
val ulog_1 : thm
val ulog_2 : thm
val ulog_2_exp : thm
val ulog_LOG2 : thm
val ulog_alt : thm
val ulog_def_alt : thm
val ulog_eq_0 : thm
val ulog_eq_1 : thm
val ulog_eq_self : thm
val ulog_eqn : thm
val ulog_even : thm
val ulog_exp : thm
val ulog_exp_exact : thm
val ulog_exp_not_exact : thm
val ulog_ge_1 : thm
val ulog_half : thm
val ulog_le : thm
val ulog_le_1 : thm
val ulog_le_self : thm
val ulog_lt : thm
val ulog_lt_self : thm
val ulog_mult : thm
val ulog_odd : thm
val ulog_pos : thm
val ulog_property : thm
val ulog_property_not_exact : thm
val ulog_property_odd : thm
val ulog_sq_gt_1 : thm
val ulog_suc : thm
val ulog_thm : thm
val ulog_twice_sq : thm
val ulog_unique : thm
(*
[combinatorics] Parent theory of "prime"
[coprimes_by_def] Definition
⊢ ∀n d.
coprimes_by n d =
if 0 < n ∧ d divides n then coprimes (n DIV d) else ∅
[divisors_def] Definition
⊢ ∀n. divisors n = {d | 0 < d ∧ d ≤ n ∧ d divides n}
[gcd_matches_def] Definition
⊢ ∀n d. gcd_matches n d = {j | j ∈ natural n ∧ gcd j n = d}
[halves_def_primitive] Definition
⊢ halves =
WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R (HALF n) n)
(λhalves a. I (if a = 0 then 0 else SUC (halves (HALF a))))
[lcm_fun_def] Definition
⊢ lcm_fun 0 = 1 ∧
∀n. lcm_fun (SUC n) =
if n = 0 then 1
else
case some p. ∃k. 0 < k ∧ prime p ∧ SUC n = p ** k of
NONE => lcm_fun n
| SOME p => p * lcm_fun n
[multiples_upto_def] Definition
⊢ ∀m n. m multiples_upto n = {x | m divides x ∧ 0 < x ∧ x ≤ n}
[perfect_power_def] Definition
⊢ ∀n m. n power_of m ⇔ ∃e. n = m ** e
[phi_def] Definition
⊢ ∀n. phi n = CARD (coprimes n)
[power_free_def] Definition
⊢ ∀n. power_free n ⇔ ∀m e. n = m ** e ⇒ m = n ∧ e = 1
[power_free_test_def] Definition
⊢ ∀n. power_free_test n ⇔ 1 < n ∧ n power_free_upto ulog n
[power_free_upto_def] Definition
⊢ ∀n k. n power_free_upto k ⇔ ∀j. 1 < j ∧ j ≤ k ⇒ ROOT j n ** j ≠ n
[prime_divisors_def] Definition
⊢ ∀n. prime_divisors n = {p | prime p ∧ p divides n}
[prime_factors_def] Definition
⊢ ∀n. prime_factors n = {p | prime p ∧ p ∈ divisors n}
[prime_power_divisors_def] Definition
⊢ ∀n. prime_power_divisors n =
IMAGE (λp. p ** ppidx n) (prime_divisors n)
[prime_power_index_def] Definition
⊢ ∀p n.
0 < n ∧ prime p ⇒
p ** ppidx n divides n ∧ coprime p (n DIV p ** ppidx n)
[prime_powers_upto_def] Definition
⊢ ∀n. prime_powers_upto n = IMAGE (λp. p ** LOG p n) (primes_upto n)
[prime_test_def] Definition
⊢ ∀n. prime_test n ⇔
if n ≤ 1 then F else factor_seek n (1 + SQRT n) 2 = n
[primes_upto_def] Definition
⊢ ∀n. primes_upto n = {p | prime p ∧ p ≤ n}
[rec_phi_def_primitive] Definition
⊢ rec_phi =
WFREC
(@R. WF R ∧
∀n a. n ≠ 0 ∧ n ≠ 1 ∧ a ∈ {m | m < n ∧ m divides n} ⇒ R a n)
(λrec_phi a'.
I
(if a' = 0 then 0
else if a' = 1 then 1
else a' − ∑ (λa. rec_phi a) {m | m < a' ∧ m divides a'}))
[square_def] Definition
⊢ ∀n. square n ⇔ ∃k. n = SQ k
[square_free_def] Definition
⊢ ∀n. square_free n ⇔ ∀p. prime p ∧ p divides n ⇒ ¬(SQ p divides n)
[ulog_def] Definition
⊢ ∀n. ulog n = count_up n 1 0
[Gauss_little_thm] Theorem
⊢ ∀n. ∑ phi (divisors n) = n
[LOG2_BY_HALF] Theorem
⊢ ∀n. 1 < n ⇒ LOG2 n = 1 + LOG2 (HALF n)
[LOG2_DIV_EXP] Theorem
⊢ ∀n m. 2 ** m < n ⇒ LOG2 (n DIV 2 ** m) = LOG2 n − m
[LOG2_HALF] Theorem
⊢ ∀n. 1 < n ⇒ LOG2 (HALF n) = LOG2 n − 1
[LOG2_SUC_TIMES_SQ_DIV_2_POS] Theorem
⊢ ∀n m. 1 < m ⇒ 0 < SUC (LOG2 n) * HALF m²
[LOG2_compute] Theorem
⊢ ∀n. LOG2 n = if n = 0 then LOG2 0 else halves n − 1
[LOG_SUC] Theorem
⊢ ∀b n.
1 < b ∧ 0 < n ⇒
LOG b (SUC n) = LOG b n + if SUC n power_of b then 1 else 0
[ROOT_EQN] Theorem
⊢ ∀r n.
0 < r ⇒
ROOT r n =
(let
m = TWICE (ROOT r (n DIV 2 ** r))
in
m + if (m + 1) ** r ≤ n then 1 else 0)
[SQRT_LE_IMP] Theorem
⊢ ∀n m. SQRT n ≤ m ⇒ n ≤ 3 * m²
[SQRT_LE_SELF] Theorem
⊢ ∀n. SQRT n ≤ n
[SQRT_MULT_LE] Theorem
⊢ ∀n m. SQRT n * SQRT m ≤ SQRT (n * m)
[SQRT_SQ] Theorem
⊢ ∀n. SQRT (SQ n) = n
[SQ_SQRT_LE] Theorem
⊢ ∀n. SQ (SQRT n) ≤ n
[SQ_SQRT_LE_alt] Theorem
⊢ ∀n. (SQRT n)² ≤ n
[SQ_SQRT_LT] Theorem
⊢ ∀n. ¬square n ⇒ SQ (SQRT n) < n
[SQ_SQRT_LT_alt] Theorem
⊢ ∀n. ¬square n ⇒ (SQRT n)² < n
[basic_prime_factorisation] Theorem
⊢ ∀n. 0 < n ⇒
n = PROD_SET (IMAGE (λp. p ** ppidx n) (prime_divisors n))
[common_prime_divisors_element] Theorem
⊢ ∀m n p.
p ∈ common_prime_divisors m n ⇔
p ∈ prime_divisors m ∧ p ∈ prime_divisors n
[common_prime_divisors_finite] Theorem
⊢ ∀m n. 0 < m ∧ 0 < n ⇒ FINITE (common_prime_divisors m n)
[common_prime_divisors_min_image_pairwise_coprime] Theorem
⊢ ∀m n x y.
x ∈
IMAGE (λp. p ** MIN (ppidx m) (ppidx n))
(common_prime_divisors m n) ∧
y ∈
IMAGE (λp. p ** MIN (ppidx m) (ppidx n))
(common_prime_divisors m n) ∧ x ≠ y ⇒
coprime x y
[common_prime_divisors_pairwise_coprime] Theorem
⊢ ∀m n x y.
x ∈ common_prime_divisors m n ∧ y ∈ common_prime_divisors m n ∧
x ≠ y ⇒
coprime x y
[coprimes_by_0] Theorem
⊢ ∀d. coprimes_by 0 d = ∅
[coprimes_by_by_0] Theorem
⊢ ∀n. coprimes_by n 0 = ∅
[coprimes_by_by_1] Theorem
⊢ ∀n. 0 < n ⇒ coprimes_by n 1 = coprimes n
[coprimes_by_by_divisor] Theorem
⊢ ∀n d. 0 < n ∧ d divides n ⇒ coprimes_by n d = coprimes (n DIV d)
[coprimes_by_by_last] Theorem
⊢ ∀n. 0 < n ⇒ coprimes_by n n = {1}
[coprimes_by_divisors_card] Theorem
⊢ ∀n x.
x ∈ divisors n ⇒ (CARD ∘ coprimes_by n) x = (λd. phi (n DIV d)) x
[coprimes_by_element] Theorem
⊢ ∀n d j.
j ∈ coprimes_by n d ⇔
0 < n ∧ d divides n ∧ j ∈ coprimes (n DIV d)
[coprimes_by_eq_empty] Theorem
⊢ ∀n d. 0 < n ⇒ (coprimes_by n d = ∅ ⇔ ¬(d divides n))
[coprimes_by_finite] Theorem
⊢ ∀n d. FINITE (coprimes_by n d)
[coprimes_by_with_card] Theorem
⊢ ∀n. 0 < n ⇒
CARD ∘ coprimes_by n =
(λd. phi (if d ∈ divisors n then n DIV d else 0))
[coprimes_eq_Euler] Theorem
⊢ ∀n. 1 < n ⇒ coprimes n = Euler n
[coprimes_from_not_1_inj] Theorem
⊢ INJ coprimes (𝕌(:num) DIFF {1}) 𝕌(:num -> bool)
[coprimes_map_cross_inj] Theorem
⊢ ∀m n.
coprime m n ⇒
INJ
(λ(x,y). if m * n = 1 then 1 else (x * n + y * m) MOD (m * n))
(coprimes m × coprimes n) 𝕌(:num)
[coprimes_mult_by_image] Theorem
⊢ ∀m n.
coprime m n ⇒
coprimes (m * n) =
IMAGE
(λ(x,y). if m * n = 1 then 1 else (x * n + y * m) MOD (m * n))
(coprimes m × coprimes n)
[coprimes_prime] Theorem
⊢ ∀n. prime n ⇒ coprimes n = residue n
[coprimes_prime_power] Theorem
⊢ ∀p n.
prime p ⇒
coprimes (p ** n) = natural (p ** n) DIFF p multiples_upto p ** n
[coprimes_thm] Theorem
⊢ ∀n. coprimes n = set (FILTER (λj. coprime j n) (GENLIST SUC n))
[count_up_def] Theorem
⊢ ∀n m k.
count_up n m k =
if m = 0 then 0
else if n ≤ m then k
else count_up n (TWICE m) (SUC k)
[count_up_exit] Theorem
⊢ ∀m n. m ≠ 0 ∧ n ≤ m ⇒ ∀k. count_up n m k = k
[count_up_exit_eqn] Theorem
⊢ ∀m. m ≠ 0 ⇒
∀n t.
2 ** t * m < TWICE n ∧ n ≤ 2 ** t * m ⇒
∀k. count_up n m k = k + t
[count_up_ind] Theorem
⊢ ∀P. (∀n m k. (m ≠ 0 ∧ ¬(n ≤ m) ⇒ P n (TWICE m) (SUC k)) ⇒ P n m k) ⇒
∀v v1 v2. P v v1 v2
[count_up_suc] Theorem
⊢ ∀m n.
m ≠ 0 ∧ m < n ⇒ ∀k. count_up n m k = count_up n (TWICE m) (SUC k)
[count_up_suc_eqn] Theorem
⊢ ∀m. m ≠ 0 ⇒
∀n t.
2 ** t * m < n ⇒
∀k. count_up n m k = count_up n (2 ** SUC t * m) (SUC k + t)
[divisor_gt_cofactor_le] Theorem
⊢ ∀n p. 0 < p ∧ p divides n ∧ SQRT n < p ⇒ n DIV p ≤ SQRT n
[divisor_le_cofactor_ge] Theorem
⊢ ∀n p. 0 < p ∧ p divides n ∧ p ≤ SQRT n ⇒ SQRT n ≤ n DIV p
[divisor_prime_factorisation] Theorem
⊢ ∀m n.
0 < n ∧ m divides n ⇒
m = PROD_SET (IMAGE (λp. p ** ppidx m) (prime_divisors n))
[divisors_0] Theorem
⊢ divisors 0 = ∅
[divisors_1] Theorem
⊢ divisors 1 = {1}
[divisors_card_upper] Theorem
⊢ ∀n. CARD (divisors n) ≤ TWICE (SQRT n)
[divisors_cofactor_inj] Theorem
⊢ ∀n. INJ (λj. n DIV j) (divisors n) 𝕌(:num)
[divisors_delete_last] Theorem
⊢ ∀n. divisors n DELETE n = {m | 0 < m ∧ m < n ∧ m divides n}
[divisors_divisors_bij] Theorem
⊢ ∀n. (λd. n DIV d) PERMUTES divisors n
[divisors_element] Theorem
⊢ ∀n d. d ∈ divisors n ⇔ 0 < d ∧ d ≤ n ∧ d divides n
[divisors_element_alt] Theorem
⊢ ∀n. 0 < n ⇒ ∀d. d ∈ divisors n ⇔ d divides n
[divisors_eq_empty] Theorem
⊢ ∀n. divisors n = ∅ ⇔ n = 0
[divisors_eq_gcd_image] Theorem
⊢ ∀n. divisors n = IMAGE (gcd n) (natural n)
[divisors_eq_image_gcd_count] Theorem
⊢ ∀n. divisors n = IMAGE (gcd n) (count n)
[divisors_eq_image_gcd_natural] Theorem
⊢ ∀n. divisors n = IMAGE (gcd n) (natural n)
[divisors_eq_image_gcd_upto] Theorem
⊢ ∀n. 0 < n ⇒ divisors n = IMAGE (gcd n) (upto n)
[divisors_eqn] Theorem
⊢ ∀n. divisors n =
IMAGE (λj. if j + 1 divides n then j + 1 else 1) (count n)
[divisors_finite] Theorem
⊢ ∀n. FINITE (divisors n)
[divisors_has_1] Theorem
⊢ ∀n. 0 < n ⇒ 1 ∈ divisors n
[divisors_has_cofactor] Theorem
⊢ ∀n d. d ∈ divisors n ⇒ n DIV d ∈ divisors n
[divisors_has_element] Theorem
⊢ ∀n d. d ∈ divisors n ⇒ 0 < n
[divisors_has_factor] Theorem
⊢ ∀n p q. 0 < n ∧ n = p * q ⇒ p ∈ divisors n ∧ q ∈ divisors n
[divisors_has_last] Theorem
⊢ ∀n. 0 < n ⇒ n ∈ divisors n
[divisors_nonzero] Theorem
⊢ ∀n d. d ∈ divisors n ⇒ 0 < d
[divisors_not_empty] Theorem
⊢ ∀n. 0 < n ⇒ divisors n ≠ ∅
[divisors_subset_natural] Theorem
⊢ ∀n. divisors n ⊆ natural n
[even_sq_free_element] Theorem
⊢ ∀s n.
n ∈ even_sq_free s ⇔
n ∈ s ∧ square_free n ∧ EVEN (CARD (prime_factors n))
[even_sq_free_finite] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (even_sq_free s)
[even_sq_free_subset] Theorem
⊢ ∀s. even_sq_free s ⊆ s
[exp_to_ulog] Theorem
⊢ ∀m n. n ≤ 2 ** m ⇒ ulog n ≤ m
[factor_seek_bound] Theorem
⊢ ∀n c q. 0 < n ⇒ factor_seek n c q ≤ n
[factor_seek_def] Theorem
⊢ ∀q n c.
factor_seek n c q =
if c ≤ q then n
else if 1 < q ∧ n MOD q = 0 then q
else factor_seek n c (q + 1)
[factor_seek_ind] Theorem
⊢ ∀P. (∀n c q.
(¬(c ≤ q) ∧ ¬(1 < q ∧ n MOD q = 0) ⇒ P n c (q + 1)) ⇒
P n c q) ⇒
∀v v1 v2. P v v1 v2
[factor_seek_thm] Theorem
⊢ ∀n c q.
1 < q ∧ q ≤ c ∧ c ≤ n ⇒
(factor_seek n c q = n ⇔ ∀p. q ≤ p ∧ p < c ⇒ ¬(p divides n))
[gcd_eq_count_partition_by_divisors] Theorem
⊢ ∀n. partition (feq (gcd n)) (count n) =
IMAGE (preimage (gcd n) (count n)) (divisors n)
[gcd_eq_equiv_class] Theorem
⊢ ∀n d. preimage (gcd n) (natural n) d = gcd_matches n d
[gcd_eq_equiv_class_fun] Theorem
⊢ ∀n. preimage (gcd n) (natural n) = gcd_matches n
[gcd_eq_equiv_on_count] Theorem
⊢ ∀n. feq (gcd n) equiv_on count n
[gcd_eq_equiv_on_natural] Theorem
⊢ ∀n. feq (gcd n) equiv_on natural n
[gcd_eq_equiv_on_upto] Theorem
⊢ ∀n. feq (gcd n) equiv_on upto n
[gcd_eq_natural_partition_by_divisors] Theorem
⊢ ∀n. partition (feq (gcd n)) (natural n) =
IMAGE (preimage (gcd n) (natural n)) (divisors n)
[gcd_eq_partition_by_divisors] Theorem
⊢ ∀n. partition (feq (gcd n)) (natural n) =
IMAGE (gcd_matches n) (divisors n)
[gcd_eq_upto_partition_by_divisors] Theorem
⊢ ∀n. 0 < n ⇒
partition (feq (gcd n)) (upto n) =
IMAGE (preimage (gcd n) (upto n)) (divisors n)
[gcd_matches_0] Theorem
⊢ ∀d. gcd_matches 0 d = ∅
[gcd_matches_1] Theorem
⊢ ∀d. gcd_matches 1 d = if d = 1 then {1} else ∅
[gcd_matches_alt] Theorem
⊢ ∀n d. gcd_matches n d = natural n ∩ {j | gcd j n = d}
[gcd_matches_and_coprimes_by_same_size] Theorem
⊢ ∀n. CARD ∘ gcd_matches n = CARD ∘ coprimes_by n
[gcd_matches_bij_coprimes] Theorem
⊢ ∀n d.
0 < n ∧ d divides n ⇒
BIJ (λj. j DIV d) (gcd_matches n d) (coprimes (n DIV d))
[gcd_matches_bij_coprimes_by] Theorem
⊢ ∀n d.
d divides n ⇒
BIJ (λj. j DIV d) (gcd_matches n d) (coprimes_by n d)
[gcd_matches_divisor_element] Theorem
⊢ ∀n d.
d divides n ⇒ ∀j. j ∈ gcd_matches n d ⇒ j DIV d ∈ coprimes_by n d
[gcd_matches_element] Theorem
⊢ ∀n d j. j ∈ gcd_matches n d ⇔ 0 < j ∧ j ≤ n ∧ gcd j n = d
[gcd_matches_element_divides] Theorem
⊢ ∀n d j. j ∈ gcd_matches n d ⇒ d divides j ∧ d divides n
[gcd_matches_eq_empty] Theorem
⊢ ∀n d. 0 < n ⇒ (gcd_matches n d = ∅ ⇔ ¬(d divides n))
[gcd_matches_finite] Theorem
⊢ ∀n d. FINITE (gcd_matches n d)
[gcd_matches_from_divisors_inj] Theorem
⊢ ∀n. INJ (gcd_matches n) (divisors n) 𝕌(:num -> bool)
[gcd_matches_has_divisor] Theorem
⊢ ∀n d. 0 < n ∧ d divides n ⇒ d ∈ gcd_matches n d
[gcd_matches_subset] Theorem
⊢ ∀n d. gcd_matches n d ⊆ natural n
[gcd_matches_with_0] Theorem
⊢ ∀n. gcd_matches n 0 = ∅
[gcd_park_decompose] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
(let
a = park m n;
b = gcd m n DIV a
in
gcd m n = a * b ∧ coprime a b)
[gcd_park_decomposition] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
(let
a = park m n;
b = gcd m n DIV a
in
b = PROD_SET (IMAGE (λp. p ** ppidx n) (park_off m n)) ∧
gcd m n = a * b ∧ coprime a b)
[gcd_prime_factorisation] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
gcd m n =
PROD_SET
(IMAGE (λp. p ** MIN (ppidx m) (ppidx n))
(common_prime_divisors m n))
[gcd_prime_power_cofactor_coprime] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
coprime p (gcd (a DIV p ** ppidx a) (b DIV p ** ppidx b))
[gcd_prime_power_divisibility] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
∀k. p ** k divides gcd a b ⇒ k ≤ MIN (ppidx a) (ppidx b)
[gcd_prime_power_factor] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
gcd a b =
p ** MIN (ppidx a) (ppidx b) *
gcd (a DIV p ** ppidx a) (b DIV p ** ppidx b)
[gcd_prime_power_factor_divides_gcd] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
p ** MIN (ppidx a) (ppidx b) divides gcd a b
[gcd_prime_power_index] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
ppidx (gcd a b) = MIN (ppidx a) (ppidx b)
[halves_0] Theorem
⊢ halves 0 = 0
[halves_1] Theorem
⊢ halves 1 = SUC (halves 0)
[halves_2] Theorem
⊢ halves 2 = SUC (SUC (halves 0))
[halves_alt] Theorem
⊢ ∀n. halves n = if n = 0 then 0 else 1 + halves (HALF n)
[halves_by_LOG2] Theorem
⊢ ∀n. 0 < n ⇒ halves n = 1 + LOG2 n
[halves_def] Theorem
⊢ ∀n. halves n = if n = 0 then 0 else SUC (halves (HALF n))
[halves_eq_0] Theorem
⊢ ∀n. halves n = 0 ⇔ n = 0
[halves_eq_1] Theorem
⊢ ∀n. halves n = 1 ⇔ n = 1
[halves_ind] Theorem
⊢ ∀P. (∀n. (n ≠ 0 ⇒ P (HALF n)) ⇒ P n) ⇒ ∀v. P v
[halves_le] Theorem
⊢ MONO halves
[halves_pos] Theorem
⊢ ∀n. 0 < n ⇒ 0 < halves n
[lcm_fun_0] Theorem
⊢ lcm_fun 0 = 1
[lcm_fun_1] Theorem
⊢ lcm_fun 1 = 1
[lcm_fun_2] Theorem
⊢ lcm_fun 2 = 2
[lcm_fun_SUC] Theorem
⊢ ∀n. lcm_fun (SUC n) =
if n = 0 then 1
else
case some p. ∃k. 0 < k ∧ prime p ∧ SUC n = p ** k of
NONE => lcm_fun n
| SOME p => p * lcm_fun n
[lcm_fun_compute] Theorem
⊢ lcm_fun 0 = 1 ∧
(∀n. lcm_fun (NUMERAL (BIT1 n)) =
if NUMERAL (BIT1 n) − 1 = 0 then 1
else
case
some p. ∃k. 0 < k ∧ prime p ∧ NUMERAL (BIT1 n) = p ** k
of
NONE => lcm_fun (NUMERAL (BIT1 n) − 1)
| SOME p => p * lcm_fun (NUMERAL (BIT1 n) − 1)) ∧
∀n. lcm_fun (NUMERAL (BIT2 n)) =
if NUMERAL (BIT1 n) = 0 then 1
else
case
some p. ∃k. 0 < k ∧ prime p ∧ NUMERAL (BIT2 n) = p ** k
of
NONE => lcm_fun (NUMERAL (BIT1 n))
| SOME p => p * lcm_fun (NUMERAL (BIT1 n))
[lcm_fun_lower_bound] Theorem
⊢ ∀n. 2 ** n ≤ lcm_fun (n + 1)
[lcm_fun_lower_bound_alt] Theorem
⊢ ∀n. 0 < n ⇒ 2 ** (n − 1) ≤ lcm_fun n
[lcm_fun_suc_none] Theorem
⊢ ∀n. ¬(∃p k. 0 < k ∧ prime p ∧ SUC n = p ** k) ⇒
lcm_fun (SUC n) = lcm_fun n
[lcm_fun_suc_some] Theorem
⊢ ∀n p.
prime p ∧ (∃k. 0 < k ∧ SUC n = p ** k) ⇒
lcm_fun (SUC n) = p * lcm_fun n
[lcm_gcd_park_decompose] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
(let
a = park m n;
b = gcd m n DIV a;
p = m DIV a;
q = a * n DIV gcd m n
in
lcm m n = p * q ∧ coprime p q ∧ gcd m n = a * b ∧ m = a * p ∧
n = b * q)
[lcm_park_decompose] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
(let
a = park m n;
p = m DIV a;
q = a * n DIV gcd m n
in
lcm m n = p * q ∧ coprime p q)
[lcm_park_decomposition] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
(let
a = park m n;
b = gcd m n DIV a;
p = m DIV a;
q = a * n DIV gcd m n
in
b = PROD_SET (IMAGE (λp. p ** ppidx n) (park_off m n)) ∧
p =
PROD_SET
(IMAGE (λp. p ** ppidx m)
(prime_divisors m DIFF park_on m n)) ∧
q =
PROD_SET
(IMAGE (λp. p ** ppidx n)
(prime_divisors n DIFF park_off m n)) ∧ lcm m n = p * q ∧
coprime p q ∧ gcd m n = a * b ∧ m = a * p ∧ n = b * q)
[lcm_prime_factorisation] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ⇒
lcm m n =
PROD_SET
(IMAGE (λp. p ** MAX (ppidx m) (ppidx n))
(total_prime_divisors m n))
[lcm_prime_power_cofactor_coprime] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
coprime p (lcm (a DIV p ** ppidx a) (b DIV p ** ppidx b))
[lcm_prime_power_divisibility] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
∀k. p ** k divides lcm a b ⇒ k ≤ MAX (ppidx a) (ppidx b)
[lcm_prime_power_factor] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
lcm a b =
p ** MAX (ppidx a) (ppidx b) *
lcm (a DIV p ** ppidx a) (b DIV p ** ppidx b)
[lcm_prime_power_factor_divides_lcm] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
p ** MAX (ppidx a) (ppidx b) divides lcm a b
[lcm_prime_power_index] Theorem
⊢ ∀a b p.
0 < a ∧ 0 < b ∧ prime p ⇒
ppidx (lcm a b) = MAX (ppidx a) (ppidx b)
[lcm_run_eq_prod_set_prime_powers] Theorem
⊢ ∀n. lcm_run n = PROD_SET (prime_powers_upto n)
[lcm_run_eq_set_lcm_prime_powers] Theorem
⊢ ∀n. lcm_run n = set_lcm (prime_powers_upto n)
[lcm_run_lower_by_primes_count] Theorem
⊢ ∀n. SQRT (n ** primes_count n) ≤ lcm_run n
[lcm_run_lower_by_primes_product] Theorem
⊢ ∀n. PROD_SET (primes_upto n) ≤ lcm_run n
[lcm_run_upper_by_primes_count] Theorem
⊢ ∀n. lcm_run n ≤ n ** primes_count n
[lcm_special_for_coprime_factors] Theorem
⊢ ∀n a b.
n = a * b ∧ coprime a b ⇒
∀m. a divides m ∧ b divides m ⇒ lcm n m = m
[lcm_special_for_prime_power] Theorem
⊢ ∀p. prime p ⇒ ∀m n. n = p ** SUC (ppidx m) ⇒ lcm n m = p * m
[less_divisors_0] Theorem
⊢ less_divisors 0 = ∅
[less_divisors_1] Theorem
⊢ less_divisors 1 = ∅
[less_divisors_element] Theorem
⊢ ∀n x. x ∈ less_divisors n ⇔ 0 < x ∧ x < n ∧ x divides n
[less_divisors_finite] Theorem
⊢ ∀n. FINITE (less_divisors n)
[less_divisors_has_1] Theorem
⊢ ∀n. 1 < n ⇒ 1 ∈ less_divisors n
[less_divisors_has_cofactor] Theorem
⊢ ∀n d. 1 < d ∧ d ∈ less_divisors n ⇒ n DIV d ∈ less_divisors n
[less_divisors_max] Theorem
⊢ ∀n. MAX_SET (less_divisors n) ≤ HALF n
[less_divisors_min] Theorem
⊢ ∀n. 1 < n ⇒ MIN_SET (less_divisors n) = 1
[less_divisors_nonzero] Theorem
⊢ ∀n x. x ∈ less_divisors n ⇒ 0 < x
[less_divisors_prime] Theorem
⊢ ∀n. prime n ⇒ less_divisors n = {1}
[less_divisors_subset_divisors] Theorem
⊢ ∀n. less_divisors n ⊆ divisors n
[less_divisors_subset_natural] Theorem
⊢ ∀n. less_divisors n ⊆ natural (HALF n)
[list_lcm_by_last_non_prime_power] Theorem
⊢ ∀n. ¬SING (prime_divisors (n + 1)) ⇒ lcm_run (n + 1) = lcm_run n
[list_lcm_by_last_prime_power] Theorem
⊢ ∀n. SING (prime_divisors (n + 1)) ⇒
lcm_run (n + 1) = CHOICE (prime_divisors (n + 1)) * lcm_run n
[list_lcm_eq_lcm_fun] Theorem
⊢ ∀n. lcm_run (n + 1) = lcm_fun (n + 1)
[list_lcm_option_last_non_prime_power] Theorem
⊢ ∀n. (∀p. prime_divisors (n + 1) ≠ {p}) ⇒
lcm_run (n + 1) = lcm_run n
[list_lcm_option_last_prime_power] Theorem
⊢ ∀n p.
prime_divisors (n + 1) = {p} ⇒ lcm_run (n + 1) = p * lcm_run n
[list_lcm_option_recurrence] Theorem
⊢ ∀n. lcm_run (n + 1) =
case some p. prime_divisors (n + 1) = {p} of
NONE => lcm_run n
| SOME p => p * lcm_run n
[list_lcm_prime_power_divisibility] Theorem
⊢ ∀l p.
prime p ∧ POSITIVE l ⇒
∀k. p ** k divides list_lcm l ⇒ k ≤ MAX_LIST (MAP ppidx l)
[list_lcm_prime_power_factor_divides] Theorem
⊢ ∀l p. prime p ⇒ p ** MAX_LIST (MAP ppidx l) divides list_lcm l
[list_lcm_prime_power_factor_member] Theorem
⊢ ∀l p.
prime p ∧ l ≠ [] ∧ POSITIVE l ⇒
∀k. p ** k divides list_lcm l ⇒ ∃x. MEM x l ∧ p ** k divides x
[list_lcm_prime_power_index] Theorem
⊢ ∀l p.
prime p ∧ POSITIVE l ⇒
ppidx (list_lcm l) = MAX_LIST (MAP ppidx l)
[list_lcm_prime_power_index_lower] Theorem
⊢ ∀l p.
prime p ∧ l ≠ [] ∧ POSITIVE l ⇒
∀x. MEM x l ⇒ ppidx x ≤ ppidx (list_lcm l)
[list_lcm_recurrence] Theorem
⊢ ∀n. lcm_run (n + 1) =
(let
s = prime_divisors (n + 1)
in
if SING s then CHOICE s * lcm_run n else lcm_run n)
[list_lcm_with_last_non_prime_power] Theorem
⊢ ∀n. (∀p k. k = 0 ∨ ¬prime p ∨ n + 2 ≠ p ** k) ⇒
lcm_run (n + 2) = lcm_run (n + 1)
[list_lcm_with_last_prime_power] Theorem
⊢ ∀n p k.
prime p ∧ n + 2 = p ** k ⇒ lcm_run (n + 2) = p * lcm_run (n + 1)
[multiples_upto_0_n] Theorem
⊢ ∀n. 0 multiples_upto n = ∅
[multiples_upto_1_n] Theorem
⊢ ∀n. 1 multiples_upto n = natural n
[multiples_upto_alt] Theorem
⊢ ∀m n. m multiples_upto n = {x | ∃k. x = k * m ∧ 0 < x ∧ x ≤ n}
[multiples_upto_card] Theorem
⊢ ∀m n. CARD (m multiples_upto n) = if m = 0 then 0 else n DIV m
[multiples_upto_element] Theorem
⊢ ∀m n x. x ∈ m multiples_upto n ⇔ m divides x ∧ 0 < x ∧ x ≤ n
[multiples_upto_element_alt] Theorem
⊢ ∀m n x. x ∈ m multiples_upto n ⇔ ∃k. x = k * m ∧ 0 < x ∧ x ≤ n
[multiples_upto_eqn] Theorem
⊢ ∀m n. m multiples_upto n = {x | m divides x ∧ x ∈ natural n}
[multiples_upto_finite] Theorem
⊢ ∀m n. FINITE (m multiples_upto n)
[multiples_upto_m_0] Theorem
⊢ ∀m. m multiples_upto 0 = ∅
[multiples_upto_m_1] Theorem
⊢ ∀m. m multiples_upto 1 = if m = 1 then {1} else ∅
[multiples_upto_subset] Theorem
⊢ ∀m n. m multiples_upto n ⊆ natural n
[multiples_upto_thm] Theorem
⊢ ∀m n.
m multiples_upto n =
if m = 0 then ∅ else IMAGE ($* m) (natural (n DIV m))
[non_prime_power_coprime_factors] Theorem
⊢ ∀n. 1 < n ∧ ¬(∃p k. 0 < k ∧ prime p ∧ n = p ** k) ⇒
∃a b. n = a * b ∧ coprime a b ∧ 1 < a ∧ a < n ∧ 1 < b ∧ b < n
[non_sq_free_element] Theorem
⊢ ∀s n. n ∈ non_sq_free s ⇔ n ∈ s ∧ ¬square_free n
[non_sq_free_finite] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (non_sq_free s)
[non_sq_free_subset] Theorem
⊢ ∀s. non_sq_free s ⊆ s
[odd_sq_free_element] Theorem
⊢ ∀s n.
n ∈ odd_sq_free s ⇔
n ∈ s ∧ square_free n ∧ ODD (CARD (prime_factors n))
[odd_sq_free_finite] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (odd_sq_free s)
[odd_sq_free_subset] Theorem
⊢ ∀s. odd_sq_free s ⊆ s
[odd_square_lt] Theorem
⊢ ∀n m. ¬square n ⇒ ((TWICE m + 1)² < n ⇔ m < HALF (1 + SQRT n))
[pairwise_coprime_for_prime_powers] Theorem
⊢ ∀s f. s ⊆ prime ⇒ PAIRWISE_COPRIME (IMAGE (λp. p ** f p) s)
[park_off_alt] Theorem
⊢ ∀m n. park_off m n = common_prime_divisors m n DIFF park_on m n
[park_off_element] Theorem
⊢ ∀m n p.
p ∈ park_off m n ⇔
p ∈ prime_divisors m ∧ p ∈ prime_divisors n ∧ ppidx n < ppidx m
[park_off_image_has_not_1] Theorem
⊢ ∀m n. 1 ∉ IMAGE (λp. p ** ppidx m) (park_off m n)
[park_off_subset_common] Theorem
⊢ ∀m n. park_off m n ⊆ common_prime_divisors m n
[park_off_subset_total] Theorem
⊢ ∀m n. park_off m n ⊆ total_prime_divisors m n
[park_on_element] Theorem
⊢ ∀m n p.
p ∈ park_on m n ⇔
p ∈ prime_divisors m ∧ p ∈ prime_divisors n ∧ ppidx m ≤ ppidx n
[park_on_off_common_image_partition] Theorem
⊢ ∀m n.
(let
s =
IMAGE (λp. p ** MIN (ppidx m) (ppidx n))
(common_prime_divisors m n);
u = IMAGE (λp. p ** ppidx m) (park_on m n);
v = IMAGE (λp. p ** ppidx n) (park_off m n)
in
0 < m ⇒ s =|= u # v)
[park_on_off_partition] Theorem
⊢ ∀m n. common_prime_divisors m n =|= park_on m n # park_off m n
[park_on_off_total_image_partition] Theorem
⊢ ∀m n.
(let
s =
IMAGE (λp. p ** MAX (ppidx m) (ppidx n))
(total_prime_divisors m n);
u =
IMAGE (λp. p ** ppidx m) (prime_divisors m DIFF park_on m n);
v =
IMAGE (λp. p ** ppidx n)
(prime_divisors n DIFF park_off m n)
in
0 < m ∧ 0 < n ⇒ s =|= u # v)
[park_on_subset_common] Theorem
⊢ ∀m n. park_on m n ⊆ common_prime_divisors m n
[park_on_subset_total] Theorem
⊢ ∀m n. park_on m n ⊆ total_prime_divisors m n
[perfect_power_0_m] Theorem
⊢ ∀m. 0 power_of m ⇔ m = 0
[perfect_power_1_m] Theorem
⊢ ∀m. 1 power_of m
[perfect_power_2_odd] Theorem
⊢ ∀n. n power_of 2 ⇒ (ODD n ⇔ n = 1)
[perfect_power_bound_LOG2] Theorem
⊢ ∀n. 0 < n ⇒ ∀m. n power_of m ⇔ ∃k. k ≤ LOG2 n ∧ n = m ** k
[perfect_power_bound_ulog] Theorem
⊢ ∀n. 0 < n ⇒ ∀m. n power_of m ⇔ ∃k. k ≤ ulog n ∧ n = m ** k
[perfect_power_cofactor] Theorem
⊢ ∀n p. 0 < p ∧ p divides n ⇒ (n power_of p ⇔ n DIV p power_of p)
[perfect_power_cofactor_alt] Theorem
⊢ ∀n p. 0 < n ∧ p divides n ⇒ (n power_of p ⇔ n DIV p power_of p)
[perfect_power_condition] Theorem
⊢ ∀p q. prime p ∧ (∃x y. 0 < x ∧ p ** x = q ** y) ⇒ q power_of p
[perfect_power_half_inequality_1] Theorem
⊢ ∀p n. 1 < p ∧ 0 < n ⇒ TWICE (p ** HALF n) ≤ p ** n
[perfect_power_half_inequality_2] Theorem
⊢ ∀p n.
1 < p ∧ 0 < n ⇒
(p ** HALF n − 2) * p ** HALF n ≤ p ** n − TWICE (p ** HALF n)
[perfect_power_mod_eq_0] Theorem
⊢ ∀n m.
0 < m ∧ 1 < n ∧ n MOD m = 0 ⇒ (n power_of m ⇔ n DIV m power_of m)
[perfect_power_mod_ne_0] Theorem
⊢ ∀n m. 0 < m ∧ 1 < n ∧ n MOD m ≠ 0 ⇒ ¬(n power_of m)
[perfect_power_n_0] Theorem
⊢ ∀n. n power_of 0 ⇔ n = 0 ∨ n = 1
[perfect_power_n_1] Theorem
⊢ ∀n. n power_of 1 ⇔ n = 1
[perfect_power_not_suc] Theorem
⊢ ∀m n. 1 < m ∧ 1 < n ∧ n power_of m ⇒ ¬(SUC n power_of m)
[perfect_power_self] Theorem
⊢ ∀n. n power_of n
[perfect_power_special_inequality] Theorem
⊢ ∀p. 1 < p ⇒ ∀n. p * tops p n < (p − 1) * TWICE (p ** n)
[perfect_power_suc] Theorem
⊢ ∀m n. 1 < m ∧ n power_of m ∧ SUC n power_of m ⇒ m = 2 ∧ n = 1
[perfect_power_test] Theorem
⊢ ∀n m.
n power_of m ⇔
if n = 0 then m = 0
else if n = 1 then T
else if m = 0 then n ≤ 1
else if m = 1 then n = 1
else if n MOD m = 0 then n DIV m power_of m
else F
[phi_0] Theorem
⊢ phi 0 = 0
[phi_1] Theorem
⊢ phi 1 = 1
[phi_2] Theorem
⊢ phi 2 = 1
[phi_eq_0] Theorem
⊢ ∀n. phi n = 0 ⇔ n = 0
[phi_eq_totient] Theorem
⊢ ∀n. 1 < n ⇒ phi n = totient n
[phi_fun] Theorem
⊢ phi = CARD ∘ coprimes
[phi_gt_1] Theorem
⊢ ∀n. 2 < n ⇒ 1 < phi n
[phi_le] Theorem
⊢ ∀n. phi n ≤ n
[phi_lt] Theorem
⊢ ∀n. 1 < n ⇒ phi n < n
[phi_mult] Theorem
⊢ ∀m n. coprime m n ⇒ phi (m * n) = phi m * phi n
[phi_pos] Theorem
⊢ ∀n. 0 < n ⇒ 0 < phi n
[phi_prime] Theorem
⊢ ∀n. prime n ⇒ phi n = n − 1
[phi_prime_power] Theorem
⊢ ∀p n. prime p ⇒ phi (p ** SUC n) = (p − 1) * p ** n
[phi_prime_sq] Theorem
⊢ ∀p. prime p ⇒ phi (SQ p) = p * (p − 1)
[phi_primes] Theorem
⊢ ∀p q.
prime p ∧ prime q ⇒
phi (p * q) = if p = q then p * (p − 1) else (p − 1) * (q − 1)
[phi_primes_distinct] Theorem
⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ phi (p * q) = (p − 1) * (q − 1)
[phi_thm] Theorem
⊢ ∀n. phi n = LENGTH (FILTER (λj. coprime j n) (GENLIST SUC n))
[power_free_0] Theorem
⊢ power_free 0 ⇔ F
[power_free_1] Theorem
⊢ power_free 1 ⇔ F
[power_free_2] Theorem
⊢ power_free 2
[power_free_3] Theorem
⊢ power_free 3
[power_free_alt] Theorem
⊢ power_free n ⇔ 1 < n ∧ ∀m. n power_of m ⇒ n = m
[power_free_by_power_index_LOG2] Theorem
⊢ ∀n. power_free n ⇔ 1 < n ∧ power_index n (LOG2 n) = 1
[power_free_by_power_index_ulog] Theorem
⊢ ∀n. power_free n ⇔ 1 < n ∧ power_index n (ulog n) = 1
[power_free_check_all] Theorem
⊢ ∀n. power_free n ⇔ 1 < n ∧ ∀j. 1 < j ⇒ ROOT j n ** j ≠ n
[power_free_check_upto] Theorem
⊢ ∀n b. LOG2 n ≤ b ⇒ (power_free n ⇔ 1 < n ∧ n power_free_upto b)
[power_free_check_upto_LOG2] Theorem
⊢ ∀n. power_free n ⇔ 1 < n ∧ n power_free_upto LOG2 n
[power_free_check_upto_ulog] Theorem
⊢ ∀n. power_free n ⇔ 1 < n ∧ n power_free_upto ulog n
[power_free_gt_1] Theorem
⊢ ∀n. power_free n ⇒ 1 < n
[power_free_perfect_power] Theorem
⊢ ∀m n. power_free n ∧ n power_of m ⇒ n = m
[power_free_property] Theorem
⊢ ∀n. power_free n ⇒ ∀j. 1 < j ⇒ ROOT j n ** j ≠ n
[power_free_test_eqn] Theorem
⊢ ∀n. power_free_test n ⇔ power_free n
[power_free_test_upto_LOG2] Theorem
⊢ ∀n. power_free n ⇔
1 < n ∧ ∀j. 1 < j ∧ j ≤ LOG2 n ⇒ ROOT j n ** j ≠ n
[power_free_test_upto_ulog] Theorem
⊢ ∀n. power_free n ⇔
1 < n ∧ ∀j. 1 < j ∧ j ≤ ulog n ⇒ ROOT j n ** j ≠ n
[power_free_upto_0] Theorem
⊢ ∀n. n power_free_upto 0 ⇔ T
[power_free_upto_1] Theorem
⊢ ∀n. n power_free_upto 1 ⇔ T
[power_free_upto_suc] Theorem
⊢ ∀n k.
0 < k ∧ n power_free_upto k ⇒
(n power_free_upto k + 1 ⇔ ROOT (k + 1) n ** (k + 1) ≠ n)
[power_index_0] Theorem
⊢ ∀n. power_index n 0 = 1
[power_index_1] Theorem
⊢ ∀n. power_index n 1 = 1
[power_index_def] Theorem
⊢ ∀n k.
power_index n k =
if k ≤ 1 then 1
else if ROOT k n ** k = n then k
else power_index n (k − 1)
[power_index_eqn] Theorem
⊢ ∀n k. ROOT (power_index n k) n ** power_index n k = n
[power_index_equal] Theorem
⊢ ∀m n k.
0 < k ∧ k ≤ m ⇒
(power_index n m = power_index n k ⇔
∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n)
[power_index_exact_root] Theorem
⊢ ∀n k. 0 < k ∧ ROOT k n ** k = n ⇒ power_index n k = k
[power_index_ind] Theorem
⊢ ∀P. (∀n k. (¬(k ≤ 1) ∧ ROOT k n ** k ≠ n ⇒ P n (k − 1)) ⇒ P n k) ⇒
∀v v1. P v v1
[power_index_lower] Theorem
⊢ ∀m n k. k ≤ m ∧ ROOT k n ** k = n ⇒ k ≤ power_index n m
[power_index_no_exact_roots] Theorem
⊢ ∀m n k.
k ≤ m ∧ (∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n) ⇒
power_index n m = power_index n k
[power_index_not_exact_root] Theorem
⊢ ∀n k. ROOT k n ** k ≠ n ⇒ power_index n k = power_index n (k − 1)
[power_index_of_1] Theorem
⊢ ∀k. power_index 1 k = if k = 0 then 1 else k
[power_index_pos] Theorem
⊢ ∀n k. 0 < power_index n k
[power_index_property] Theorem
⊢ ∀m n k. power_index n m = k ⇒ ∀j. k < j ∧ j ≤ m ⇒ ROOT j n ** j ≠ n
[power_index_root] Theorem
⊢ ∀n k. n power_of ROOT (power_index n k) n
[power_index_upper] Theorem
⊢ ∀n k. 0 < k ⇒ power_index n k ≤ k
[prime_by_sqrt_factors] Theorem
⊢ ∀p. prime p ⇔ 1 < p ∧ ∀q. 1 < q ∧ q ≤ SQRT p ⇒ ¬(q divides p)
[prime_divisors_0] Theorem
⊢ prime_divisors 0 = {p | prime p}
[prime_divisors_0_not_sing] Theorem
⊢ ¬SING (prime_divisors 0)
[prime_divisors_1] Theorem
⊢ prime_divisors 1 = ∅
[prime_divisors_common_divisor] Theorem
⊢ ∀n m x.
x divides m ∧ x divides n ⇒
prime_divisors x ⊆ common_prime_divisors m n
[prime_divisors_common_multiple] Theorem
⊢ ∀n m x.
m divides x ∧ n divides x ⇒
total_prime_divisors m n ⊆ prime_divisors x
[prime_divisors_divisor_subset] Theorem
⊢ ∀m n. m divides n ⇒ prime_divisors m ⊆ prime_divisors n
[prime_divisors_element] Theorem
⊢ ∀n p. p ∈ prime_divisors n ⇔ prime p ∧ p divides n
[prime_divisors_empty_iff] Theorem
⊢ ∀n. prime_divisors n = ∅ ⇔ n = 1
[prime_divisors_finite] Theorem
⊢ ∀n. 0 < n ⇒ FINITE (prime_divisors n)
[prime_divisors_nonempty] Theorem
⊢ ∀n. 1 < n ⇒ prime_divisors n ≠ ∅
[prime_divisors_prime] Theorem
⊢ ∀n. prime n ⇒ prime_divisors n = {n}
[prime_divisors_prime_power] Theorem
⊢ ∀n. prime n ⇒ ∀k. 0 < k ⇒ prime_divisors (n ** k) = {n}
[prime_divisors_sing] Theorem
⊢ ∀n. SING (prime_divisors n) ⇔ ∃p k. prime p ∧ 0 < k ∧ n = p ** k
[prime_divisors_sing_alt] Theorem
⊢ ∀n p. prime_divisors n = {p} ⇔ ∃k. prime p ∧ 0 < k ∧ n = p ** k
[prime_divisors_sing_property] Theorem
⊢ ∀n. SING (prime_divisors n) ⇒
(let
p = CHOICE (prime_divisors n)
in
prime p ∧ n = p ** ppidx n)
[prime_divisors_subset_natural] Theorem
⊢ ∀n. 0 < n ⇒ prime_divisors n ⊆ natural n
[prime_divisors_subset_prime] Theorem
⊢ ∀n. prime_divisors n ⊆ prime
[prime_factor_estimate] Theorem
⊢ ∀n. 1 < n ⇒ (¬prime n ⇔ ∃p. prime p ∧ p divides n ∧ p ≤ SQRT n)
[prime_factorisation] Theorem
⊢ ∀n. 0 < n ⇒ n = PROD_SET (prime_power_divisors n)
[prime_factors_element] Theorem
⊢ ∀n p. p ∈ prime_factors n ⇔ prime p ∧ p ≤ n ∧ p divides n
[prime_factors_finite] Theorem
⊢ ∀n. FINITE (prime_factors n)
[prime_factors_subset] Theorem
⊢ ∀n. prime_factors n ⊆ divisors n
[prime_is_power_free] Theorem
⊢ ∀n. prime n ⇒ power_free n
[prime_non_square] Theorem
⊢ ∀p. prime p ⇒ ¬square p
[prime_power_cofactor_coprime] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ coprime p (n DIV p ** ppidx n)
[prime_power_divisibility] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ ∀k. p ** k divides n ⇔ k ≤ ppidx n
[prime_power_divisors_1] Theorem
⊢ prime_power_divisors 1 = ∅
[prime_power_divisors_element] Theorem
⊢ ∀n x.
x ∈ prime_power_divisors n ⇔
∃p. x = p ** ppidx n ∧ prime p ∧ p divides n
[prime_power_divisors_element_alt] Theorem
⊢ ∀p n. prime p ∧ p divides n ⇒ p ** ppidx n ∈ prime_power_divisors n
[prime_power_divisors_finite] Theorem
⊢ ∀n. 0 < n ⇒ FINITE (prime_power_divisors n)
[prime_power_divisors_pairwise_coprime] Theorem
⊢ ∀n x y.
x ∈ prime_power_divisors n ∧ y ∈ prime_power_divisors n ∧ x ≠ y ⇒
coprime x y
[prime_power_eqn] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ n = p ** ppidx n * (n DIV p ** ppidx n)
[prime_power_factor_divides] Theorem
⊢ ∀n p. prime p ⇒ p ** ppidx n divides n
[prime_power_index_1] Theorem
⊢ ∀p. prime p ⇒ ppidx 1 = 0
[prime_power_index_common_divisor] Theorem
⊢ ∀n m x.
0 < m ∧ 0 < n ∧ x divides m ∧ x divides n ⇒
∀p. prime p ⇒ ppidx x ≤ MIN (ppidx m) (ppidx n)
[prime_power_index_common_multiple] Theorem
⊢ ∀n m x.
0 < x ∧ m divides x ∧ n divides x ⇒
∀p. prime p ⇒ MAX (ppidx m) (ppidx n) ≤ ppidx x
[prime_power_index_eq_0] Theorem
⊢ ∀n p. 0 < n ∧ prime p ∧ ¬(p divides n) ⇒ ppidx n = 0
[prime_power_index_eqn] Theorem
⊢ ∀n p.
0 < n ∧ prime p ⇒
(let
q = n DIV p ** ppidx n
in
n = p ** ppidx n * q ∧ coprime p q)
[prime_power_index_exists] Theorem
⊢ ∀n p.
0 < n ∧ prime p ⇒ ∃m. p ** m divides n ∧ coprime p (n DIV p ** m)
[prime_power_index_le_log_index] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ ppidx n ≤ LOG p n
[prime_power_index_maximal] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ ∀k. k > ppidx n ⇒ ¬(p ** k divides n)
[prime_power_index_of_divisor] Theorem
⊢ ∀m n. 0 < n ∧ m divides n ⇒ ∀p. prime p ⇒ ppidx m ≤ ppidx n
[prime_power_index_pos] Theorem
⊢ ∀n p. 0 < n ∧ prime p ∧ p divides n ⇒ 0 < ppidx n
[prime_power_index_prime] Theorem
⊢ ∀p. prime p ⇒ ppidx p = 1
[prime_power_index_prime_power] Theorem
⊢ ∀p. prime p ⇒ ∀k. ppidx (p ** k) = k
[prime_power_index_suc_property] Theorem
⊢ ∀n p.
0 < n ∧ prime p ∧ n + 1 = p ** ppidx (n + 1) ⇒
ppidx (n + 1) = 1 + ppidx (lcm_run n)
[prime_power_index_suc_special] Theorem
⊢ ∀n p.
0 < n ∧ prime p ∧ SUC n = p ** ppidx (SUC n) ⇒
ppidx (SUC n) = SUC (ppidx (lcm_run n))
[prime_power_index_test] Theorem
⊢ ∀n p.
0 < n ∧ prime p ⇒
∀k. k = ppidx n ⇔ ∃q. n = p ** k * q ∧ coprime p q
[prime_power_or_coprime_factors] Theorem
⊢ ∀n. 1 < n ⇒
(∃p k. 0 < k ∧ prime p ∧ n = p ** k) ∨
∃a b. n = a * b ∧ coprime a b ∧ 1 < a ∧ 1 < b ∧ a < n ∧ b < n
[prime_powers_upto_0] Theorem
⊢ prime_powers_upto 0 = ∅
[prime_powers_upto_1] Theorem
⊢ prime_powers_upto 1 = ∅
[prime_powers_upto_element] Theorem
⊢ ∀n x.
x ∈ prime_powers_upto n ⇔ ∃p. x = p ** LOG p n ∧ prime p ∧ p ≤ n
[prime_powers_upto_element_alt] Theorem
⊢ ∀p n. prime p ∧ p ≤ n ⇒ p ** LOG p n ∈ prime_powers_upto n
[prime_powers_upto_finite] Theorem
⊢ ∀n. FINITE (prime_powers_upto n)
[prime_powers_upto_lcm_divisor] Theorem
⊢ ∀n x. 0 < x ∧ x ≤ n ⇒ x divides set_lcm (prime_powers_upto n)
[prime_powers_upto_lcm_prime_divisor] Theorem
⊢ ∀n p. prime p ∧ p ≤ n ⇒ p divides set_lcm (prime_powers_upto n)
[prime_powers_upto_lcm_prime_to_log_divisor] Theorem
⊢ ∀n p.
prime p ∧ p ≤ n ⇒
p ** LOG p n divides set_lcm (prime_powers_upto n)
[prime_powers_upto_lcm_prime_to_power_divisor] Theorem
⊢ ∀n p.
prime p ∧ p ≤ n ⇒
p ** ppidx n divides set_lcm (prime_powers_upto n)
[prime_powers_upto_list_mem] Theorem
⊢ ∀n x.
MEM x (SET_TO_LIST (prime_powers_upto n)) ⇔
∃p. x = p ** LOG p n ∧ prime p ∧ p ≤ n
[prime_powers_upto_pairwise_coprime] Theorem
⊢ ∀n x y.
x ∈ prime_powers_upto n ∧ y ∈ prime_powers_upto n ∧ x ≠ y ⇒
coprime x y
[prime_powers_upto_prod_set_ge] Theorem
⊢ ∀n. PROD_SET (primes_upto n) ≤ PROD_SET (prime_powers_upto n)
[prime_powers_upto_prod_set_le] Theorem
⊢ ∀n. PROD_SET (prime_powers_upto n) ≤ n ** primes_count n
[prime_powers_upto_prod_set_mix_ge] Theorem
⊢ ∀n. n ** primes_count n ≤
PROD_SET (primes_upto n) * PROD_SET (prime_powers_upto n)
[prime_test_thm] Theorem
⊢ ∀n. prime n ⇔ prime_test n
[primes_count_0] Theorem
⊢ primes_count 0 = 0
[primes_count_1] Theorem
⊢ primes_count 1 = 0
[primes_count_upper_by_lcm_run] Theorem
⊢ ∀n. n ** primes_count n ≤ (lcm_run n)²
[primes_count_upper_by_product] Theorem
⊢ ∀n. n ** primes_count n ≤ PROD_SET (primes_upto n) * lcm_run n
[primes_upto_0] Theorem
⊢ primes_upto 0 = ∅
[primes_upto_1] Theorem
⊢ primes_upto 1 = ∅
[primes_upto_element] Theorem
⊢ ∀n p. p ∈ primes_upto n ⇔ prime p ∧ p ≤ n
[primes_upto_finite] Theorem
⊢ ∀n. FINITE (primes_upto n)
[primes_upto_pairwise_coprime] Theorem
⊢ ∀n x y. x ∈ primes_upto n ∧ y ∈ primes_upto n ∧ x ≠ y ⇒ coprime x y
[primes_upto_subset_natural] Theorem
⊢ ∀n. primes_upto n ⊆ natural n
[proper_divisors_0] Theorem
⊢ proper_divisors 0 = ∅
[proper_divisors_1] Theorem
⊢ proper_divisors 1 = ∅
[proper_divisors_by_less_divisors] Theorem
⊢ ∀n. proper_divisors n = less_divisors n DELETE 1
[proper_divisors_element] Theorem
⊢ ∀n x. x ∈ proper_divisors n ⇔ 1 < x ∧ x < n ∧ x divides n
[proper_divisors_finite] Theorem
⊢ ∀n. FINITE (proper_divisors n)
[proper_divisors_has_cofactor] Theorem
⊢ ∀n d. d ∈ proper_divisors n ⇒ n DIV d ∈ proper_divisors n
[proper_divisors_max_min] Theorem
⊢ ∀n. proper_divisors n ≠ ∅ ⇒
MAX_SET (proper_divisors n) = n DIV MIN_SET (proper_divisors n) ∧
MIN_SET (proper_divisors n) = n DIV MAX_SET (proper_divisors n)
[proper_divisors_min_gt_1] Theorem
⊢ ∀n. proper_divisors n ≠ ∅ ⇒ 1 < MIN_SET (proper_divisors n)
[proper_divisors_not_1] Theorem
⊢ ∀n. 1 ∉ proper_divisors n
[proper_divisors_prime] Theorem
⊢ ∀n. prime n ⇒ proper_divisors n = ∅
[proper_divisors_subset] Theorem
⊢ ∀n. proper_divisors n ⊆ less_divisors n
[rec_phi_0] Theorem
⊢ rec_phi 0 = 0
[rec_phi_1] Theorem
⊢ rec_phi 1 = 1
[rec_phi_def] Theorem
⊢ ∀n. rec_phi n =
if n = 0 then 0
else if n = 1 then 1
else n − ∑ (λa. rec_phi a) {m | m < n ∧ m divides n}
[rec_phi_eq_phi] Theorem
⊢ ∀n. rec_phi n = phi n
[rec_phi_ind] Theorem
⊢ ∀P. (∀n. (∀a. n ≠ 0 ∧ n ≠ 1 ∧ a ∈ {m | m < n ∧ m divides n} ⇒ P a) ⇒
P n) ⇒
∀v. P v
[self_to_log_index_member] Theorem
⊢ ∀n x. MEM x [1 .. n] ⇒ MEM (x ** LOG x n) [1 .. n]
[set_lcm_prime_powers_upto_eqn] Theorem
⊢ ∀n. set_lcm (prime_powers_upto n) = PROD_SET (prime_powers_upto n)
[sigma_eq_perfect_power_bounds_1] Theorem
⊢ ∀p. 1 < p ⇒
∀f. (∀n. 0 < n ⇒ p ** n = ∑ (λd. d * f d) (divisors n)) ⇒
(∀n. 0 < n ⇒ n * f n ≤ p ** n) ∧
∀n. 0 < n ⇒ p ** n − TWICE (p ** HALF n) < n * f n
[sigma_eq_perfect_power_bounds_2] Theorem
⊢ ∀p. 1 < p ⇒
∀f. (∀n. 0 < n ⇒ p ** n = ∑ (λd. d * f d) (divisors n)) ⇒
(∀n. 0 < n ⇒ n * f n ≤ p ** n) ∧
∀n. 0 < n ⇒ (p ** HALF n − 2) * p ** HALF n < n * f n
[sq_free_disjoint] Theorem
⊢ ∀s. DISJOINT (sq_free s) (non_sq_free s)
[sq_free_disjoint_even_odd] Theorem
⊢ ∀s. DISJOINT (even_sq_free s) (odd_sq_free s)
[sq_free_element] Theorem
⊢ ∀s n. n ∈ sq_free s ⇔ n ∈ s ∧ square_free n
[sq_free_finite] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (sq_free s)
[sq_free_inter] Theorem
⊢ ∀s. sq_free s ∩ non_sq_free s = ∅
[sq_free_inter_even_odd] Theorem
⊢ ∀s. even_sq_free s ∩ odd_sq_free s = ∅
[sq_free_split] Theorem
⊢ ∀s. s = sq_free s ∪ non_sq_free s ∧ sq_free s ∩ non_sq_free s = ∅
[sq_free_split_even_odd] Theorem
⊢ ∀s. sq_free s = even_sq_free s ∪ odd_sq_free s ∧
even_sq_free s ∩ odd_sq_free s = ∅
[sq_free_subset] Theorem
⊢ ∀s. sq_free s ⊆ s
[sq_free_union] Theorem
⊢ ∀s. s = sq_free s ∪ non_sq_free s
[sq_free_union_even_odd] Theorem
⊢ ∀s. sq_free s = even_sq_free s ∪ odd_sq_free s
[sqrt_upper] Theorem
⊢ ∀n. SQRT n ≤ 2 ** ulog n
[square_0] Theorem
⊢ square 0
[square_1] Theorem
⊢ square 1
[square_alt] Theorem
⊢ ∀n. square n ⇔ ∃k. n = k²
[square_eqn] Theorem
⊢ ∀n. square n ⇔ (SQRT n)² = n
[square_free_1] Theorem
⊢ square_free 1
[square_free_prime] Theorem
⊢ ∀n. prime n ⇒ square_free n
[sum_image_divisors_cong] Theorem
⊢ ∀f g. f 0 = g 0 ∧ (∀n. ∑ f (divisors n) = ∑ g (divisors n)) ⇒ f = g
[sum_over_count_by_divisors] Theorem
⊢ ∀f n.
∑ f (count n) =
∑ (∑ f) (IMAGE (preimage (gcd n) (count n)) (divisors n))
[sum_over_count_by_gcd_partition] Theorem
⊢ ∀f n. ∑ f (count n) = ∑ (∑ f) (partition (feq (gcd n)) (count n))
[sum_over_natural_by_divisors] Theorem
⊢ ∀f n.
∑ f (natural n) = ∑ (∑ f) (IMAGE (gcd_matches n) (divisors n))
[sum_over_natural_by_gcd_partition] Theorem
⊢ ∀f n.
∑ f (natural n) = ∑ (∑ f) (partition (feq (gcd n)) (natural n))
[sum_over_natural_by_preimage_divisors] Theorem
⊢ ∀f n.
∑ f (natural n) =
∑ (∑ f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))
[sum_over_upto_by_divisors] Theorem
⊢ ∀f n.
0 < n ⇒
∑ f (upto n) =
∑ (∑ f) (IMAGE (preimage (gcd n) (upto n)) (divisors n))
[sum_over_upto_by_gcd_partition] Theorem
⊢ ∀f n. ∑ f (upto n) = ∑ (∑ f) (partition (feq (gcd n)) (upto n))
[total_prime_divisors_element] Theorem
⊢ ∀m n p.
p ∈ total_prime_divisors m n ⇔
p ∈ prime_divisors m ∨ p ∈ prime_divisors n
[total_prime_divisors_finite] Theorem
⊢ ∀m n. 0 < m ∧ 0 < n ⇒ FINITE (total_prime_divisors m n)
[total_prime_divisors_max_image_pairwise_coprime] Theorem
⊢ ∀m n x y.
x ∈
IMAGE (λp. p ** MAX (ppidx m) (ppidx n))
(total_prime_divisors m n) ∧
y ∈
IMAGE (λp. p ** MAX (ppidx m) (ppidx n))
(total_prime_divisors m n) ∧ x ≠ y ⇒
coprime x y
[total_prime_divisors_pairwise_coprime] Theorem
⊢ ∀m n x y.
x ∈ total_prime_divisors m n ∧ y ∈ total_prime_divisors m n ∧
x ≠ y ⇒
coprime x y
[two_factors_property] Theorem
⊢ ∀n a b. n = a * b ⇒ a ≤ SQRT n ∨ b ≤ SQRT n
[two_factors_property_1] Theorem
⊢ ∀n a b. n = a * b ∧ a < SQRT n ⇒ SQRT n ≤ b
[two_factors_property_2] Theorem
⊢ ∀n a b. n = a * b ∧ SQRT n < a ⇒ b ≤ SQRT n
[ulog_0] Theorem
⊢ ulog 0 = 0
[ulog_1] Theorem
⊢ ulog 1 = 0
[ulog_2] Theorem
⊢ ulog 2 = 1
[ulog_2_exp] Theorem
⊢ ∀n. ulog (2 ** n) = n
[ulog_LOG2] Theorem
⊢ ∀n. 0 < n ⇒ LOG2 n ≤ ulog n ∧ ulog n ≤ 1 + LOG2 n
[ulog_alt] Theorem
⊢ ∀n. ulog n =
if n = 0 then 0
else if n power_of 2 then LOG2 n
else SUC (LOG2 n)
[ulog_def_alt] Theorem
⊢ ulog 0 = 0 ∧
∀n. 0 < n ⇒ ∀m. ulog n = m ⇔ n ≤ 2 ** m ∧ 2 ** m < TWICE n
[ulog_eq_0] Theorem
⊢ ∀n. ulog n = 0 ⇔ n = 0 ∨ n = 1
[ulog_eq_1] Theorem
⊢ ∀n. ulog n = 1 ⇔ n = 2
[ulog_eq_self] Theorem
⊢ ∀n. ulog n = n ⇔ n = 0
[ulog_eqn] Theorem
⊢ ∀n. ulog n = if 1 < n then SUC (LOG2 (n − 1)) else 0
[ulog_even] Theorem
⊢ ∀n. 0 < n ∧ EVEN n ⇒ ulog n = 1 + ulog (HALF n)
[ulog_exp] Theorem
⊢ ∀m n. ulog (m ** n) ≤ n * ulog m
[ulog_exp_exact] Theorem
⊢ ∀n. 2 ** ulog n = n ⇔ n power_of 2
[ulog_exp_not_exact] Theorem
⊢ ∀n. ¬(n power_of 2) ⇒ 2 ** ulog n ≠ n
[ulog_ge_1] Theorem
⊢ ∀n. 1 < n ⇒ 1 ≤ ulog n
[ulog_half] Theorem
⊢ ∀n. 1 < n ⇒ ulog (HALF n) + 1 ≤ ulog n
[ulog_le] Theorem
⊢ ∀m n. n ≤ m ⇒ ulog n ≤ ulog m
[ulog_le_1] Theorem
⊢ ∀n. ulog n ≤ 1 ⇔ n ≤ 2
[ulog_le_self] Theorem
⊢ ∀n. ulog n ≤ n
[ulog_lt] Theorem
⊢ ∀m n. n < m ⇒ ulog n ≤ ulog m
[ulog_lt_self] Theorem
⊢ ∀n. 0 < n ⇒ ulog n < n
[ulog_mult] Theorem
⊢ ∀m n. ulog (m * n) ≤ ulog m + ulog n
[ulog_odd] Theorem
⊢ ∀n. 1 < n ∧ ODD n ⇒ ulog (HALF n) + 1 ≤ ulog n
[ulog_pos] Theorem
⊢ ∀n. 1 < n ⇒ 0 < ulog n
[ulog_property] Theorem
⊢ ∀n. 0 < n ⇒ 2 ** ulog n < TWICE n ∧ n ≤ 2 ** ulog n
[ulog_property_not_exact] Theorem
⊢ ∀n. 0 < n ∧ ¬(n power_of 2) ⇒ n < 2 ** ulog n
[ulog_property_odd] Theorem
⊢ ∀n. 1 < n ∧ ODD n ⇒ n < 2 ** ulog n
[ulog_sq_gt_1] Theorem
⊢ ∀n. 2 < n ⇒ 1 < (ulog n)²
[ulog_suc] Theorem
⊢ ∀n. 0 < n ⇒ ulog (SUC n) = SUC (LOG2 n)
[ulog_thm] Theorem
⊢ ∀n. 0 < n ⇒ ∀m. ulog n = m ⇔ 2 ** m < TWICE n ∧ n ≤ 2 ** m
[ulog_twice_sq] Theorem
⊢ ∀n. 1 < n ⇒ 4 ≤ (TWICE (ulog n))²
[ulog_unique] Theorem
⊢ ∀m n. 2 ** m < TWICE n ∧ n ≤ 2 ** m ⇒ ulog n = m
*)
end
HOL 4, Trindemossen-2