Structure numberTheory
signature numberTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Euler_def : thm
val GEN_MULT_INV_DEF : thm
val MOD_MULT_INV_DEF : thm
val fequiv_def : thm
val preimage_def : thm
val residue_def : thm
val totient_def : thm
(* Theorems *)
val ADD_EQ_2 : thm
val ADD_SUB_SUB : thm
val ALL_PRIME_FACTORS_MOD_EQ_1 : thm
val AND_IMP_IMP : thm
val AND_IMP_OR_NEG : thm
val BIGUNION_ELEMENTS_SING : thm
val BIJ_LINV_ELEMENT : thm
val BIJ_LINV_THM : thm
val BIJ_RINV_BIJ : thm
val BIJ_RINV_INV : thm
val BOOL_EQ : thm
val CARD_BIGUNION_PAIR_DISJOINT : thm
val CARD_EQ_1 : thm
val CARD_PPOW : thm
val CARD_PPOW_EQN : thm
val CARD_UNION_3_DISJOINT : thm
val CARD_UNION_3_EQN : thm
val COUNT_0 : thm
val COUNT_1 : thm
val COUNT_NOT_SELF : thm
val COUNT_SUBSET : thm
val COUNT_SUC_BY_SUC : thm
val COUNT_SUC_SUBSET : thm
val DIFF_COUNT_SUC : thm
val DIFF_DELETE : thm
val DIFF_DIFF_EQ_INTER : thm
val DISJOINT_DIFF : thm
val DISJOINT_DIFF_IFF : thm
val DIVIDES_CANCEL : thm
val DIVIDES_CANCEL_COMM : thm
val DIVIDES_COFACTOR : thm
val DIVIDES_FACTORS : thm
val DIVIDES_MOD_MOD : thm
val DIVIDES_MULTIPLE_IFF : thm
val DIV_COMMON_FACTOR : thm
val DIV_DIV_MULT : thm
val DIV_LT_MONOTONE_REVERSE : thm
val DIV_LT_SUC : thm
val DIV_MULT_LESS_EQ : thm
val EQ_IMP2_THM : thm
val EQ_PARITY : thm
val EVEN_0 : thm
val EVEN_2 : thm
val EVEN_HALF : thm
val EVEN_MOD_EVEN : thm
val EVEN_MOD_ODD : thm
val EVEN_ODD_PRE : thm
val EVEN_ODD_SUC : thm
val EVEN_PARTNERS : thm
val EVEN_PRIME : thm
val EVEN_SQ : thm
val EVEN_SUC_HALF : thm
val EXP_2_EQ_0 : thm
val EXP_2_EVEN : thm
val EXP_2_HALF : thm
val EXP_2_PRE_ODD : thm
val EXP_ALT_EQN : thm
val EXP_BY_ADD_SUB_LE : thm
val EXP_BY_ADD_SUB_LT : thm
val EXP_EQN : thm
val EXP_EQN_ALT : thm
val EXP_EVEN : thm
val EXP_EXP_BASE_LE : thm
val EXP_EXP_LE_MONO_IMP : thm
val EXP_EXP_SUC : thm
val EXP_LOWER_LE_HIGH : thm
val EXP_LOWER_LE_LOW : thm
val EXP_LOWER_LT_LOW : thm
val EXP_MOD_ALT : thm
val EXP_MOD_EQN : thm
val EXP_ODD : thm
val EXP_SUC_DIV : thm
val EXP_THM : thm
val Euler_0 : thm
val Euler_1 : thm
val Euler_card_bounds : thm
val Euler_card_prime : thm
val Euler_card_upper_le : thm
val Euler_card_upper_lt : thm
val Euler_element : thm
val Euler_empty : thm
val Euler_finite : thm
val Euler_has_1 : thm
val Euler_nonempty : thm
val Euler_prime : thm
val Euler_thm : thm
val FACTOR_OUT_POWER : thm
val FACTOR_OUT_PRIME : thm
val FACT_EQ_PROD : thm
val FACT_REDUCTION : thm
val FILTER_element_order : thm
val FINITE_BIJ_COUNT_CARD : thm
val FINITE_COUNT_IMAGE : thm
val FINITE_INJ_AS_SURJ : thm
val FINITE_INJ_IS_BIJ : thm
val FINITE_INJ_IS_SURJ : thm
val FINITE_PPOW : thm
val FINITE_SURJ_IS_INJ : thm
val FIVE : thm
val FOUR : thm
val FUNPOW_ADD1 : thm
val FUNPOW_DIV : thm
val FUNPOW_EQ_LINV : thm
val FUNPOW_GE_MONO : thm
val FUNPOW_LE_FALLING : thm
val FUNPOW_LE_MONO : thm
val FUNPOW_LE_RISING : thm
val FUNPOW_LINV_EQ : thm
val FUNPOW_LINV_INV : thm
val FUNPOW_LINV_SUB1 : thm
val FUNPOW_LINV_SUB2 : thm
val FUNPOW_LINV_closure : thm
val FUNPOW_LINV_permutes : thm
val FUNPOW_MAX : thm
val FUNPOW_MIN : thm
val FUNPOW_MOD : thm
val FUNPOW_MUL : thm
val FUNPOW_MULTIPLE : thm
val FUNPOW_PAIR : thm
val FUNPOW_SQ : thm
val FUNPOW_SQ_MOD : thm
val FUNPOW_SUB1 : thm
val FUNPOW_SUB_LINV1 : thm
val FUNPOW_SUB_LINV2 : thm
val FUNPOW_TRIPLE : thm
val FUNPOW_closure : thm
val FUNPOW_permutes : thm
val GCD_MOD_MULT_INV : thm
val GCD_SUB_MULTIPLE : thm
val GCD_SUB_MULTIPLE_COMM : thm
val HALF_ADD1_LE : thm
val HALF_ADD1_LT : thm
val HALF_DIV_TWO_POWER : thm
val HALF_EQ_0 : thm
val HALF_EQ_SELF : thm
val HALF_EVEN_LE : thm
val HALF_EXP_5 : thm
val HALF_LE : thm
val HALF_LE_MONO : thm
val HALF_LT : thm
val HALF_MULT : thm
val HALF_MULT_EVEN : thm
val HALF_ODD_LT : thm
val HALF_SQ_LE : thm
val HALF_SUC : thm
val HALF_SUC_LE : thm
val HALF_SUC_SUC : thm
val HALF_TWICE : thm
val IMAGE_COUNT_SUC : thm
val IMAGE_COUNT_SUC_BY_SUC : thm
val IMAGE_DIFF : thm
val IMAGE_ELEMENT_CONDITION : thm
val IMAGE_K : thm
val IMAGE_SUBSET_TARGET : thm
val INJ_CARD_IMAGE_EQN : thm
val INJ_IMAGE_BIJ_ALT : thm
val INJ_UNIV : thm
val INSERT_DELETE_COMM : thm
val INSERT_DELETE_NON_ELEMENT : thm
val INSERT_SUBSET_SUBSET : thm
val INTER_DIFF : thm
val IN_PPOW : thm
val IN_SING_OR_EMPTY : thm
val LCM_EXCHANGE : thm
val LESS_HALF_IFF : thm
val LESS_SUC : thm
val LE_IMP_REVERSE_LT : thm
val LE_MONO_ADD2 : thm
val LE_MONO_MULT2 : thm
val LE_MULT_LCANCEL_IMP : thm
val LE_ONE : thm
val LE_TWICE_ALT : thm
val LINV_SUBSET : thm
val LINV_permutes : thm
val LT_MONO_ADD2 : thm
val LT_MONO_MULT2 : thm
val MAX_1_EXP : thm
val MAX_1_POS : thm
val MAX_ADD : thm
val MAX_ALT : thm
val MAX_ID : thm
val MAX_IS_MAX : thm
val MAX_LESS : thm
val MAX_LE_PAIR : thm
val MAX_LE_SUM : thm
val MAX_SET_DELETE : thm
val MAX_SET_IMAGE_SUC_COUNT : thm
val MAX_SET_IMAGE_with_DEC : thm
val MAX_SET_IMAGE_with_DIV : thm
val MAX_SET_IMAGE_with_HALF : thm
val MAX_SUC : thm
val MAX_SWAP : thm
val MIN_1_EXP : thm
val MIN_1_POS : thm
val MIN_ADD : thm
val MIN_ALT : thm
val MIN_ID : thm
val MIN_IS_MIN : thm
val MIN_LE_PAIR : thm
val MIN_LE_SUM : thm
val MIN_SUC : thm
val MIN_SWAP : thm
val MOD_MULT_INV_EXISTS : thm
val MOD_MULT_LCANCEL : thm
val MOD_MULT_RCANCEL : thm
val MOD_SUC_EQN : thm
val MONOTONE_MAX : thm
val MORE_HALF_IMP : thm
val MULT3_EQ_0 : thm
val MULT3_EQ_1 : thm
val MULTIPLE_INTERVAL : thm
val MULTIPLE_SUC_LE : thm
val MULTIPLY_DIV : thm
val MULT_EQ_LESS_TO_MORE : thm
val MULT_EVEN : thm
val MULT_LE_IMP_LE : thm
val MULT_LT_IMP_LT : thm
val MULT_ODD : thm
val NOT_LT_ONE : thm
val NOT_PRIME_4 : thm
val NOT_ZERO_GE_ONE : thm
val ODD_1 : thm
val ODD_EXP : thm
val ODD_HALF : thm
val ODD_MOD2 : thm
val ODD_PRIME : thm
val ODD_SQ : thm
val ODD_SUC_HALF : thm
val ONE_LT_HALF_SQ : thm
val ONE_LT_NONZERO : thm
val ONE_LT_POS : thm
val ONE_NOT_0 : thm
val ONE_NOT_ZERO : thm
val OR_IMP_IMP : thm
val POWER_EQ_SELF : thm
val PRE_LESS : thm
val PRIME_EXP_FACTOR : thm
val PRIME_FACTOR_PROPER : thm
val PROD_SET_DIVISORS : thm
val PROD_SET_ELEMENT_DIVIDES : thm
val PROD_SET_EUCLID : thm
val PROD_SET_IMAGE_EQN : thm
val PROD_SET_IMAGE_EXP : thm
val PROD_SET_IMAGE_EXP_NONZERO : thm
val PROD_SET_LESS : thm
val PROD_SET_LESS_EQ : thm
val PROD_SET_LESS_SUC : thm
val PROD_SET_LE_CONSTANT : thm
val PROD_SET_NONZERO : thm
val PROD_SET_PRODUCT_BY_PARTITION : thm
val PROD_SET_PRODUCT_GE_CONSTANT : thm
val PROD_SET_SING : thm
val PUSH_IN_INTO_IF : thm
val SELF_LE_SQ : thm
val SET_EQ_BY_DIFF : thm
val SIGMA_CARD_FACTOR : thm
val SING_SUBSET : thm
val SPLIT_BY_SUBSET : thm
val SPLIT_CARD : thm
val SPLIT_EMPTY : thm
val SPLIT_EQ : thm
val SPLIT_EQ_DIFF : thm
val SPLIT_FINITE : thm
val SPLIT_SING : thm
val SPLIT_SUBSETS : thm
val SPLIT_SYM : thm
val SPLIT_SYM_IMP : thm
val SPLIT_UNION : thm
val SQ_0 : thm
val SQ_EQ_0 : thm
val SQ_EQ_1 : thm
val SQ_EQ_SELF : thm
val SQ_LE : thm
val SUBSET_CARD_EQ : thm
val SUBSET_DIFF_CARD : thm
val SUBSET_DIFF_DIFF : thm
val SUBSET_DIFF_EQ : thm
val SUBSET_INSERT_BOTH : thm
val SUBSET_INTER_SUBSET : thm
val SUBSET_SING_IFF : thm
val SUB_DIV_EQN : thm
val SUB_EQ_ADD : thm
val SUB_MOD_EQN : thm
val SUB_SUB_SUB : thm
val SUC_ADD_SUC : thm
val SUC_EQ : thm
val SUC_EXISTS : thm
val SUC_MAX : thm
val SUC_MIN : thm
val SUC_MULT_SUC : thm
val SUC_SQ : thm
val SUC_X_LT_2_EXP_X : thm
val SUM_IMAGE_AS_SUM_SET : thm
val SUM_IMAGE_DOUBLET : thm
val SUM_IMAGE_PSUBSET_LT : thm
val SUM_IMAGE_TRIPLET : thm
val SUM_LE_PRODUCT : thm
val SUM_SET_COUNT : thm
val SUM_SET_IMAGE_EQN : thm
val SURJ_CARD_IMAGE : thm
val THREE : thm
val TWICE_EQ_0 : thm
val TWO_HALF_LE_THM : thm
val TWO_HALF_TIMES_LE : thm
val TWO_LE_PRIME : thm
val UNION_DIFF_EQ_UNION : thm
val ZERO_LE_ALL : thm
val binomial_2 : thm
val binomial_add : thm
val binomial_means : thm
val binomial_sub : thm
val binomial_sub_add : thm
val binomial_sub_sum : thm
val card_eq_sigma_card : thm
val card_le_sigma_card : thm
val card_mod_image : thm
val card_mod_image_nonzero : thm
val coprime_all_le_imp_lt : thm
val coprime_by_le_not_divides : thm
val coprime_condition : thm
val coprime_iff_coprime_exp : thm
val coprime_linear_mod_prod : thm
val coprime_linear_mult : thm
val coprime_linear_mult_iff : thm
val coprime_mod_mod_prod_eq : thm
val coprime_mod_mod_prod_eq_iff : thm
val coprime_mod_mod_solve : thm
val coprime_multiple_linear_mod_prod : thm
val coprime_not_divides : thm
val coprime_power_and_power_predecessor : thm
val coprime_power_and_power_successor : thm
val coprime_prime_power : thm
val countFrom_0 : thm
val countFrom_SUC : thm
val countFrom_first : thm
val countFrom_less : thm
val count_SUC_by_countFrom : thm
val count_by_countFrom : thm
val difference_of_squares : thm
val difference_of_squares_alt : thm
val disjoint_bigunion_add_fun : thm
val disjoint_bigunion_card : thm
val disjoint_bigunion_mult_fun : thm
val disjoint_bigunion_sigma : thm
val dividend_divides_divisor_multiple : thm
val divides_eq_thm : thm
val divides_iff_equal : thm
val divides_self_power : thm
val equal_partition_card : thm
val equal_partition_factor : thm
val equiv_class_element : thm
val equiv_class_not_empty : thm
val euclid_coprime : thm
val euclid_prime : thm
val every_coprime_prod_set_coprime : thm
val factor_eq_cofactor : thm
val factor_partition_card : thm
val feq_class_element : thm
val feq_class_fun : thm
val feq_class_property : thm
val feq_equiv : thm
val feq_partition : thm
val feq_partition_element : thm
val feq_partition_element_exists : thm
val feq_partition_element_not_empty : thm
val feq_sum_over_partition : thm
val fequiv_equiv_class : thm
val fequiv_refl : thm
val fequiv_sym : thm
val fequiv_trans : thm
val finite_card_by_feq_partition : thm
val finite_card_by_image_preimage : thm
val finite_card_surj_by_image_preimage : thm
val finite_partition_by_predicate : thm
val finite_partition_property : thm
val fit_for_10 : thm
val fit_for_100 : thm
val gcd_divides_iff : thm
val gcd_le : thm
val gcd_linear_mod_1 : thm
val gcd_linear_mod_2 : thm
val gcd_linear_mod_prod : thm
val gcd_linear_mod_thm : thm
val gcd_linear_thm : thm
val gcd_multiple_linear_mod_prod : thm
val gcd_multiple_linear_mod_thm : thm
val gcd_powers : thm
val image_mod_subset_count : thm
val in_preimage : thm
val in_prime : thm
val inj_iff_partition_element_card_1 : thm
val inj_iff_partition_element_sing : thm
val lcm_powers : thm
val listRangeINC_sublist : thm
val listRangeLHI_sublist : thm
val mod_add_eq_sub : thm
val mod_add_eq_sub_eq : thm
val mod_divides : thm
val mod_divides_divides : thm
val mod_divides_divides_iff : thm
val mod_divides_iff : thm
val mod_eq_divides : thm
val mod_eq_divides_iff : thm
val mod_mod_prod_eq : thm
val mod_mult_eq_mult : thm
val natural_by_upto : thm
val natural_thm : thm
val nines_divisibility : thm
val nines_division_alt : thm
val nines_division_eqn : thm
val nines_divisor : thm
val nines_gcd_identity : thm
val nines_gcd_reduction : thm
val pair_disjoint_subset : thm
val pairwise_coprime_insert : thm
val pairwise_coprime_partition_coprime : thm
val pairwise_coprime_prod_set_partition : thm
val pairwise_coprime_prod_set_subset_divides : thm
val partition_as_image : thm
val partition_by_element : thm
val partition_by_subset : thm
val partition_cong : thm
val partition_element : thm
val partition_element_exists : thm
val partition_element_not_empty : thm
val partition_elements : thm
val partition_on_empty : thm
val power_divides_iff : thm
val power_eq_prime_power : thm
val power_parity : thm
val power_predecessor_divisibility : thm
val power_predecessor_division_alt : thm
val power_predecessor_division_eqn : thm
val power_predecessor_divisor : thm
val power_predecessor_gcd_identity : thm
val power_predecessor_gcd_reduction : thm
val preimage_alt : thm
val preimage_choice_property : thm
val preimage_element : thm
val preimage_finite : thm
val preimage_image_bij : thm
val preimage_image_inj : thm
val preimage_inj : thm
val preimage_inj_choice : thm
val preimage_of_image : thm
val preimage_property : thm
val preimage_subset : thm
val prime_coprime_all_less : thm
val prime_coprime_all_lt : thm
val prime_divides_power : thm
val prime_divides_prime : thm
val prime_divides_prime_power : thm
val prime_divides_self_power : thm
val prime_iff_coprime_all_lt : thm
val prime_iff_no_proper_factor : thm
val prime_power_divides_iff : thm
val prime_power_divisor : thm
val prime_power_factor : thm
val prime_powers_coprime : thm
val prime_powers_divide : thm
val prime_powers_eq : thm
val prod_set_residue : thm
val residue_0 : thm
val residue_1 : thm
val residue_card : thm
val residue_count : thm
val residue_delete : thm
val residue_element : thm
val residue_finite : thm
val residue_insert : thm
val residue_no_self : thm
val residue_no_zero : thm
val residue_nonempty : thm
val residue_prime_neq : thm
val residue_suc : thm
val residue_thm : thm
val set_add_fun_by_partition : thm
val set_additive_card : thm
val set_additive_sigma : thm
val set_card_by_partition : thm
val set_mult_fun_by_partition : thm
val set_sigma_by_partition : thm
val sigma_geometric_natural : thm
val sigma_geometric_natural_eqn : thm
val sublist_element_order : thm
val sum_image_by_composition : thm
val sum_image_by_composition_with_partial_inj : thm
val sum_image_by_composition_without_inj : thm
val sum_image_by_permutation : thm
val upto_by_count : thm
val upto_by_natural : thm
val upto_card : thm
val upto_delete : thm
val upto_finite : thm
val upto_has_last : thm
val upto_split_first : thm
val upto_split_last : thm
(*
[gcdset] Parent theory of "number"
[hol] Parent theory of "number"
[listRange] Parent theory of "number"
[logroot] Parent theory of "number"
[Euler_def] Definition
⊢ ∀n. Euler n = {i | 0 < i ∧ i < n ∧ coprime n i}
[GEN_MULT_INV_DEF] Definition
⊢ ∀n x.
1 < n ∧ 0 < x ∧ x < n ∧ coprime n x ⇒
0 < GCD_MOD_MUL_INV n x ∧ GCD_MOD_MUL_INV n x < n ∧
coprime n (GCD_MOD_MUL_INV n x) ∧
(GCD_MOD_MUL_INV n x * x) MOD n = 1
[MOD_MULT_INV_DEF] Definition
⊢ ∀p x.
prime p ∧ 0 < x ∧ x < p ⇒
0 < MOD_MULT_INV p x ∧ MOD_MULT_INV p x < p ∧
(MOD_MULT_INV p x * x) MOD p = 1
[fequiv_def] Definition
⊢ ∀x y f. (x == y) f ⇔ f x = f y
[preimage_def] Definition
⊢ ∀f s y. preimage f s y = {x | x ∈ s ∧ f x = y}
[residue_def] Definition
⊢ ∀n. residue n = {i | 0 < i ∧ i < n}
[totient_def] Definition
⊢ ∀n. totient n = CARD (Euler n)
[ADD_EQ_2] Theorem
⊢ ∀m n. 0 < m ∧ 0 < n ∧ m + n = 2 ⇒ m = 1 ∧ n = 1
[ADD_SUB_SUB] Theorem
⊢ ∀a b c. c ≤ a ⇒ a + b − (a − c) = c + b
[ALL_PRIME_FACTORS_MOD_EQ_1] Theorem
⊢ ∀m n.
0 < m ∧ 1 < n ∧ (∀p. prime p ∧ p divides m ⇒ p MOD n = 1) ⇒
m MOD n = 1
[AND_IMP_IMP] Theorem
⊢ ∀b c d. b ∧ (c ⇒ d) ⇒ (b ⇒ c) ⇒ d
[AND_IMP_OR_NEG] Theorem
⊢ ∀p q. p ∧ q ⇒ p ∨ ¬q
[BIGUNION_ELEMENTS_SING] Theorem
⊢ ∀s. BIGUNION (IMAGE (λx. {x}) s) = s
[BIJ_LINV_ELEMENT] Theorem
⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ LINV f s x ∈ s
[BIJ_LINV_THM] Theorem
⊢ ∀f s t.
BIJ f s t ⇒
(∀x. x ∈ s ⇒ LINV f s (f x) = x) ∧ ∀x. x ∈ t ⇒ f (LINV f s x) = x
[BIJ_RINV_BIJ] Theorem
⊢ ∀f s t.
BIJ f s t ∧ (∀y. y ∈ t ⇒ RINV f s y ∈ s) ⇒ BIJ (RINV f s) t s
[BIJ_RINV_INV] Theorem
⊢ ∀f s t.
BIJ f s t ∧ (∀y. y ∈ t ⇒ RINV f s y ∈ s) ⇒
∀x. x ∈ s ⇒ RINV f s (f x) = x
[BOOL_EQ] Theorem
⊢ ∀b1 b2 f. (b1 ⇔ b2) ⇒ f b1 = f b2
[CARD_BIGUNION_PAIR_DISJOINT] Theorem
⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
CARD (BIGUNION P) = ∑ CARD P
[CARD_EQ_1] Theorem
⊢ ∀s. FINITE s ⇒ (CARD s = 1 ⇔ SING s)
[CARD_PPOW] Theorem
⊢ ∀s. FINITE s ⇒ CARD (PPOW s) = PRE (2 ** CARD s)
[CARD_PPOW_EQN] Theorem
⊢ ∀s. FINITE s ⇒ CARD (PPOW s) = tops 2 (CARD s)
[CARD_UNION_3_DISJOINT] Theorem
⊢ ∀a b c.
FINITE a ∧ FINITE b ∧ FINITE c ∧ DISJOINT a b ∧ DISJOINT b c ∧
DISJOINT a c ⇒
CARD (a ∪ b ∪ c) = CARD a + CARD b + CARD c
[CARD_UNION_3_EQN] Theorem
⊢ ∀a b c.
FINITE a ∧ FINITE b ∧ FINITE c ⇒
CARD (a ∪ b ∪ c) =
CARD a + CARD b + CARD c + CARD (a ∩ b ∩ c) − CARD (a ∩ b) −
CARD (b ∩ c) − CARD (a ∩ c)
[COUNT_0] Theorem
⊢ count 0 = ∅
[COUNT_1] Theorem
⊢ count 1 = {0}
[COUNT_NOT_SELF] Theorem
⊢ ∀n. n ∉ count n
[COUNT_SUBSET] Theorem
⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n
[COUNT_SUC_BY_SUC] Theorem
⊢ ∀n. upto n = 0 INSERT natural n
[COUNT_SUC_SUBSET] Theorem
⊢ ∀n t. upto n ⊆ t ⇔ count n ⊆ t ∧ n ∈ t
[DIFF_COUNT_SUC] Theorem
⊢ ∀n t. t DIFF upto n = t DIFF count n DELETE n
[DIFF_DELETE] Theorem
⊢ ∀s t x. s DIFF t DELETE x = s DIFF (x INSERT t)
[DIFF_DIFF_EQ_INTER] Theorem
⊢ ∀s t. s DIFF (s DIFF t) = s ∩ t
[DISJOINT_DIFF] Theorem
⊢ ∀s t. DISJOINT (s DIFF t) t ∧ DISJOINT t (s DIFF t)
[DISJOINT_DIFF_IFF] Theorem
⊢ ∀s t. DISJOINT s t ⇔ s DIFF t = s
[DIVIDES_CANCEL] Theorem
⊢ ∀k. 0 < k ⇒ ∀m n. m divides n ⇔ m * k divides n * k
[DIVIDES_CANCEL_COMM] Theorem
⊢ ∀m n k. m divides n ⇒ k * m divides k * n
[DIVIDES_COFACTOR] Theorem
⊢ ∀m n. 0 < n ∧ n divides m ⇒ m DIV n divides m
[DIVIDES_FACTORS] Theorem
⊢ ∀m n. 0 < n ∧ n divides m ⇒ m = n * (m DIV n)
[DIVIDES_MOD_MOD] Theorem
⊢ ∀m n. 0 < n ∧ m divides n ⇒ ∀x. x MOD n MOD m = x MOD m
[DIVIDES_MULTIPLE_IFF] Theorem
⊢ ∀m n k. k ≠ 0 ⇒ (m divides n ⇔ k * m divides k * n)
[DIV_COMMON_FACTOR] Theorem
⊢ ∀m n. 0 < n ∧ 0 < m ⇒ ∀x. n divides x ⇒ m * x DIV (m * n) = x DIV n
[DIV_DIV_MULT] Theorem
⊢ ∀m n x.
0 < n ∧ 0 < m ∧ 0 < m DIV n ∧ n divides m ∧ m divides x ∧
m DIV n divides x ⇒
x DIV (m DIV n) = n * (x DIV m)
[DIV_LT_MONOTONE_REVERSE] Theorem
⊢ ∀x y.
0 < x ∧ 0 < y ∧ x < y ⇒
∀n. 0 < n ∧ n MOD x = 0 ⇒ n DIV y < n DIV x
[DIV_LT_SUC] Theorem
⊢ ∀m n. 0 < m ∧ 0 < n ∧ n MOD m = 0 ⇒ n DIV SUC m < n DIV m
[DIV_MULT_LESS_EQ] Theorem
⊢ ∀m n. 0 < m ⇒ m * (n DIV m) ≤ n ∧ n < m * SUC (n DIV m)
[EQ_IMP2_THM] Theorem
⊢ ∀A B. (A ⇔ B) ⇔ (A ⇒ B) ∧ ((A ⇒ B) ⇒ B ⇒ A)
[EQ_PARITY] Theorem
⊢ ∀a b. EVEN (TWICE a + b) ⇔ EVEN b
[EVEN_0] Theorem
⊢ EVEN 0
[EVEN_2] Theorem
⊢ EVEN 2
[EVEN_HALF] Theorem
⊢ ∀n. EVEN n ⇒ n = TWICE (HALF n)
[EVEN_MOD_EVEN] Theorem
⊢ ∀m. EVEN m ∧ m ≠ 0 ⇒ ∀n. EVEN n ⇔ EVEN (n MOD m)
[EVEN_MOD_ODD] Theorem
⊢ ∀m. EVEN m ∧ m ≠ 0 ⇒ ∀n. ODD n ⇔ ODD (n MOD m)
[EVEN_ODD_PRE] Theorem
⊢ ∀n. 0 < n ⇒ (EVEN n ⇔ ODD (PRE n)) ∧ (ODD n ⇔ EVEN (PRE n))
[EVEN_ODD_SUC] Theorem
⊢ ∀n. (EVEN n ⇔ ODD (SUC n)) ∧ (ODD n ⇔ EVEN (SUC n))
[EVEN_PARTNERS] Theorem
⊢ ∀n. EVEN (n * (n + 1))
[EVEN_PRIME] Theorem
⊢ ∀n. EVEN n ∧ prime n ⇔ n = 2
[EVEN_SQ] Theorem
⊢ ∀n. EVEN n² ⇔ EVEN n
[EVEN_SUC_HALF] Theorem
⊢ ∀n. EVEN n ⇒ HALF (SUC n) = HALF n
[EXP_2_EQ_0] Theorem
⊢ ∀n. n² = 0 ⇔ n = 0
[EXP_2_EVEN] Theorem
⊢ ∀n. 0 < n ⇒ EVEN (2 ** n)
[EXP_2_HALF] Theorem
⊢ ∀n. 0 < n ⇒ HALF (2 ** n) = 2 ** (n − 1)
[EXP_2_PRE_ODD] Theorem
⊢ ∀n. 0 < n ⇒ ODD (tops 2 n)
[EXP_ALT_EQN] Theorem
⊢ ∀m n.
m ** n =
if n = 0 then 1 else (if EVEN n then 1 else m) * m² ** HALF n
[EXP_BY_ADD_SUB_LE] Theorem
⊢ ∀m n. m ≤ n ⇒ ∀p. p ** n = p ** m * p ** (n − m)
[EXP_BY_ADD_SUB_LT] Theorem
⊢ ∀m n. m < n ⇒ ∀p. p ** n = p ** m * p ** (n − m)
[EXP_EQN] Theorem
⊢ ∀m n.
m ** n =
if n = 0 then 1
else if EVEN n then SQ m ** HALF n
else m * SQ m ** HALF n
[EXP_EQN_ALT] Theorem
⊢ ∀m n.
m ** n =
if n = 0 then 1 else (if EVEN n then 1 else m) * SQ m ** HALF n
[EXP_EVEN] Theorem
⊢ ∀n. EVEN n ⇒ ∀m. m ** n = SQ m ** HALF n
[EXP_EXP_BASE_LE] Theorem
⊢ ∀b c m n. m ≤ n ∧ 0 < c ⇒ b ** c ** m ≤ b ** c ** n
[EXP_EXP_LE_MONO_IMP] Theorem
⊢ ∀a b n. a ≤ b ⇒ a ** n ≤ b ** n
[EXP_EXP_SUC] Theorem
⊢ ∀x y n. x ** y ** SUC n = (x ** y) ** y ** n
[EXP_LOWER_LE_HIGH] Theorem
⊢ ∀n m. n * m ** (n − 1) + m ** n ≤ (1 + m) ** n
[EXP_LOWER_LE_LOW] Theorem
⊢ ∀n m. 1 + n * m ≤ (1 + m) ** n
[EXP_LOWER_LT_LOW] Theorem
⊢ ∀n m. 0 < m ∧ 1 < n ⇒ 1 + n * m < (1 + m) ** n
[EXP_MOD_ALT] Theorem
⊢ ∀b n m.
1 < m ⇒
b ** n MOD m =
if n = 0 then 1
else ((if EVEN n then 1 else b) * SQ b ** HALF n MOD m) MOD m
[EXP_MOD_EQN] Theorem
⊢ ∀b n m.
1 < m ⇒
b ** n MOD m =
if n = 0 then 1
else
(let
result = SQ b ** HALF n MOD m
in
if EVEN n then result else (b * result) MOD m)
[EXP_ODD] Theorem
⊢ ∀n. ODD n ⇒ ∀m. m ** n = m * SQ m ** HALF n
[EXP_SUC_DIV] Theorem
⊢ ∀m n. 0 < m ⇒ m ** SUC n DIV m = m ** n
[EXP_THM] Theorem
⊢ ∀m n.
m ** n =
if n = 0 then 1
else if n = 1 then m
else if EVEN n then SQ m ** HALF n
else m * SQ m ** HALF n
[Euler_0] Theorem
⊢ Euler 0 = ∅
[Euler_1] Theorem
⊢ Euler 1 = ∅
[Euler_card_bounds] Theorem
⊢ ∀n. totient n ≤ n ∧ (1 < n ⇒ 0 < totient n ∧ totient n < n)
[Euler_card_prime] Theorem
⊢ ∀p. prime p ⇒ totient p = p − 1
[Euler_card_upper_le] Theorem
⊢ FALLING totient
[Euler_card_upper_lt] Theorem
⊢ ∀n. 1 < n ⇒ totient n < n
[Euler_element] Theorem
⊢ ∀n x. x ∈ Euler n ⇔ 0 < x ∧ x < n ∧ coprime n x
[Euler_empty] Theorem
⊢ ∀n. Euler n = ∅ ⇔ n = 0 ∨ n = 1
[Euler_finite] Theorem
⊢ ∀n. FINITE (Euler n)
[Euler_has_1] Theorem
⊢ ∀n. 1 < n ⇒ 1 ∈ Euler n
[Euler_nonempty] Theorem
⊢ ∀n. 1 < n ⇒ Euler n ≠ ∅
[Euler_prime] Theorem
⊢ ∀p. prime p ⇒ Euler p = residue p
[Euler_thm] Theorem
⊢ ∀n. Euler n = residue n ∩ {j | coprime j n}
[FACTOR_OUT_POWER] Theorem
⊢ ∀n p.
0 < n ∧ 1 < p ∧ p divides n ⇒
∃m. p ** m divides n ∧ ¬(p divides n DIV p ** m)
[FACTOR_OUT_PRIME] Theorem
⊢ ∀n p.
0 < n ∧ prime p ∧ p divides n ⇒
∃m. 0 < m ∧ p ** m divides n ∧
∀k. coprime (p ** k) (n DIV p ** m)
[FACT_EQ_PROD] Theorem
⊢ ∀n. FACT n = PROD_SET (natural n)
[FACT_REDUCTION] Theorem
⊢ ∀n m.
m < n ⇒
FACT n = PROD_SET (IMAGE SUC (count n DIFF count m)) * FACT m
[FILTER_element_order] Theorem
⊢ ∀P ls j h.
(let
fs = FILTER P ls
in
ALL_DISTINCT ls ∧ j < h ∧ h < LENGTH fs ⇒
findi (EL j fs) ls < findi (EL h fs) ls)
[FINITE_BIJ_COUNT_CARD] Theorem
⊢ ∀s. FINITE s ⇒ ∃f. BIJ f (count (CARD s)) s
[FINITE_COUNT_IMAGE] Theorem
⊢ ∀P n. FINITE {P x | x < n}
[FINITE_INJ_AS_SURJ] Theorem
⊢ ∀f s t.
INJ f s t ∧ FINITE s ∧ FINITE t ∧ CARD s = CARD t ⇒ SURJ f s t
[FINITE_INJ_IS_BIJ] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ CARD s = CARD t ∧ INJ f s t ⇒ BIJ f s t
[FINITE_INJ_IS_SURJ] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ CARD s = CARD t ∧ INJ f s t ⇒ SURJ f s t
[FINITE_PPOW] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (PPOW s)
[FINITE_SURJ_IS_INJ] Theorem
⊢ ∀f s t. FINITE s ∧ CARD s = CARD t ∧ SURJ f s t ⇒ INJ f s t
[FIVE] Theorem
⊢ 5 = SUC 4
[FOUR] Theorem
⊢ 4 = SUC 3
[FUNPOW_ADD1] Theorem
⊢ ∀m n. FUNPOW SUC n m = m + n
[FUNPOW_DIV] Theorem
⊢ ∀b m n. 0 < b ⇒ FUNPOW (flip $DIV b) n m = m DIV b ** n
[FUNPOW_EQ_LINV] Theorem
⊢ ∀f s x n.
f PERMUTES s ∧ x ∈ s ⇒ FUNPOW (LINV f s) n (FUNPOW f n x) = x
[FUNPOW_GE_MONO] Theorem
⊢ ∀f g. (∀x. f x ≤ g x) ∧ MONO f ⇒ ∀n x. FUNPOW f n x ≤ FUNPOW g n x
[FUNPOW_LE_FALLING] Theorem
⊢ ∀f m n. FALLING f ∧ m ≤ n ⇒ ∀x. FUNPOW f n x ≤ FUNPOW f m x
[FUNPOW_LE_MONO] Theorem
⊢ ∀f g. (∀x. f x ≤ g x) ∧ MONO g ⇒ ∀n x. FUNPOW f n x ≤ FUNPOW g n x
[FUNPOW_LE_RISING] Theorem
⊢ ∀f m n. RISING f ∧ m ≤ n ⇒ ∀x. FUNPOW f m x ≤ FUNPOW f n x
[FUNPOW_LINV_EQ] Theorem
⊢ ∀f s x n.
f PERMUTES s ∧ x ∈ s ⇒ FUNPOW f n (FUNPOW (LINV f s) n x) = x
[FUNPOW_LINV_INV] Theorem
⊢ ∀f s x y n.
f PERMUTES s ∧ x ∈ s ∧ y ∈ s ⇒
(x = FUNPOW f n y ⇔ y = FUNPOW (LINV f s) n x)
[FUNPOW_LINV_SUB1] Theorem
⊢ ∀f s x m n.
f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
FUNPOW (LINV f s) (n − m) x = FUNPOW (LINV f s) n (FUNPOW f m x)
[FUNPOW_LINV_SUB2] Theorem
⊢ ∀f s x m n.
f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
FUNPOW (LINV f s) (n − m) x = FUNPOW f m (FUNPOW (LINV f s) n x)
[FUNPOW_LINV_closure] Theorem
⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW (LINV f s) n x ∈ s
[FUNPOW_LINV_permutes] Theorem
⊢ ∀f s n. f PERMUTES s ⇒ FUNPOW (LINV f s) n PERMUTES s
[FUNPOW_MAX] Theorem
⊢ ∀m n k. 0 < n ⇒ FUNPOW (λx. MAX x m) n k = MAX k m
[FUNPOW_MIN] Theorem
⊢ ∀m n k. 0 < n ⇒ FUNPOW (λx. MIN x m) n k = MIN k m
[FUNPOW_MOD] Theorem
⊢ ∀f k e.
0 < k ∧ FUNPOW f k e = e ⇒
∀n. FUNPOW f n e = FUNPOW f (n MOD k) e
[FUNPOW_MUL] Theorem
⊢ ∀b m n. FUNPOW ($* b) n m = m * b ** n
[FUNPOW_MULTIPLE] Theorem
⊢ ∀f k e. 0 < k ∧ FUNPOW f k e = e ⇒ ∀n. FUNPOW f (n * k) e = e
[FUNPOW_PAIR] Theorem
⊢ ∀f g n x y.
FUNPOW (λ(x,y). (f x,g y)) n (x,y) = (FUNPOW f n x,FUNPOW g n y)
[FUNPOW_SQ] Theorem
⊢ ∀m n. FUNPOW (λn. SQ n) n m = m ** 2 ** n
[FUNPOW_SQ_MOD] Theorem
⊢ ∀m n k.
0 < m ∧ 0 < n ⇒ FUNPOW (λn. SQ n MOD m) n k = k ** 2 ** n MOD m
[FUNPOW_SUB1] Theorem
⊢ ∀m n. FUNPOW PRE n m = m − n
[FUNPOW_SUB_LINV1] Theorem
⊢ ∀f s x m n.
f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
FUNPOW f (n − m) x = FUNPOW f n (FUNPOW (LINV f s) m x)
[FUNPOW_SUB_LINV2] Theorem
⊢ ∀f s x m n.
f PERMUTES s ∧ x ∈ s ∧ m ≤ n ⇒
FUNPOW f (n − m) x = FUNPOW (LINV f s) m (FUNPOW f n x)
[FUNPOW_TRIPLE] Theorem
⊢ ∀f g h n x y z.
FUNPOW (λ(x,y,z). (f x,g y,h z)) n (x,y,z) =
(FUNPOW f n x,FUNPOW g n y,FUNPOW h n z)
[FUNPOW_closure] Theorem
⊢ ∀f s x n. f PERMUTES s ∧ x ∈ s ⇒ FUNPOW f n x ∈ s
[FUNPOW_permutes] Theorem
⊢ ∀f s n. f PERMUTES s ⇒ FUNPOW f n PERMUTES s
[GCD_MOD_MULT_INV] Theorem
⊢ ∀n x.
1 < n ∧ 0 < x ∧ x < n ∧ coprime n x ⇒
∃y. 0 < y ∧ y < n ∧ coprime n y ∧ (y * x) MOD n = 1
[GCD_SUB_MULTIPLE] Theorem
⊢ ∀a b k. k * a ≤ b ⇒ gcd a b = gcd a (b − k * a)
[GCD_SUB_MULTIPLE_COMM] Theorem
⊢ ∀a b k. k * a ≤ b ⇒ gcd b a = gcd a (b − k * a)
[HALF_ADD1_LE] Theorem
⊢ ∀n. 0 < n ⇒ 1 + HALF n ≤ n
[HALF_ADD1_LT] Theorem
⊢ ∀n. 2 < n ⇒ 1 + HALF n < n
[HALF_DIV_TWO_POWER] Theorem
⊢ ∀m n. HALF n DIV 2 ** m = n DIV 2 ** SUC m
[HALF_EQ_0] Theorem
⊢ ∀n. HALF n = 0 ⇔ n = 0 ∨ n = 1
[HALF_EQ_SELF] Theorem
⊢ ∀n. HALF n = n ⇔ n = 0
[HALF_EVEN_LE] Theorem
⊢ ∀n m. TWICE n < m ⇒ n ≤ HALF m
[HALF_EXP_5] Theorem
⊢ ∀n. n * HALF (SQ n)² ≤ HALF (n ** 5)
[HALF_LE] Theorem
⊢ ∀n. HALF n ≤ n
[HALF_LE_MONO] Theorem
⊢ ∀x y. x ≤ y ⇒ HALF x ≤ HALF y
[HALF_LT] Theorem
⊢ ∀n. 0 < n ⇒ HALF n < n
[HALF_MULT] Theorem
⊢ ∀m n. n * HALF m ≤ HALF (n * m)
[HALF_MULT_EVEN] Theorem
⊢ ∀m n. EVEN n ⇒ HALF (m * n) = m * HALF n
[HALF_ODD_LT] Theorem
⊢ ∀n m. TWICE n + 1 < m ⇒ n < HALF m
[HALF_SQ_LE] Theorem
⊢ ∀n. (HALF n)² ≤ n² DIV 4
[HALF_SUC] Theorem
⊢ ∀n. HALF (SUC n) ≤ n
[HALF_SUC_LE] Theorem
⊢ ∀n m. n < HALF (SUC m) ⇒ TWICE n + 1 ≤ m
[HALF_SUC_SUC] Theorem
⊢ ∀n. 0 < n ⇒ HALF (SUC (SUC n)) ≤ n
[HALF_TWICE] Theorem
⊢ ∀n. HALF (TWICE n) = n
[IMAGE_COUNT_SUC] Theorem
⊢ ∀f n. IMAGE f (upto n) = f n INSERT IMAGE f (count n)
[IMAGE_COUNT_SUC_BY_SUC] Theorem
⊢ ∀f n. IMAGE f (upto n) = f 0 INSERT IMAGE (f ∘ SUC) (count n)
[IMAGE_DIFF] Theorem
⊢ ∀s t f.
s ⊆ t ∧ INJ f t 𝕌(:β) ⇒
IMAGE f (t DIFF s) = IMAGE f t DIFF IMAGE f s
[IMAGE_ELEMENT_CONDITION] Theorem
⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∀s e. e ∈ s ⇔ f e ∈ IMAGE f s
[IMAGE_K] Theorem
⊢ ∀s. s ≠ ∅ ⇒ ∀e. IMAGE (K e) s = {e}
[IMAGE_SUBSET_TARGET] Theorem
⊢ ∀f s t. (∀x. x ∈ s ⇒ f x ∈ t) ⇔ IMAGE f s ⊆ t
[INJ_CARD_IMAGE_EQN] Theorem
⊢ ∀f s. INJ f s 𝕌(:β) ∧ FINITE s ⇒ CARD (IMAGE f s) = CARD s
[INJ_IMAGE_BIJ_ALT] Theorem
⊢ ∀f s. INJ f s 𝕌(:β) ⇒ BIJ f s (IMAGE f s)
[INJ_UNIV] Theorem
⊢ ∀f s t. INJ f s t ⇒ INJ f s 𝕌(:β)
[INSERT_DELETE_COMM] Theorem
⊢ ∀s x y. x ≠ y ⇒ (x INSERT s) DELETE y = x INSERT s DELETE y
[INSERT_DELETE_NON_ELEMENT] Theorem
⊢ ∀x s. x ∉ s ⇒ (x INSERT s) DELETE x = s
[INSERT_SUBSET_SUBSET] Theorem
⊢ ∀s t x. x ∉ s ∧ x INSERT s ⊆ t ⇒ s ⊆ t DELETE x
[INTER_DIFF] Theorem
⊢ ∀s t. s ∩ (t DIFF s) = ∅ ∧ (t DIFF s) ∩ s = ∅
[IN_PPOW] Theorem
⊢ ∀s e. e ∈ PPOW s ⇒ e ⊂ s
[IN_SING_OR_EMPTY] Theorem
⊢ ∀b x y. x ∈ (if b then {y} else ∅) ⇒ x = y
[LCM_EXCHANGE] Theorem
⊢ ∀a b c. a * b = c * (a − b) ⇒ lcm a b = lcm a c
[LESS_HALF_IFF] Theorem
⊢ ∀n k. k < HALF n ⇔ k + 1 < n − k
[LESS_SUC] Theorem
⊢ ∀n. n < SUC n
[LE_IMP_REVERSE_LT] Theorem
⊢ ∀a b c d. 0 < c ∧ 0 < d ∧ a * b ≤ c * d ∧ d < b ⇒ a < c
[LE_MONO_ADD2] Theorem
⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a + c ≤ b + d
[LE_MONO_MULT2] Theorem
⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a * c ≤ b * d
[LE_MULT_LCANCEL_IMP] Theorem
⊢ ∀m n p. n ≤ p ⇒ m * n ≤ m * p
[LE_ONE] Theorem
⊢ ∀n. n ≤ 1 ⇔ n = 0 ∨ n = 1
[LE_TWICE_ALT] Theorem
⊢ ∀m n. n ≤ TWICE m ⇔ n ≠ 0 ⇒ HALF (n − 1) < m
[LINV_SUBSET] Theorem
⊢ ∀f s t. INJ f t 𝕌(:β) ∧ s ⊆ t ⇒ ∀x. x ∈ s ⇒ LINV f t (f x) = x
[LINV_permutes] Theorem
⊢ ∀f s. f PERMUTES s ⇒ LINV f s PERMUTES s
[LT_MONO_ADD2] Theorem
⊢ ∀a b c d. a < b ∧ c < d ⇒ a + c < b + d
[LT_MONO_MULT2] Theorem
⊢ ∀a b c d. a < b ∧ c < d ⇒ a * c < b * d
[MAX_1_EXP] Theorem
⊢ ∀n m. MAX 1 (m ** n) = MAX 1 m ** n
[MAX_1_POS] Theorem
⊢ ∀n. 0 < n ⇒ MAX 1 n = n
[MAX_ADD] Theorem
⊢ ∀a b c. MAX a (b + c) ≤ MAX a b + MAX a c
[MAX_ALT] Theorem
⊢ ∀m n. MAX m n = if m ≤ n then n else m
[MAX_ID] Theorem
⊢ ∀m n. MAX (MAX m n) n = MAX m n ∧ MAX m (MAX m n) = MAX m n
[MAX_IS_MAX] Theorem
⊢ ∀m n. m ≤ MAX m n ∧ n ≤ MAX m n
[MAX_LESS] Theorem
⊢ ∀x y n. x < n ∧ y < n ⇒ MAX x y < n
[MAX_LE_PAIR] Theorem
⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ MAX a c ≤ MAX b d
[MAX_LE_SUM] Theorem
⊢ ∀m n. MAX m n ≤ m + n
[MAX_SET_DELETE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ s ≠ {MIN_SET s} ⇒
MAX_SET (s DELETE MIN_SET s) = MAX_SET s
[MAX_SET_IMAGE_SUC_COUNT] Theorem
⊢ ∀n. MAX_SET (natural n) = n
[MAX_SET_IMAGE_with_DEC] Theorem
⊢ ∀f b c x. x − b ≤ c ⇒ f x ≤ MAX_SET {f x | x − b ≤ c}
[MAX_SET_IMAGE_with_DIV] Theorem
⊢ ∀f b c x. 0 < b ∧ x DIV b ≤ c ⇒ f x ≤ MAX_SET {f x | x DIV b ≤ c}
[MAX_SET_IMAGE_with_HALF] Theorem
⊢ ∀f c x. HALF x ≤ c ⇒ f x ≤ MAX_SET {f x | HALF x ≤ c}
[MAX_SUC] Theorem
⊢ ∀m n. MAX (SUC m) (SUC n) = SUC (MAX m n)
[MAX_SWAP] Theorem
⊢ ∀f. MONO f ⇒ ∀x y. f (MAX x y) = MAX (f x) (f y)
[MIN_1_EXP] Theorem
⊢ ∀n m. MIN 1 (m ** n) = MIN 1 m ** n
[MIN_1_POS] Theorem
⊢ ∀n. 0 < n ⇒ MIN 1 n = 1
[MIN_ADD] Theorem
⊢ ∀a b c. MIN a (b + c) ≤ MIN a b + MIN a c
[MIN_ALT] Theorem
⊢ ∀m n. MIN m n = if m ≤ n then m else n
[MIN_ID] Theorem
⊢ ∀m n. MIN (MIN m n) n = MIN m n ∧ MIN m (MIN m n) = MIN m n
[MIN_IS_MIN] Theorem
⊢ ∀m n. MIN m n ≤ m ∧ MIN m n ≤ n
[MIN_LE_PAIR] Theorem
⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ MIN a c ≤ MIN b d
[MIN_LE_SUM] Theorem
⊢ ∀m n. MIN m n ≤ m + n
[MIN_SUC] Theorem
⊢ ∀m n. MIN (SUC m) (SUC n) = SUC (MIN m n)
[MIN_SWAP] Theorem
⊢ ∀f. MONO f ⇒ ∀x y. f (MIN x y) = MIN (f x) (f y)
[MOD_MULT_INV_EXISTS] Theorem
⊢ ∀p x.
prime p ∧ 0 < x ∧ x < p ⇒ ∃y. 0 < y ∧ y < p ∧ (y * x) MOD p = 1
[MOD_MULT_LCANCEL] Theorem
⊢ ∀p x y z.
prime p ∧ (x * y) MOD p = (x * z) MOD p ∧ x MOD p ≠ 0 ⇒
y MOD p = z MOD p
[MOD_MULT_RCANCEL] Theorem
⊢ ∀p x y z.
prime p ∧ (y * x) MOD p = (z * x) MOD p ∧ x MOD p ≠ 0 ⇒
y MOD p = z MOD p
[MOD_SUC_EQN] Theorem
⊢ ∀m n.
0 < m ⇒ SUC (n MOD m) = SUC n MOD m + (SUC n DIV m − n DIV m) * m
[MONOTONE_MAX] Theorem
⊢ ∀f m. (∀k. k < m ⇒ f k < f (k + 1)) ⇒ ∀k. k < m ⇒ f k < f m
[MORE_HALF_IMP] Theorem
⊢ ∀n k. HALF n < k ⇒ n − k ≤ HALF n
[MULT3_EQ_0] Theorem
⊢ ∀x y z. x * y * z = 0 ⇔ x = 0 ∨ y = 0 ∨ z = 0
[MULT3_EQ_1] Theorem
⊢ ∀x y z. x * y * z = 1 ⇔ x = 1 ∧ y = 1 ∧ z = 1
[MULTIPLE_INTERVAL] Theorem
⊢ ∀n m. n divides m ⇒ ∀x. m − n < x ∧ x < m + n ∧ n divides x ⇒ x = m
[MULTIPLE_SUC_LE] Theorem
⊢ ∀n k. 0 < n ⇒ k * n + 1 ≤ (k + 1) * n
[MULTIPLY_DIV] Theorem
⊢ ∀n p q. 0 < n ∧ n divides q ⇒ p * (q DIV n) = p * q DIV n
[MULT_EQ_LESS_TO_MORE] Theorem
⊢ ∀a b c d. 0 < a ∧ 0 < b ∧ a < c ∧ a * b = c * d ⇒ d < b
[MULT_EVEN] Theorem
⊢ ∀n. EVEN n ⇒ ∀m. m * n = TWICE m * HALF n
[MULT_LE_IMP_LE] Theorem
⊢ ∀m n k. 0 < k ∧ k * m ≤ n ⇒ m ≤ n
[MULT_LT_IMP_LT] Theorem
⊢ ∀m n k. 0 < k ∧ k * m < n ⇒ m < n
[MULT_ODD] Theorem
⊢ ∀n. ODD n ⇒ ∀m. m * n = m + TWICE m * HALF n
[NOT_LT_ONE] Theorem
⊢ ∀n. ¬(1 < n) ⇔ n = 0 ∨ n = 1
[NOT_PRIME_4] Theorem
⊢ ¬prime 4
[NOT_ZERO_GE_ONE] Theorem
⊢ ∀n. n ≠ 0 ⇔ 1 ≤ n
[ODD_1] Theorem
⊢ ODD 1
[ODD_EXP] Theorem
⊢ ∀m n. 0 < n ∧ ODD m ⇒ ODD (m ** n)
[ODD_HALF] Theorem
⊢ ∀n. ODD n ⇒ n = TWICE (HALF n) + 1
[ODD_MOD2] Theorem
⊢ ∀x. ODD x ⇔ x MOD 2 = 1
[ODD_PRIME] Theorem
⊢ ∀n. prime n ∧ n ≠ 2 ⇒ ODD n
[ODD_SQ] Theorem
⊢ ∀n. ODD n² ⇔ ODD n
[ODD_SUC_HALF] Theorem
⊢ ∀n. ODD n ⇒ HALF (SUC n) = SUC (HALF n)
[ONE_LT_HALF_SQ] Theorem
⊢ ∀n. 1 < n ⇒ 1 < HALF n²
[ONE_LT_NONZERO] Theorem
⊢ ∀n. 1 < n ⇒ n ≠ 0
[ONE_LT_POS] Theorem
⊢ ∀n. 1 < n ⇒ 0 < n
[ONE_NOT_0] Theorem
⊢ 1 ≠ 0
[ONE_NOT_ZERO] Theorem
⊢ 1 ≠ 0
[OR_IMP_IMP] Theorem
⊢ ∀p q r. (p ∨ q ⇒ r) ⇒ p ∧ ¬q ⇒ r
[POWER_EQ_SELF] Theorem
⊢ ∀n. 1 < n ⇒ ∀m. n ** m = n ⇔ m = 1
[PRE_LESS] Theorem
⊢ ∀n. 0 < n ⇒ PRE n < n
[PRIME_EXP_FACTOR] Theorem
⊢ ∀p q n. prime p ∧ q divides p ** n ⇒ q = 1 ∨ p divides q
[PRIME_FACTOR_PROPER] Theorem
⊢ ∀n. 1 < n ∧ ¬prime n ⇒ ∃p. prime p ∧ p < n ∧ p divides n
[PROD_SET_DIVISORS] Theorem
⊢ ∀s. FINITE s ⇒ ∀n x. x ∈ s ∧ n divides x ⇒ n divides PROD_SET s
[PROD_SET_ELEMENT_DIVIDES] Theorem
⊢ ∀s x. FINITE s ∧ x ∈ s ⇒ x divides PROD_SET s
[PROD_SET_EUCLID] Theorem
⊢ ∀s. FINITE s ⇒
∀p. prime p ∧ p divides PROD_SET s ⇒ ∃b. b ∈ s ∧ p divides b
[PROD_SET_IMAGE_EQN] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. INJ f s 𝕌(:num) ⇒ PROD_SET (IMAGE f s) = Π f s
[PROD_SET_IMAGE_EXP] Theorem
⊢ ∀n. 1 < n ⇒
∀m. PROD_SET (IMAGE (λj. n ** j) (count m)) =
n ** SUM_SET (count m)
[PROD_SET_IMAGE_EXP_NONZERO] Theorem
⊢ ∀n m.
PROD_SET (IMAGE (λj. n ** j) (count m)) =
PROD_SET (IMAGE (λj. n ** j) (residue m))
[PROD_SET_LESS] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ 0 ∉ s ⇒
∀f. INJ f s 𝕌(:num) ∧ (∀x. x < f x) ⇒
PROD_SET s < PROD_SET (IMAGE f s)
[PROD_SET_LESS_EQ] Theorem
⊢ ∀s. FINITE s ⇒
∀f g.
INJ f s 𝕌(:num) ∧ INJ g s 𝕌(:num) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
PROD_SET (IMAGE f s) ≤ PROD_SET (IMAGE g s)
[PROD_SET_LESS_SUC] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ 0 ∉ s ⇒ PROD_SET s < PROD_SET (IMAGE SUC s)
[PROD_SET_LE_CONSTANT] Theorem
⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ x ≤ n) ⇒ PROD_SET s ≤ n ** CARD s
[PROD_SET_NONZERO] Theorem
⊢ ∀s. FINITE s ∧ 0 ∉ s ⇒ 0 < PROD_SET s
[PROD_SET_PRODUCT_BY_PARTITION] Theorem
⊢ ∀s. FINITE s ⇒
∀u v. s =|= u # v ⇒ PROD_SET s = PROD_SET u * PROD_SET v
[PROD_SET_PRODUCT_GE_CONSTANT] Theorem
⊢ ∀s. FINITE s ⇒
∀n f g.
INJ f s 𝕌(:num) ∧ INJ g s 𝕌(:num) ∧
(∀x. x ∈ s ⇒ n ≤ f x * g x) ⇒
n ** CARD s ≤ PROD_SET (IMAGE f s) * PROD_SET (IMAGE g s)
[PROD_SET_SING] Theorem
⊢ ∀x. PROD_SET {x} = x
[PUSH_IN_INTO_IF] Theorem
⊢ ∀b x s t. x ∈ (if b then s else t) ⇔ if b then x ∈ s else x ∈ t
[SELF_LE_SQ] Theorem
⊢ ∀n. n ≤ n²
[SET_EQ_BY_DIFF] Theorem
⊢ ∀s t. s = t ⇔ s ⊆ t ∧ t DIFF s = ∅
[SIGMA_CARD_FACTOR] Theorem
⊢ ∀n s.
FINITE s ∧ (∀e. e ∈ s ⇒ n divides CARD e) ⇒ n divides ∑ CARD s
[SING_SUBSET] Theorem
⊢ ∀s x. {x} ⊆ s ∧ SING s ⇔ s = {x}
[SPLIT_BY_SUBSET] Theorem
⊢ ∀s u. u ⊆ s ⇒ (let v = s DIFF u in s =|= u # v)
[SPLIT_CARD] Theorem
⊢ ∀s u v. FINITE s ∧ s =|= u # v ⇒ CARD s = CARD u + CARD v
[SPLIT_EMPTY] Theorem
⊢ ∀s t. s =|= ∅ # t ⇔ s = t
[SPLIT_EQ] Theorem
⊢ ∀s u v. s =|= u # v ⇔ u ⊆ s ∧ v = s DIFF u
[SPLIT_EQ_DIFF] Theorem
⊢ ∀s u v. s =|= u # v ⇔ u = s DIFF v ∧ v = s DIFF u
[SPLIT_FINITE] Theorem
⊢ ∀s u v. FINITE s ∧ s =|= u # v ⇒ FINITE u ∧ FINITE v
[SPLIT_SING] Theorem
⊢ ∀s v x. s =|= {x} # v ⇔ x ∈ s ∧ v = s DELETE x
[SPLIT_SUBSETS] Theorem
⊢ ∀s u v. s =|= u # v ⇒ u ⊆ s ∧ v ⊆ s
[SPLIT_SYM] Theorem
⊢ ∀s u v. s =|= u # v ⇔ s =|= v # u
[SPLIT_SYM_IMP] Theorem
⊢ ∀s u v. s =|= u # v ⇒ s =|= v # u
[SPLIT_UNION] Theorem
⊢ ∀s u v a b.
s =|= u # v ∧ v =|= a # b ⇒ s =|= u ∪ a # b ∧ u ∪ a =|= u # a
[SQ_0] Theorem
⊢ 0² = 0
[SQ_EQ_0] Theorem
⊢ ∀n. SQ n = 0 ⇔ n = 0
[SQ_EQ_1] Theorem
⊢ ∀n. SQ n = 1 ⇔ n = 1
[SQ_EQ_SELF] Theorem
⊢ ∀n. SQ n = n ⇔ n = 0 ∨ n = 1
[SQ_LE] Theorem
⊢ ∀m n. m ≤ n ⇒ SQ m ≤ SQ n
[SUBSET_CARD_EQ] Theorem
⊢ ∀s t. FINITE t ∧ s ⊆ t ⇒ (CARD s = CARD t ⇔ s = t)
[SUBSET_DIFF_CARD] Theorem
⊢ ∀a b. FINITE a ∧ b ⊆ a ⇒ CARD (a DIFF b) = CARD a − CARD b
[SUBSET_DIFF_DIFF] Theorem
⊢ ∀s t. t ⊆ s ⇒ s DIFF (s DIFF t) = t
[SUBSET_DIFF_EQ] Theorem
⊢ ∀s1 s2 t. s1 ⊆ t ∧ s2 ⊆ t ∧ t DIFF s1 = t DIFF s2 ⇒ s1 = s2
[SUBSET_INSERT_BOTH] Theorem
⊢ ∀s1 s2 x. s1 ⊆ s2 ⇒ x INSERT s1 ⊆ x INSERT s2
[SUBSET_INTER_SUBSET] Theorem
⊢ ∀s t u. s ⊆ u ⇒ s ∩ t ⊆ u
[SUBSET_SING_IFF] Theorem
⊢ ∀s x. s ⊆ {x} ⇔ s = ∅ ∨ s = {x}
[SUB_DIV_EQN] Theorem
⊢ ∀m n. 0 < n ⇒ (m − n) DIV n = if m < n then 0 else m DIV n − 1
[SUB_EQ_ADD] Theorem
⊢ ∀p. 0 < p ⇒ ∀m n. m − n = p ⇔ m = n + p
[SUB_MOD_EQN] Theorem
⊢ ∀m n. 0 < n ⇒ (m − n) MOD n = if m < n then 0 else m MOD n
[SUB_SUB_SUB] Theorem
⊢ ∀a b c. c ≤ a ⇒ a − b − (a − c) = c − b
[SUC_ADD_SUC] Theorem
⊢ ∀m n. SUC m + SUC n = m + n + 2
[SUC_EQ] Theorem
⊢ ∀m n. SUC m = SUC n ⇔ m = n
[SUC_EXISTS] Theorem
⊢ ∀n. 0 < n ⇒ ∃m. n = SUC m
[SUC_MAX] Theorem
⊢ ∀m n. SUC (MAX m n) = MAX (SUC m) (SUC n)
[SUC_MIN] Theorem
⊢ ∀m n. SUC (MIN m n) = MIN (SUC m) (SUC n)
[SUC_MULT_SUC] Theorem
⊢ ∀m n. SUC m * SUC n = m * n + m + n + 1
[SUC_SQ] Theorem
⊢ ∀n. (SUC n)² = SUC n² + TWICE n
[SUC_X_LT_2_EXP_X] Theorem
⊢ ∀n. 1 < n ⇒ SUC n < 2 ** n
[SUM_IMAGE_AS_SUM_SET] Theorem
⊢ ∀s. FINITE s ⇒
∀f. (∀x y. f x = f y ⇒ x = y) ⇒ ∑ f s = SUM_SET (IMAGE f s)
[SUM_IMAGE_DOUBLET] Theorem
⊢ ∀f x y. x ≠ y ⇒ ∑ f {x; y} = f x + f y
[SUM_IMAGE_PSUBSET_LT] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊂ s ∧ (∀x. x ∈ s ⇒ f x ≠ 0) ⇒ ∑ f t < ∑ f s
[SUM_IMAGE_TRIPLET] Theorem
⊢ ∀f x y z. x ≠ y ∧ y ≠ z ∧ z ≠ x ⇒ ∑ f {x; y; z} = f x + f y + f z
[SUM_LE_PRODUCT] Theorem
⊢ ∀m n. 1 < m ∧ 1 < n ⇒ m + n ≤ m * n
[SUM_SET_COUNT] Theorem
⊢ ∀n. SUM_SET (count n) = HALF (n * (n − 1))
[SUM_SET_IMAGE_EQN] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. INJ f s 𝕌(:num) ⇒ SUM_SET (IMAGE f s) = ∑ f s
[SURJ_CARD_IMAGE] Theorem
⊢ ∀f s t. SURJ f s t ⇒ CARD (IMAGE f s) = CARD t
[THREE] Theorem
⊢ 3 = SUC 2
[TWICE_EQ_0] Theorem
⊢ ∀n. TWICE n = 0 ⇔ n = 0
[TWO_HALF_LE_THM] Theorem
⊢ ∀n. TWICE (HALF n) ≤ n ∧ n ≤ SUC (TWICE (HALF n))
[TWO_HALF_TIMES_LE] Theorem
⊢ ∀m n. TWICE (HALF n * m) ≤ n * m
[TWO_LE_PRIME] Theorem
⊢ ∀p. prime p ⇒ 2 ≤ p
[UNION_DIFF_EQ_UNION] Theorem
⊢ ∀s t. s ∪ (t DIFF s) = s ∪ t
[ZERO_LE_ALL] Theorem
⊢ ∀n. 0 ≤ n
[binomial_2] Theorem
⊢ ∀m n. (m + n)² = m² + n² + TWICE m * n
[binomial_add] Theorem
⊢ ∀a b. (a + b)² = a² + b² + TWICE a * b
[binomial_means] Theorem
⊢ ∀a b. TWICE a * b ≤ a² + b²
[binomial_sub] Theorem
⊢ ∀a b. b ≤ a ⇒ (a − b)² = a² + b² − TWICE a * b
[binomial_sub_add] Theorem
⊢ ∀a b. b ≤ a ⇒ (a − b)² + 4 * a * b = (a + b)²
[binomial_sub_sum] Theorem
⊢ ∀a b. b ≤ a ⇒ (a − b)² + TWICE a * b = a² + b²
[card_eq_sigma_card] Theorem
⊢ ∀s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e ≠ 0) ∧ CARD s = ∑ CARD s ⇒
∀e. e ∈ s ⇒ CARD e = 1
[card_le_sigma_card] Theorem
⊢ ∀s. FINITE s ∧ (∀e. e ∈ s ⇒ CARD e ≠ 0) ⇒ CARD s ≤ ∑ CARD s
[card_mod_image] Theorem
⊢ ∀s n. 0 < n ⇒ CARD (IMAGE (λx. x MOD n) s) ≤ n
[card_mod_image_nonzero] Theorem
⊢ ∀s n.
0 < n ∧ 0 ∉ IMAGE (λx. x MOD n) s ⇒
CARD (IMAGE (λx. x MOD n) s) < n
[coprime_all_le_imp_lt] Theorem
⊢ ∀n. 1 < n ⇒ ∀m. (∀j. 0 < j ∧ j ≤ m ⇒ coprime n j) ⇒ m < n
[coprime_by_le_not_divides] Theorem
⊢ ∀m n. 1 < m ∧ (∀j. 1 < j ∧ j ≤ m ⇒ ¬(j divides n)) ⇒ coprime m n
[coprime_condition] Theorem
⊢ ∀m n.
(∀j. 1 < j ∧ j ≤ m ⇒ ¬(j divides n)) ⇔
∀j. 1 < j ∧ j ≤ m ⇒ coprime j n
[coprime_iff_coprime_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀a b. coprime a b ⇔ coprime a (b ** n)
[coprime_linear_mod_prod] Theorem
⊢ ∀a b.
0 < a ∧ 0 < b ∧ coprime a b ⇒
∃p q. (p * a + q * b) MOD (a * b) = 1 MOD (a * b)
[coprime_linear_mult] Theorem
⊢ ∀a b p q.
coprime a b ∧ coprime p b ∧ coprime q a ⇒
coprime (p * a + q * b) (a * b)
[coprime_linear_mult_iff] Theorem
⊢ ∀a b p q.
coprime a b ⇒
(coprime p b ∧ coprime q a ⇔ coprime (p * a + q * b) (a * b))
[coprime_mod_mod_prod_eq] Theorem
⊢ ∀m n a b.
0 < m ∧ 0 < n ∧ coprime m n ∧ a MOD m = b MOD m ∧
a MOD n = b MOD n ⇒
a MOD (m * n) = b MOD (m * n)
[coprime_mod_mod_prod_eq_iff] Theorem
⊢ ∀m n.
0 < m ∧ 0 < n ∧ coprime m n ⇒
∀a b.
a MOD (m * n) = b MOD (m * n) ⇔
a MOD m = b MOD m ∧ a MOD n = b MOD n
[coprime_mod_mod_solve] Theorem
⊢ ∀m n a b.
0 < m ∧ 0 < n ∧ coprime m n ⇒
∃!x. x < m * n ∧ x MOD m = a MOD m ∧ x MOD n = b MOD n
[coprime_multiple_linear_mod_prod] Theorem
⊢ ∀a b c.
0 < a ∧ 0 < b ∧ coprime a b ⇒
∃p q. (p * a + q * b) MOD (a * b) = c MOD (a * b)
[coprime_not_divides] Theorem
⊢ ∀m n. 1 < n ∧ coprime n m ⇒ ¬(n divides m)
[coprime_power_and_power_predecessor] Theorem
⊢ ∀b m n. 0 < b ∧ 0 < m ⇒ coprime (b ** n) (tops b m)
[coprime_power_and_power_successor] Theorem
⊢ ∀b m n. 0 < b ∧ 0 < m ⇒ coprime (b ** n) (b ** m + 1)
[coprime_prime_power] Theorem
⊢ ∀p n. prime p ∧ 0 < n ⇒ ∀q. coprime q (p ** n) ⇔ ¬(p divides q)
[countFrom_0] Theorem
⊢ ∀m. countFrom m 0 = ∅
[countFrom_SUC] Theorem
⊢ ∀m n m n. countFrom m (SUC n) = m INSERT countFrom (m + 1) n
[countFrom_first] Theorem
⊢ ∀m n. 0 < n ⇒ m ∈ countFrom m n
[countFrom_less] Theorem
⊢ ∀m n x. x < m ⇒ x ∉ countFrom m n
[count_SUC_by_countFrom] Theorem
⊢ ∀n. upto n = 0 INSERT countFrom 1 n
[count_by_countFrom] Theorem
⊢ ∀n. count n = countFrom 0 n
[difference_of_squares] Theorem
⊢ ∀a b. a² − b² = (a − b) * (a + b)
[difference_of_squares_alt] Theorem
⊢ ∀a b. SQ a − SQ b = (a − b) * (a + b)
[disjoint_bigunion_add_fun] Theorem
⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
∀f. SET_ADDITIVE f ⇒ f (BIGUNION P) = ∑ f P
[disjoint_bigunion_card] Theorem
⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
CARD (BIGUNION P) = ∑ CARD P
[disjoint_bigunion_mult_fun] Theorem
⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
∀f. SET_MULTIPLICATIVE f ⇒ f (BIGUNION P) = Π f P
[disjoint_bigunion_sigma] Theorem
⊢ ∀P. FINITE P ∧ EVERY_FINITE P ∧ PAIR_DISJOINT P ⇒
∀f. ∑ f (BIGUNION P) = ∑ (∑ f) P
[dividend_divides_divisor_multiple] Theorem
⊢ ∀m n. 0 < m ∧ n divides m ⇒ ∀t. m divides t * n ⇔ m DIV n divides t
[divides_eq_thm] Theorem
⊢ ∀a b. a divides b ∧ 0 < b ∧ b < TWICE a ⇒ b = a
[divides_iff_equal] Theorem
⊢ ∀m n. 0 < n ∧ n < TWICE m ⇒ (m divides n ⇔ n = m)
[divides_self_power] Theorem
⊢ ∀n p. 0 < n ∧ 1 < p ⇒ p divides p ** n
[equal_partition_card] Theorem
⊢ ∀R s n.
FINITE s ∧ R equiv_on s ∧ (∀e. e ∈ partition R s ⇒ CARD e = n) ⇒
CARD s = n * CARD (partition R s)
[equal_partition_factor] Theorem
⊢ ∀R s n.
FINITE s ∧ R equiv_on s ∧ (∀e. e ∈ partition R s ⇒ CARD e = n) ⇒
n divides CARD s
[equiv_class_element] Theorem
⊢ ∀R s x y. y ∈ equiv_class R s x ⇔ y ∈ s ∧ R x y
[equiv_class_not_empty] Theorem
⊢ ∀R s x. R equiv_on s ∧ x ∈ s ⇒ equiv_class R s x ≠ ∅
[euclid_coprime] Theorem
⊢ ∀a b c. coprime a b ∧ b divides a * c ⇒ b divides c
[euclid_prime] Theorem
⊢ ∀p a b. prime p ∧ p divides a * b ⇒ p divides a ∨ p divides b
[every_coprime_prod_set_coprime] Theorem
⊢ ∀s. FINITE s ⇒
∀x. x ∉ s ∧ (∀z. z ∈ s ⇒ coprime x z) ⇒ coprime x (PROD_SET s)
[factor_eq_cofactor] Theorem
⊢ ∀m n. 0 < m ∧ m divides n ⇒ (m = n DIV m ⇔ n = m²)
[factor_partition_card] Theorem
⊢ ∀R s n.
FINITE s ∧ R equiv_on s ∧
(∀e. e ∈ partition R s ⇒ n divides CARD e) ⇒
n divides CARD s
[feq_class_element] Theorem
⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y
[feq_class_fun] Theorem
⊢ ∀f s. preimage f s ∘ f = (λx. equiv_class (feq f) s x)
[feq_class_property] Theorem
⊢ ∀f s x. preimage f s (f x) = equiv_class (feq f) s x
[feq_equiv] Theorem
⊢ ∀s f. feq f equiv_on s
[feq_partition] Theorem
⊢ ∀s f. partition (feq f) s = IMAGE (preimage f s ∘ f) s
[feq_partition_element] Theorem
⊢ ∀s f t.
t ∈ partition (feq f) s ⇔
∃z. z ∈ s ∧ ∀x. x ∈ t ⇔ x ∈ s ∧ f x = f z
[feq_partition_element_exists] Theorem
⊢ ∀f s x. x ∈ s ⇔ ∃e. e ∈ partition (feq f) s ∧ x ∈ e
[feq_partition_element_not_empty] Theorem
⊢ ∀f s e. e ∈ partition (feq f) s ⇒ e ≠ ∅
[feq_sum_over_partition] Theorem
⊢ ∀s. FINITE s ⇒ ∀f g. ∑ g s = ∑ (∑ g) (partition (feq f) s)
[fequiv_equiv_class] Theorem
⊢ ∀f. (λx y. (x == y) f) equiv_on 𝕌(:α)
[fequiv_refl] Theorem
⊢ ∀f x. (x == x) f
[fequiv_sym] Theorem
⊢ ∀f x y. (x == y) f ⇒ (y == x) f
[fequiv_trans] Theorem
⊢ ∀f x y z. (x == y) f ∧ (y == z) f ⇒ (x == z) f
[finite_card_by_feq_partition] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. CARD s = ∑ CARD (partition (feq f) s)
[finite_card_by_image_preimage] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. CARD s = ∑ CARD (IMAGE (preimage f s ∘ f) s)
[finite_card_surj_by_image_preimage] Theorem
⊢ ∀f s t.
FINITE s ∧ SURJ f s t ⇒ CARD s = ∑ CARD (IMAGE (preimage f s) t)
[finite_partition_by_predicate] Theorem
⊢ ∀s. FINITE s ⇒
∀P. (let
u = {x | x ∈ s ∧ P x};
v = {x | x ∈ s ∧ ¬P x}
in
FINITE u ∧ FINITE v ∧ s =|= u # v)
[finite_partition_property] Theorem
⊢ ∀s. FINITE s ⇒ ∀u v. s =|= u # v ⇒ (u = ∅ ⇔ v = s)
[fit_for_10] Theorem
⊢ 1 + 2 + 3 + 4 = 10
[fit_for_100] Theorem
⊢ 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100
[gcd_divides_iff] Theorem
⊢ ∀a b c. 0 < a ⇒ (gcd a b divides c ⇔ ∃p q. p * a = q * b + c)
[gcd_le] Theorem
⊢ ∀m n. 0 < m ∧ 0 < n ⇒ gcd m n ≤ m ∧ gcd m n ≤ n
[gcd_linear_mod_1] Theorem
⊢ ∀a b. 0 < a ⇒ ∃q. (q * b) MOD a = gcd a b MOD a
[gcd_linear_mod_2] Theorem
⊢ ∀a b. 0 < b ⇒ ∃p. (p * a) MOD b = gcd a b MOD b
[gcd_linear_mod_prod] Theorem
⊢ ∀a b.
0 < a ∧ 0 < b ⇒
∃p q. (p * a + q * b) MOD (a * b) = gcd a b MOD (a * b)
[gcd_linear_mod_thm] Theorem
⊢ ∀n a b. 0 < n ∧ 0 < a ⇒ ∃p q. (p * a + q * b) MOD n = gcd a b MOD n
[gcd_linear_thm] Theorem
⊢ ∀a b c. 0 < a ⇒ (gcd a b divides c ⇔ ∃p q. p * a = q * b + c)
[gcd_multiple_linear_mod_prod] Theorem
⊢ ∀a b c.
0 < a ∧ 0 < b ∧ gcd a b divides c ⇒
∃p q. (p * a + q * b) MOD (a * b) = c MOD (a * b)
[gcd_multiple_linear_mod_thm] Theorem
⊢ ∀n a b c.
0 < n ∧ 0 < a ∧ gcd a b divides c ⇒
∃p q. (p * a + q * b) MOD n = c MOD n
[gcd_powers] Theorem
⊢ ∀b m n. gcd (b ** m) (b ** n) = b ** MIN m n
[image_mod_subset_count] Theorem
⊢ ∀s n. 0 < n ⇒ IMAGE (λx. x MOD n) s ⊆ count n
[in_preimage] Theorem
⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y
[in_prime] Theorem
⊢ ∀p. p ∈ prime ⇔ prime p
[inj_iff_partition_element_card_1] Theorem
⊢ ∀f s.
FINITE s ⇒
(INJ f s (IMAGE f s) ⇔ ∀e. e ∈ partition (feq f) s ⇒ CARD e = 1)
[inj_iff_partition_element_sing] Theorem
⊢ ∀f s. INJ f s (IMAGE f s) ⇔ ∀e. e ∈ partition (feq f) s ⇒ SING e
[lcm_powers] Theorem
⊢ ∀b m n. lcm (b ** m) (b ** n) = b ** MAX m n
[listRangeINC_sublist] Theorem
⊢ ∀m n. m < n ⇒ [m; n] ≤ [m .. n]
[listRangeLHI_sublist] Theorem
⊢ ∀m n. m + 1 < n ⇒ [m; n − 1] ≤ [m ..< n]
[mod_add_eq_sub] Theorem
⊢ ∀n a b c d.
b < n ∧ c < n ⇒
((a + b) MOD n = (c + d) MOD n ⇔
(a + (n − c)) MOD n = (d + (n − b)) MOD n)
[mod_add_eq_sub_eq] Theorem
⊢ ∀n a b c d.
0 < n ⇒
((a + b) MOD n = (c + d) MOD n ⇔
(a + (n − c MOD n)) MOD n = (d + (n − b MOD n)) MOD n)
[mod_divides] Theorem
⊢ ∀n a b. 0 < n ∧ b divides n ∧ b divides a MOD n ⇒ b divides a
[mod_divides_divides] Theorem
⊢ ∀n a b c.
0 < n ∧ a MOD n = b ∧ c divides n ∧ c divides a ⇒ c divides b
[mod_divides_divides_iff] Theorem
⊢ ∀n a b c.
0 < n ∧ a MOD n = b ∧ c divides n ⇒ (c divides a ⇔ c divides b)
[mod_divides_iff] Theorem
⊢ ∀n a b. 0 < n ∧ b divides n ⇒ (b divides a MOD n ⇔ b divides a)
[mod_eq_divides] Theorem
⊢ ∀n a b c.
0 < n ∧ a MOD n = b MOD n ∧ c divides n ∧ c divides a ⇒
c divides b
[mod_eq_divides_iff] Theorem
⊢ ∀n a b c.
0 < n ∧ a MOD n = b MOD n ∧ c divides n ⇒
(c divides a ⇔ c divides b)
[mod_mod_prod_eq] Theorem
⊢ ∀m n a b.
0 < m ∧ 0 < n ∧ a MOD (m * n) = b MOD (m * n) ⇒
a MOD m = b MOD m ∧ a MOD n = b MOD n
[mod_mult_eq_mult] Theorem
⊢ ∀m n a b.
coprime m n ∧ 0 < a ∧ a < TWICE n ∧ 0 < b ∧ b < TWICE m ∧
(m * a) MOD (m * n) = (n * b) MOD (m * n) ⇒
a = n ∧ b = m
[natural_by_upto] Theorem
⊢ ∀n. natural n = upto n DELETE 0
[natural_thm] Theorem
⊢ ∀n. natural n = set (GENLIST SUC n)
[nines_divisibility] Theorem
⊢ ∀n m. nines n divides nines m ⇔ n divides m
[nines_division_alt] Theorem
⊢ ∀m n. m ≤ n ⇒ nines n − 10 ** (n − m) * nines m = nines (n − m)
[nines_division_eqn] Theorem
⊢ ∀m n. m ≤ n ⇒ nines n = 10 ** (n − m) * nines m + nines (n − m)
[nines_divisor] Theorem
⊢ ∀n. 9 divides nines n
[nines_gcd_identity] Theorem
⊢ ∀n m. gcd (nines n) (nines m) = nines (gcd n m)
[nines_gcd_reduction] Theorem
⊢ ∀n m.
m ≤ n ⇒ gcd (nines n) (nines m) = gcd (nines m) (nines (n − m))
[pair_disjoint_subset] Theorem
⊢ ∀s t. t ⊆ s ∧ PAIR_DISJOINT s ⇒ PAIR_DISJOINT t
[pairwise_coprime_insert] Theorem
⊢ ∀s e.
e ∉ s ∧ PAIRWISE_COPRIME (e INSERT s) ⇒
(∀x. x ∈ s ⇒ coprime e x) ∧ PAIRWISE_COPRIME s
[pairwise_coprime_partition_coprime] Theorem
⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
∀u v. s =|= u # v ⇒ coprime (PROD_SET u) (PROD_SET v)
[pairwise_coprime_prod_set_partition] Theorem
⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
∀u v.
s =|= u # v ⇒
PROD_SET s = PROD_SET u * PROD_SET v ∧
coprime (PROD_SET u) (PROD_SET v)
[pairwise_coprime_prod_set_subset_divides] Theorem
⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒
∀t. t ⊆ s ⇒ PROD_SET t divides PROD_SET s
[partition_as_image] Theorem
⊢ ∀R s. partition R s = IMAGE (λx. equiv_class R s x) s
[partition_by_element] Theorem
⊢ ∀s x. x ∈ s ⇒ s =|= {x} # s DELETE x
[partition_by_subset] Theorem
⊢ ∀s u. u ⊆ s ⇒ (let v = s DIFF u in s =|= u # v)
[partition_cong] Theorem
⊢ ∀R1 R2 s1 s2. R1 = R2 ∧ s1 = s2 ⇒ partition R1 s1 = partition R2 s2
[partition_element] Theorem
⊢ ∀R s t. t ∈ partition R s ⇔ ∃x. x ∈ s ∧ t = equiv_class R s x
[partition_element_exists] Theorem
⊢ ∀R s x. R equiv_on s ⇒ (x ∈ s ⇔ ∃e. e ∈ partition R s ∧ x ∈ e)
[partition_element_not_empty] Theorem
⊢ ∀R s e. R equiv_on s ∧ e ∈ partition R s ⇒ e ≠ ∅
[partition_elements] Theorem
⊢ ∀R s. partition R s = IMAGE (λx. equiv_class R s x) s
[partition_on_empty] Theorem
⊢ ∀R. partition R ∅ = ∅
[power_divides_iff] Theorem
⊢ ∀p. 1 < p ⇒ ∀m n. p ** m divides p ** n ⇔ m ≤ n
[power_eq_prime_power] Theorem
⊢ ∀p. prime p ⇒
∀b n m. 0 < m ∧ b ** n = p ** m ⇒ ∃k. b = p ** k ∧ k * n = m
[power_parity] Theorem
⊢ ∀n. 0 < n ⇒ ∀m. (EVEN m ⇔ EVEN (m ** n)) ∧ (ODD m ⇔ ODD (m ** n))
[power_predecessor_divisibility] Theorem
⊢ ∀t n m. 1 < t ⇒ (tops t n divides tops t m ⇔ n divides m)
[power_predecessor_division_alt] Theorem
⊢ ∀t m n.
0 < t ∧ m ≤ n ⇒
tops t n − t ** (n − m) * tops t m = tops t (n − m)
[power_predecessor_division_eqn] Theorem
⊢ ∀t m n.
0 < t ∧ m ≤ n ⇒
tops t n = t ** (n − m) * tops t m + tops t (n − m)
[power_predecessor_divisor] Theorem
⊢ ∀t n. t − 1 divides tops t n
[power_predecessor_gcd_identity] Theorem
⊢ ∀t n m. gcd (tops t n) (tops t m) = tops t (gcd n m)
[power_predecessor_gcd_reduction] Theorem
⊢ ∀t n m.
m ≤ n ⇒
gcd (tops t n) (tops t m) = gcd (tops t m) (tops t (n − m))
[preimage_alt] Theorem
⊢ ∀f s y. preimage f s y = PREIMAGE f {y} ∩ s
[preimage_choice_property] Theorem
⊢ ∀f s y.
y ∈ IMAGE f s ⇒
CHOICE (preimage f s y) ∈ s ∧ f (CHOICE (preimage f s y)) = y
[preimage_element] Theorem
⊢ ∀f s x y. x ∈ preimage f s y ⇔ x ∈ s ∧ f x = y
[preimage_finite] Theorem
⊢ ∀f s y. FINITE s ⇒ FINITE (preimage f s y)
[preimage_image_bij] Theorem
⊢ ∀f s. BIJ (preimage f s) (IMAGE f s) (partition (feq f) s)
[preimage_image_inj] Theorem
⊢ ∀f s. INJ (preimage f s) (IMAGE f s) (POW s)
[preimage_inj] Theorem
⊢ ∀f s. INJ f s 𝕌(:β) ⇒ ∀x. x ∈ s ⇒ preimage f s (f x) = {x}
[preimage_inj_choice] Theorem
⊢ ∀f s. INJ f s 𝕌(:β) ⇒ ∀x. x ∈ s ⇒ CHOICE (preimage f s (f x)) = x
[preimage_of_image] Theorem
⊢ ∀f s x. x ∈ s ⇒ x ∈ preimage f s (f x)
[preimage_property] Theorem
⊢ ∀f s y x. x ∈ preimage f s y ⇒ f x = y
[preimage_subset] Theorem
⊢ ∀f s y. preimage f s y ⊆ s
[prime_coprime_all_less] Theorem
⊢ ∀m n. prime n ∧ m < n ⇒ ∀j. 0 < j ∧ j ≤ m ⇒ coprime n j
[prime_coprime_all_lt] Theorem
⊢ ∀n. prime n ⇒ ∀m. 0 < m ∧ m < n ⇒ coprime n m
[prime_divides_power] Theorem
⊢ ∀p n. prime p ∧ 0 < n ⇒ ∀b. p divides b ** n ⇔ p divides b
[prime_divides_prime] Theorem
⊢ ∀n m. prime n ∧ prime m ⇒ (n divides m ⇔ n = m)
[prime_divides_prime_power] Theorem
⊢ ∀m n k. prime m ∧ prime n ∧ m divides n ** k ⇒ m = n
[prime_divides_self_power] Theorem
⊢ ∀p. prime p ⇒ ∀n. 0 < n ⇒ p divides p ** n
[prime_iff_coprime_all_lt] Theorem
⊢ ∀n. prime n ⇔ 1 < n ∧ ∀j. 0 < j ∧ j < n ⇒ coprime n j
[prime_iff_no_proper_factor] Theorem
⊢ ∀n. prime n ⇔ 1 < n ∧ ∀j. 1 < j ∧ j < n ⇒ ¬(j divides n)
[prime_power_divides_iff] Theorem
⊢ ∀p. prime p ⇒ ∀m n. p ** m divides p ** n ⇔ m ≤ n
[prime_power_divisor] Theorem
⊢ ∀p n a. prime p ∧ a divides p ** n ⇒ ∃j. j ≤ n ∧ a = p ** j
[prime_power_factor] Theorem
⊢ ∀n p. 0 < n ∧ prime p ⇒ ∃q m. n = p ** m * q ∧ coprime p q
[prime_powers_coprime] Theorem
⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ ∀m n. coprime (p ** m) (q ** n)
[prime_powers_divide] Theorem
⊢ ∀p q.
prime p ∧ prime q ⇒
∀m n. 0 < m ⇒ (p ** m divides q ** n ⇔ p = q ∧ m ≤ n)
[prime_powers_eq] Theorem
⊢ ∀p q.
prime p ∧ prime q ⇒ ∀m n. 0 < m ∧ p ** m = q ** n ⇒ p = q ∧ m = n
[prod_set_residue] Theorem
⊢ ∀n. PROD_SET (residue n) = FACT (n − 1)
[residue_0] Theorem
⊢ residue 0 = ∅
[residue_1] Theorem
⊢ residue 1 = ∅
[residue_card] Theorem
⊢ ∀n. 0 < n ⇒ CARD (residue n) = n − 1
[residue_count] Theorem
⊢ ∀n. 0 < n ⇒ count n = 0 INSERT residue n
[residue_delete] Theorem
⊢ ∀n. 0 < n ⇒ residue n DELETE n = residue n
[residue_element] Theorem
⊢ ∀n j. j ∈ residue n ⇒ 0 < j ∧ j < n
[residue_finite] Theorem
⊢ ∀n. FINITE (residue n)
[residue_insert] Theorem
⊢ ∀n. 0 < n ⇒ residue (SUC n) = n INSERT residue n
[residue_no_self] Theorem
⊢ ∀n. n ∉ residue n
[residue_no_zero] Theorem
⊢ ∀n. 0 ∉ residue n
[residue_nonempty] Theorem
⊢ ∀n. 1 < n ⇒ residue n ≠ ∅
[residue_prime_neq] Theorem
⊢ ∀p a n.
prime p ∧ a ∈ residue p ∧ n ≤ p ⇒
∀x. x ∈ residue n ⇒ (a * n) MOD p ≠ (a * x) MOD p
[residue_suc] Theorem
⊢ ∀n. 0 < n ⇒ residue (SUC n) = n INSERT residue n
[residue_thm] Theorem
⊢ ∀n. residue n = count n DIFF {0}
[set_add_fun_by_partition] Theorem
⊢ ∀R s.
R equiv_on s ∧ FINITE s ⇒
∀f. SET_ADDITIVE f ⇒ f s = ∑ f (partition R s)
[set_additive_card] Theorem
⊢ SET_ADDITIVE CARD
[set_additive_sigma] Theorem
⊢ ∀f. SET_ADDITIVE (∑ f)
[set_card_by_partition] Theorem
⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ CARD s = ∑ CARD (partition R s)
[set_mult_fun_by_partition] Theorem
⊢ ∀R s.
R equiv_on s ∧ FINITE s ⇒
∀f. SET_MULTIPLICATIVE f ⇒ f s = Π f (partition R s)
[set_sigma_by_partition] Theorem
⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ ∀f. ∑ f s = ∑ (∑ f) (partition R s)
[sigma_geometric_natural] Theorem
⊢ ∀p. 1 < p ⇒
∀n. ∑ (λj. p ** j) (natural n) = p * tops p n DIV (p − 1)
[sigma_geometric_natural_eqn] Theorem
⊢ ∀p. 0 < p ⇒ ∀n. (p − 1) * ∑ (λj. p ** j) (natural n) = p * tops p n
[sublist_element_order] Theorem
⊢ ∀ls sl j h.
sl ≤ ls ∧ ALL_DISTINCT ls ∧ j < h ∧ h < LENGTH sl ⇒
findi (EL j sl) ls < findi (EL h sl) ls
[sum_image_by_composition] Theorem
⊢ ∀s. FINITE s ⇒
∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) s
[sum_image_by_composition_with_partial_inj] Theorem
⊢ ∀s. FINITE s ⇒
∀f. f ∅ = 0 ⇒
∀g. (∀t. FINITE t ∧ (∀x. x ∈ t ⇒ g x ≠ ∅) ⇒
INJ g t 𝕌(:β -> bool)) ⇒
∑ f (IMAGE g s) = ∑ (f ∘ g) s
[sum_image_by_composition_without_inj] Theorem
⊢ ∀s. FINITE s ⇒
∀f g.
(∀x y. x ∈ s ∧ y ∈ s ∧ g x = g y ⇒ x = y ∨ f (g x) = 0) ⇒
∑ f (IMAGE g s) = ∑ (f ∘ g) s
[sum_image_by_permutation] Theorem
⊢ ∀s. FINITE s ⇒ ∀g. g PERMUTES s ⇒ ∀f. ∑ (f ∘ g) s = ∑ f s
[upto_by_count] Theorem
⊢ ∀n. upto n = n INSERT count n
[upto_by_natural] Theorem
⊢ ∀n. upto n = 0 INSERT natural n
[upto_card] Theorem
⊢ ∀n. CARD (upto n) = SUC n
[upto_delete] Theorem
⊢ ∀n. upto n DELETE n = count n
[upto_finite] Theorem
⊢ ∀n. FINITE (upto n)
[upto_has_last] Theorem
⊢ ∀n. n ∈ upto n
[upto_split_first] Theorem
⊢ ∀n. upto n = {0} ∪ natural n
[upto_split_last] Theorem
⊢ ∀n. upto n = count n ∪ {n}
*)
end
HOL 4, Trindemossen-2