Structure extrealTheory
signature extrealTheory =
sig
type thm = Thm.thm
(* Definitions *)
val EXTREAL_PROD_IMAGE_DEF : thm
val EXTREAL_SUM_IMAGE_DEF : thm
val Q_set_def : thm
val ceiling_def : thm
val ext_liminf_def : thm
val ext_limsup_def : thm
val ext_mono_decreasing_def : thm
val ext_mono_increasing_def : thm
val ext_suminf_def : thm
val extreal_TY_DEF : thm
val extreal_abs_primitive_def : thm
val extreal_ainv_def : thm
val extreal_case_def : thm
val extreal_div_def : thm
val extreal_exp_def : thm
val extreal_inf_def : thm
val extreal_inv_def : thm
val extreal_lg_def : thm
val extreal_ln_def : thm
val extreal_logr_def : thm
val extreal_lt_def : thm
val extreal_max_def : thm
val extreal_min_def : thm
val extreal_of_num_def : thm
val extreal_pow_def : thm
val extreal_powr_def : thm
val extreal_size_def : thm
val extreal_sqrt_def : thm
val extreal_sup_def : thm
val max_fn_seq_def : thm
val open_interval_def : thm
val open_intervals_def : thm
val rational_intervals_def : thm
val real_def : thm
val real_set_def : thm
val seq_sup_def : thm
(* Theorems *)
val ABS_LE_HALF_POW2 : thm
val ADD_IN_Q : thm
val CEILING_LBOUND : thm
val CEILING_UBOUND : thm
val CMUL_IN_Q : thm
val COUNTABLE_ENUM_Q : thm
val COUNTABLE_RATIONAL_INTERVALS : thm
val CROSS_COUNTABLE_UNIV : thm
val DIV_IN_Q : thm
val EXTREAL_ARCH : thm
val EXTREAL_ARCH_POW : thm
val EXTREAL_ARCH_POW_INV : thm
val EXTREAL_EQ_LADD : thm
val EXTREAL_EQ_RADD : thm
val EXTREAL_PROD_IMAGE_DISJOINT_UNION : thm
val EXTREAL_PROD_IMAGE_EMPTY : thm
val EXTREAL_PROD_IMAGE_EQ : thm
val EXTREAL_PROD_IMAGE_IMAGE : thm
val EXTREAL_PROD_IMAGE_PAIR : thm
val EXTREAL_PROD_IMAGE_PROPERTY : thm
val EXTREAL_PROD_IMAGE_SING : thm
val EXTREAL_PROD_IMAGE_THM : thm
val EXTREAL_SUM_IMAGE_0 : thm
val EXTREAL_SUM_IMAGE_ADD : thm
val EXTREAL_SUM_IMAGE_CMUL : thm
val EXTREAL_SUM_IMAGE_COUNT : thm
val EXTREAL_SUM_IMAGE_DISJOINT_UNION : thm
val EXTREAL_SUM_IMAGE_EMPTY : thm
val EXTREAL_SUM_IMAGE_EQ : thm
val EXTREAL_SUM_IMAGE_EQ_CARD : thm
val EXTREAL_SUM_IMAGE_FINITE_CONST : thm
val EXTREAL_SUM_IMAGE_FINITE_SAME : thm
val EXTREAL_SUM_IMAGE_IF_ELIM : thm
val EXTREAL_SUM_IMAGE_IMAGE : thm
val EXTREAL_SUM_IMAGE_INSERT : thm
val EXTREAL_SUM_IMAGE_INTER_ELIM : thm
val EXTREAL_SUM_IMAGE_INTER_NONZERO : thm
val EXTREAL_SUM_IMAGE_INV_CARD_EQ_1 : thm
val EXTREAL_SUM_IMAGE_IN_IF : thm
val EXTREAL_SUM_IMAGE_IN_IF_ALT : thm
val EXTREAL_SUM_IMAGE_MONO : thm
val EXTREAL_SUM_IMAGE_MONO_SET : thm
val EXTREAL_SUM_IMAGE_NEG : thm
val EXTREAL_SUM_IMAGE_NORMAL : thm
val EXTREAL_SUM_IMAGE_NOT_INFTY : thm
val EXTREAL_SUM_IMAGE_NOT_NEGINF : thm
val EXTREAL_SUM_IMAGE_NOT_POSINF : thm
val EXTREAL_SUM_IMAGE_PERMUTES : thm
val EXTREAL_SUM_IMAGE_POS : thm
val EXTREAL_SUM_IMAGE_POS_MEM_LE : thm
val EXTREAL_SUM_IMAGE_POW : thm
val EXTREAL_SUM_IMAGE_PROPERTY : thm
val EXTREAL_SUM_IMAGE_PROPERTY_NEG : thm
val EXTREAL_SUM_IMAGE_PROPERTY_POS : thm
val EXTREAL_SUM_IMAGE_SING : thm
val EXTREAL_SUM_IMAGE_SNEG : thm
val EXTREAL_SUM_IMAGE_SPOS : thm
val EXTREAL_SUM_IMAGE_SUB : thm
val EXTREAL_SUM_IMAGE_SUM_IMAGE : thm
val EXTREAL_SUM_IMAGE_SUM_IMAGE_MONO : thm
val EXTREAL_SUM_IMAGE_THM : thm
val EXTREAL_SUM_IMAGE_ZERO : thm
val EXTREAL_SUM_IMAGE_ZERO_DIFF : thm
val EXTREAL_SUM_IMAGE_le_suminf : thm
val EXTREAL_SUP_FUN_SEQ_IMAGE : thm
val EXTREAL_SUP_FUN_SEQ_MONO_IMAGE : thm
val EXTREAL_SUP_SEQ : thm
val INV_IN_Q : thm
val MUL_IN_Q : thm
val NESTED_EXTREAL_SUM_IMAGE_REVERSE : thm
val NUM_IN_Q : thm
val OPP_IN_Q : thm
val Q_COUNTABLE : thm
val Q_DENSE_IN_R : thm
val Q_DENSE_IN_R_LEMMA : thm
val Q_INFINITE : thm
val Q_not_infty : thm
val REAL_LE_MUL_EPSILON : thm
val REAL_LE_RSUB_GE0 : thm
val SIMP_EXTREAL_ARCH : thm
val SIMP_EXTREAL_ARCH_NEG : thm
val SUB_IN_Q : thm
val abs_0 : thm
val abs_abs : thm
val abs_bounds : thm
val abs_bounds_lt : thm
val abs_div : thm
val abs_eq_0 : thm
val abs_gt_0 : thm
val abs_le_0 : thm
val abs_le_half_pow2 : thm
val abs_le_square_plus1 : thm
val abs_max : thm
val abs_mul : thm
val abs_neg : thm
val abs_not_infty : thm
val abs_pos : thm
val abs_pow2 : thm
val abs_pow_le_mono : thm
val abs_refl : thm
val abs_triangle : thm
val abs_triangle_sub : thm
val abs_unbounds : thm
val add2_sub2 : thm
val add_assoc : thm
val add_comm : thm
val add_comm_normal : thm
val add_infty : thm
val add_ldistrib : thm
val add_ldistrib_neg : thm
val add_ldistrib_normal : thm
val add_ldistrib_normal2 : thm
val add_ldistrib_pos : thm
val add_lzero : thm
val add_not_infty : thm
val add_pow2 : thm
val add_pow2_pos : thm
val add_rdistrib : thm
val add_rdistrib_normal : thm
val add_rdistrib_normal2 : thm
val add_rzero : thm
val add_sub : thm
val add_sub2 : thm
val datatype_extreal : thm
val div_add : thm
val div_add2 : thm
val div_eq_mul_linv : thm
val div_infty : thm
val div_mul_refl : thm
val div_not_infty : thm
val div_one : thm
val div_refl : thm
val div_refl_pos : thm
val entire : thm
val eq_add_sub_switch : thm
val eq_neg : thm
val eq_sub_ladd : thm
val eq_sub_ladd_normal : thm
val eq_sub_radd : thm
val eq_sub_switch : thm
val exp_0 : thm
val exp_pos : thm
val ext_mono_decreasing_suc : thm
val ext_mono_increasing_suc : thm
val ext_suminf_0 : thm
val ext_suminf_2d : thm
val ext_suminf_2d_full : thm
val ext_suminf_add : thm
val ext_suminf_alt : thm
val ext_suminf_alt' : thm
val ext_suminf_cmul : thm
val ext_suminf_cmul_alt : thm
val ext_suminf_eq : thm
val ext_suminf_eq_infty : thm
val ext_suminf_eq_infty_imp : thm
val ext_suminf_lt_infty : thm
val ext_suminf_mono : thm
val ext_suminf_pos : thm
val ext_suminf_posinf : thm
val ext_suminf_real_suminf : thm
val ext_suminf_sigma : thm
val ext_suminf_sigma' : thm
val ext_suminf_sing : thm
val ext_suminf_sub : thm
val ext_suminf_sum : thm
val ext_suminf_suminf : thm
val ext_suminf_suminf' : thm
val ext_suminf_summable : thm
val ext_suminf_sup_eq : thm
val ext_suminf_zero : thm
val extreal_11 : thm
val extreal_Axiom : thm
val extreal_abs_def : thm
val extreal_abs_ind : thm
val extreal_add_def : thm
val extreal_add_eq : thm
val extreal_add_ind : thm
val extreal_case_cong : thm
val extreal_case_eq : thm
val extreal_cases : thm
val extreal_distinct : thm
val extreal_div_eq : thm
val extreal_eq_zero : thm
val extreal_induction : thm
val extreal_inv_eq : thm
val extreal_le_def : thm
val extreal_le_eq : thm
val extreal_le_ind : thm
val extreal_lt_eq : thm
val extreal_mean : thm
val extreal_mul_def : thm
val extreal_mul_ind : thm
val extreal_nchotomy : thm
val extreal_not_infty : thm
val extreal_not_lt : thm
val extreal_sub_add : thm
val extreal_sub_def : thm
val extreal_sub_eq : thm
val extreal_sub_ind : thm
val fourth_cancel : thm
val fourths_between : thm
val gen_powr : thm
val half_between : thm
val half_cancel : thm
val half_not_infty : thm
val harmonic_series_pow_2 : thm
val inf_cminus : thm
val inf_const : thm
val inf_const_alt : thm
val inf_const_over_set : thm
val inf_empty : thm
val inf_eq : thm
val inf_eq' : thm
val inf_le : thm
val inf_le' : thm
val inf_le_imp : thm
val inf_le_imp' : thm
val inf_lt : thm
val inf_lt' : thm
val inf_lt_infty : thm
val inf_min : thm
val inf_minimal : thm
val inf_mono_subset : thm
val inf_seq : thm
val inf_sing : thm
val inf_suc : thm
val inf_univ : thm
val infty_div : thm
val inv_1over : thm
val inv_inj : thm
val inv_le_antimono : thm
val inv_lt_antimono : thm
val inv_mul : thm
val inv_not_infty : thm
val inv_one : thm
val inv_pos : thm
val inv_pos' : thm
val inv_pos_eq : thm
val ldiv_eq : thm
val ldiv_le_imp : thm
val le_01 : thm
val le_02 : thm
val le_abs : thm
val le_abs_bounds : thm
val le_add : thm
val le_add2 : thm
val le_add_neg : thm
val le_addl_imp : thm
val le_addr : thm
val le_addr_imp : thm
val le_antisym : thm
val le_div : thm
val le_epsilon : thm
val le_inf : thm
val le_inf' : thm
val le_inf_epsilon_set : thm
val le_infty : thm
val le_inv : thm
val le_ladd : thm
val le_ladd_imp : thm
val le_ldiv : thm
val le_lmul_imp : thm
val le_lneg : thm
val le_lsub_imp : thm
val le_lt : thm
val le_max : thm
val le_max1 : thm
val le_max2 : thm
val le_min : thm
val le_mul : thm
val le_mul_epsilon : thm
val le_mul_neg : thm
val le_neg : thm
val le_not_infty : thm
val le_num : thm
val le_pow2 : thm
val le_radd : thm
val le_radd_imp : thm
val le_rdiv : thm
val le_refl : thm
val le_rmul_imp : thm
val le_rsub_imp : thm
val le_sub_eq : thm
val le_sub_eq2 : thm
val le_sub_imp : thm
val le_sub_imp2 : thm
val le_sup : thm
val le_sup' : thm
val le_sup_imp : thm
val le_sup_imp' : thm
val le_sup_imp2 : thm
val le_total : thm
val le_trans : thm
val let_add : thm
val let_add2 : thm
val let_add2_alt : thm
val let_antisym : thm
val let_mul : thm
val let_total : thm
val let_trans : thm
val linv_uniq : thm
val logr_not_infty : thm
val lt_01 : thm
val lt_02 : thm
val lt_10 : thm
val lt_abs_bounds : thm
val lt_add : thm
val lt_add2 : thm
val lt_add_neg : thm
val lt_addl : thm
val lt_addr_imp : thm
val lt_antisym : thm
val lt_div : thm
val lt_imp_le : thm
val lt_imp_ne : thm
val lt_inf_epsilon : thm
val lt_inf_epsilon_set : thm
val lt_infty : thm
val lt_ladd : thm
val lt_ldiv : thm
val lt_le : thm
val lt_lmul : thm
val lt_max_between : thm
val lt_mul : thm
val lt_mul2 : thm
val lt_mul_neg : thm
val lt_neg : thm
val lt_radd : thm
val lt_rdiv : thm
val lt_rdiv_neg : thm
val lt_refl : thm
val lt_rmul : thm
val lt_sub : thm
val lt_sub' : thm
val lt_sub_imp : thm
val lt_sub_imp' : thm
val lt_sub_imp2 : thm
val lt_sup : thm
val lt_total : thm
val lt_trans : thm
val lte_add : thm
val lte_mul : thm
val lte_total : thm
val lte_trans : thm
val max_comm : thm
val max_fn_seq_compute : thm
val max_fn_seq_mono : thm
val max_infty : thm
val max_le : thm
val max_le2_imp : thm
val max_reduce : thm
val max_refl : thm
val min_comm : thm
val min_infty : thm
val min_le : thm
val min_le1 : thm
val min_le2 : thm
val min_le2_imp : thm
val min_le_between : thm
val min_reduce : thm
val min_refl : thm
val mul_assoc : thm
val mul_comm : thm
val mul_div_refl : thm
val mul_infty : thm
val mul_lcancel : thm
val mul_le : thm
val mul_le2 : thm
val mul_let : thm
val mul_linv : thm
val mul_linv_pos : thm
val mul_lneg : thm
val mul_lone : thm
val mul_lposinf : thm
val mul_lt : thm
val mul_lt2 : thm
val mul_lte : thm
val mul_lzero : thm
val mul_not_infty : thm
val mul_not_infty2 : thm
val mul_rneg : thm
val mul_rone : thm
val mul_rposinf : thm
val mul_rzero : thm
val ne_01 : thm
val ne_02 : thm
val neg_0 : thm
val neg_add : thm
val neg_eq0 : thm
val neg_minus1 : thm
val neg_mul2 : thm
val neg_neg : thm
val neg_not_posinf : thm
val neg_sub : thm
val normal_exp : thm
val normal_inv_eq : thm
val normal_powr : thm
val normal_real : thm
val normal_real_set : thm
val num_lt_infty : thm
val num_not_infty : thm
val one_pow : thm
val pos_not_neginf : thm
val pos_summable : thm
val pow2_le_eq : thm
val pow2_sqrt : thm
val pow_0 : thm
val pow_1 : thm
val pow_2 : thm
val pow_add : thm
val pow_div : thm
val pow_half_pos_le : thm
val pow_half_pos_lt : thm
val pow_half_ser : thm
val pow_half_ser' : thm
val pow_half_ser_by_e : thm
val pow_inv : thm
val pow_le : thm
val pow_le_full : thm
val pow_le_mono : thm
val pow_lt : thm
val pow_lt2 : thm
val pow_minus1 : thm
val pow_mul : thm
val pow_neg_odd : thm
val pow_not_infty : thm
val pow_pos_even : thm
val pow_pos_le : thm
val pow_pos_lt : thm
val pow_zero : thm
val pow_zero_imp : thm
val powr_0 : thm
val powr_pos : thm
val quotient_normal : thm
val rat_not_infty : thm
val rdiv_eq : thm
val real_normal : thm
val rinv_uniq : thm
val seq_sup_compute : thm
val sqrt_mono_le : thm
val sqrt_pos_le : thm
val sqrt_pos_lt : thm
val sqrt_pow2 : thm
val sub_0 : thm
val sub_add : thm
val sub_add2 : thm
val sub_eq_0 : thm
val sub_infty : thm
val sub_ldistrib : thm
val sub_le_eq : thm
val sub_le_eq2 : thm
val sub_le_imp : thm
val sub_le_imp2 : thm
val sub_le_switch : thm
val sub_le_switch2 : thm
val sub_le_zero : thm
val sub_lneg : thm
val sub_lt_eq : thm
val sub_lt_imp : thm
val sub_lt_imp2 : thm
val sub_lt_zero : thm
val sub_lt_zero2 : thm
val sub_lzero : thm
val sub_not_infty : thm
val sub_pow2 : thm
val sub_rdistrib : thm
val sub_refl : thm
val sub_rneg : thm
val sub_rzero : thm
val sub_zero_le : thm
val sub_zero_lt : thm
val sub_zero_lt2 : thm
val summable_ext_suminf : thm
val summable_ext_suminf_suminf : thm
val sup_add_mono : thm
val sup_close : thm
val sup_cmul : thm
val sup_cmult : thm
val sup_comm : thm
val sup_const : thm
val sup_const_alt : thm
val sup_const_alt' : thm
val sup_const_over_set : thm
val sup_const_over_univ : thm
val sup_countable_seq : thm
val sup_empty : thm
val sup_eq : thm
val sup_eq' : thm
val sup_le : thm
val sup_le' : thm
val sup_le_mono : thm
val sup_le_sup_imp : thm
val sup_le_sup_imp' : thm
val sup_lt : thm
val sup_lt' : thm
val sup_lt_epsilon : thm
val sup_lt_infty : thm
val sup_max : thm
val sup_maximal : thm
val sup_mono : thm
val sup_mono_ext : thm
val sup_mono_subset : thm
val sup_num : thm
val sup_seq : thm
val sup_seq_countable_seq : thm
val sup_shift : thm
val sup_sing : thm
val sup_suc : thm
val sup_sum_mono : thm
val sup_univ : thm
val third_cancel : thm
val thirds_between : thm
val zero_div : thm
val zero_pow : thm
val zero_rpow : thm
val extreal_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cardinal] Parent theory of "extreal"
[util_prob] Parent theory of "extreal"
[EXTREAL_PROD_IMAGE_DEF] Definition
⊢ ∀f s. ∏ f s = ITSET (λe acc. f e * acc) s 1
[EXTREAL_SUM_IMAGE_DEF] Definition
⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0
[Q_set_def] Definition
⊢ ℚ =
{x | ∃a b. x = &a / &b ∧ 0 < &b} ∪
{x | ∃a b. x = -(&a / &b) ∧ 0 < &b}
[ceiling_def] Definition
⊢ ∀x. ceiling (Normal x) = LEAST n. x ≤ &n
[ext_liminf_def] Definition
⊢ ∀a. liminf a = sup (IMAGE (λm. inf {a n | m ≤ n}) 𝕌(:num))
[ext_limsup_def] Definition
⊢ ∀a. limsup a = inf (IMAGE (λm. sup {a n | m ≤ n}) 𝕌(:num))
[ext_mono_decreasing_def] Definition
⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m
[ext_mono_increasing_def] Definition
⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n
[ext_suminf_def] Definition
⊢ ∀f. (∀n. 0 ≤ f n) ⇒
suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))
[extreal_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0.
∀ $var$('extreal').
(∀a0.
a0 = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
a0 =
ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
(∃a. a0 =
(λa.
ind_type$CONSTR (SUC (SUC 0)) a
(λn. ind_type$BOTTOM)) a) ⇒
$var$('extreal') a0) ⇒
$var$('extreal') a0) rep
[extreal_abs_primitive_def] Definition
⊢ abs =
WFREC (@R. WF R)
(λextreal_abs a.
case a of
−∞ => I +∞
| +∞ => I +∞
| Normal x => I (Normal (abs x)))
[extreal_ainv_def] Definition
⊢ -−∞ = +∞ ∧ -+∞ = −∞ ∧ ∀x. -Normal x = Normal (-x)
[extreal_case_def] Definition
⊢ (∀v v1 f. extreal_CASE −∞ v v1 f = v) ∧
(∀v v1 f. extreal_CASE +∞ v v1 f = v1) ∧
∀a v v1 f. extreal_CASE (Normal a) v v1 f = f a
[extreal_div_def] Definition
⊢ (∀r. Normal r / +∞ = Normal 0) ∧ (∀r. Normal r / −∞ = Normal 0) ∧
∀x r. r ≠ 0 ⇒ x / Normal r = x * (Normal r)⁻¹
[extreal_exp_def] Definition
⊢ (∀x. exp (Normal x) = Normal (exp x)) ∧ exp +∞ = +∞ ∧
exp −∞ = Normal 0
[extreal_inf_def] Definition
⊢ ∀p. inf p = -sup (IMAGE numeric_negate p)
[extreal_inv_def] Definition
⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹
[extreal_lg_def] Definition
⊢ ∀x. lg x = logr 2 x
[extreal_ln_def] Definition
⊢ (∀x. 0 < x ⇒ ln (Normal x) = Normal (ln x)) ∧ ln (Normal 0) = −∞ ∧
ln +∞ = +∞
[extreal_logr_def] Definition
⊢ (∀b x. logr b (Normal x) = Normal (logr b x)) ∧ ∀b. logr b +∞ = +∞
[extreal_lt_def] Definition
⊢ ∀x y. x < y ⇔ ¬(y ≤ x)
[extreal_max_def] Definition
⊢ ∀x y. max x y = if x ≤ y then y else x
[extreal_min_def] Definition
⊢ ∀x y. min x y = if x ≤ y then x else y
[extreal_of_num_def] Definition
⊢ ∀n. &n = Normal (&n)
[extreal_pow_def] Definition
⊢ (∀a n. Normal a pow n = Normal (a pow n)) ∧
(∀n. +∞ pow n = if n = 0 then Normal 1 else +∞) ∧
∀n. −∞ pow n =
if n = 0 then Normal 1 else if EVEN n then +∞ else −∞
[extreal_powr_def] Definition
⊢ ∀x a. x powr a = exp (a * ln x)
[extreal_size_def] Definition
⊢ extreal_size −∞ = 0 ∧ extreal_size +∞ = 0 ∧
∀a. extreal_size (Normal a) = 1
[extreal_sqrt_def] Definition
⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ sqrt +∞ = +∞
[extreal_sup_def] Definition
⊢ ∀p. sup p =
if ∀x. (∀y. p y ⇒ y ≤ x) ⇒ x = +∞ then +∞
else if ∀x. p x ⇒ x = −∞ then −∞
else Normal (sup (λr. p (Normal r)))
[max_fn_seq_def] Definition
⊢ (∀g x. max_fn_seq g 0 x = g 0 x) ∧
∀g n x.
max_fn_seq g (SUC n) x = max (max_fn_seq g n x) (g (SUC n) x)
[open_interval_def] Definition
⊢ ∀a b. open_interval a b = {x | a < x ∧ x < b}
[open_intervals_def] Definition
⊢ open_intervals = {open_interval a b | T}
[rational_intervals_def] Definition
⊢ rational_intervals = {open_interval a b | a ∈ ℚ ∧ b ∈ ℚ}
[real_def] Definition
⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r
[real_set_def] Definition
⊢ ∀s. real_set s = {real x | x ≠ +∞ ∧ x ≠ −∞ ∧ x ∈ s}
[seq_sup_def] Definition
⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
∀P n.
seq_sup P (SUC n) =
@r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow SUC n) ∧
seq_sup P n < r ∧ r < sup P
[ABS_LE_HALF_POW2] Theorem
⊢ ∀x y. abs (x * y) ≤ 1 / 2 * (x² + y²)
[ADD_IN_Q] Theorem
⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x + y ∈ ℚ
[CEILING_LBOUND] Theorem
⊢ ∀x. Normal x ≤ &ceiling (Normal x)
[CEILING_UBOUND] Theorem
⊢ ∀x. 0 ≤ x ⇒ &ceiling (Normal x) < Normal x + 1
[CMUL_IN_Q] Theorem
⊢ ∀z x. x ∈ ℚ ⇒ &z * x ∈ ℚ ∧ -&z * x ∈ ℚ
[COUNTABLE_ENUM_Q] Theorem
⊢ ∀c. COUNTABLE c ⇔ c = ∅ ∨ ∃f. c = IMAGE f ℚ
[COUNTABLE_RATIONAL_INTERVALS] Theorem
⊢ COUNTABLE rational_intervals
[CROSS_COUNTABLE_UNIV] Theorem
⊢ COUNTABLE (𝕌(:num) × 𝕌(:num))
[DIV_IN_Q] Theorem
⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ∧ y ≠ 0 ⇒ x / y ∈ ℚ
[EXTREAL_ARCH] Theorem
⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x
[EXTREAL_ARCH_POW] Theorem
⊢ ∀x. x ≠ +∞ ⇒ ∃n. x < 2 pow n
[EXTREAL_ARCH_POW_INV] Theorem
⊢ ∀e. 0 < e ⇒ ∃n. Normal ((1 / 2) pow n) < e
[EXTREAL_EQ_LADD] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y = x + z ⇔ y = z)
[EXTREAL_EQ_RADD] Theorem
⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x + z = y + z ⇔ x = y)
[EXTREAL_PROD_IMAGE_DISJOINT_UNION] Theorem
⊢ ∀s s'.
FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
∀f. ∏ f (s ∪ s') = ∏ f s * ∏ f s'
[EXTREAL_PROD_IMAGE_EMPTY] Theorem
⊢ ∀f. ∏ f ∅ = 1
[EXTREAL_PROD_IMAGE_EQ] Theorem
⊢ ∀s. FINITE s ⇒ ∀f f'. (∀x. x ∈ s ⇒ f x = f' x) ⇒ ∏ f s = ∏ f' s
[EXTREAL_PROD_IMAGE_IMAGE] Theorem
⊢ ∀s. FINITE s ⇒
∀f'.
INJ f' s (IMAGE f' s) ⇒ ∀f. ∏ f (IMAGE f' s) = ∏ (f ∘ f') s
[EXTREAL_PROD_IMAGE_PAIR] Theorem
⊢ ∀f a b. a ≠ b ⇒ ∏ f {a; b} = f a * f b
[EXTREAL_PROD_IMAGE_PROPERTY] Theorem
⊢ ∀f e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
[EXTREAL_PROD_IMAGE_SING] Theorem
⊢ ∀f e. ∏ f {e} = f e
[EXTREAL_PROD_IMAGE_THM] Theorem
⊢ ∀f. ∏ f ∅ = 1 ∧
∀e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
[EXTREAL_SUM_IMAGE_0] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = 0) ⇒ ∑ f s = 0
[EXTREAL_SUM_IMAGE_ADD] Theorem
⊢ ∀s. FINITE s ⇒
∀f f'.
(∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
(∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ⇒
∑ (λx. f x + f' x) s = ∑ f s + ∑ f' s
[EXTREAL_SUM_IMAGE_CMUL] Theorem
⊢ ∀s. FINITE s ⇒
∀f c.
(∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
∑ (λx. Normal c * f x) s = Normal c * ∑ f s
[EXTREAL_SUM_IMAGE_COUNT] Theorem
⊢ ∀f. (∀x. f x ≠ +∞) ∨ (∀x. f x ≠ −∞) ⇒
∑ f (count 2) = f 0 + f 1 ∧ ∑ f (count 3) = f 0 + f 1 + f 2 ∧
∑ f (count 4) = f 0 + f 1 + f 2 + f 3 ∧
∑ f (count 5) = f 0 + f 1 + f 2 + f 3 + f 4
[EXTREAL_SUM_IMAGE_DISJOINT_UNION] Theorem
⊢ ∀s s'.
FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
∀f. (∀x. x ∈ s ∪ s' ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ∪ s' ⇒ f x ≠ +∞) ⇒
∑ f (s ∪ s') = ∑ f s + ∑ f s'
[EXTREAL_SUM_IMAGE_EMPTY] Theorem
⊢ ∀f. ∑ f ∅ = 0
[EXTREAL_SUM_IMAGE_EQ] Theorem
⊢ ∀s. FINITE s ⇒
∀f f'.
((∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ∧ (∀x. x ∈ s ⇒ f x = f' x) ⇒
∑ f s = ∑ f' s
[EXTREAL_SUM_IMAGE_EQ_CARD] Theorem
⊢ ∀s. FINITE s ⇒ ∑ (λx. if x ∈ s then 1 else 0) s = &CARD s
[EXTREAL_SUM_IMAGE_FINITE_CONST] Theorem
⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. y ∈ P ⇒ f y = x) ⇒ ∑ f P = &CARD P * x
[EXTREAL_SUM_IMAGE_FINITE_SAME] Theorem
⊢ ∀s. FINITE s ⇒
∀f p. p ∈ s ∧ (∀q. q ∈ s ⇒ f p = f q) ⇒ ∑ f s = &CARD s * f p
[EXTREAL_SUM_IMAGE_IF_ELIM] Theorem
⊢ ∀s P f.
FINITE s ∧ (∀x. x ∈ s ⇒ P x) ∧
((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
∑ (λx. if P x then f x else 0) s = ∑ f s
[EXTREAL_SUM_IMAGE_IMAGE] Theorem
⊢ ∀s. FINITE s ⇒
∀f'.
INJ f' s (IMAGE f' s) ⇒
∀f. (∀x. x ∈ IMAGE f' s ⇒ f x ≠ −∞) ∨
(∀x. x ∈ IMAGE f' s ⇒ f x ≠ +∞) ⇒
∑ f (IMAGE f' s) = ∑ (f ∘ f') s
[EXTREAL_SUM_IMAGE_INSERT] Theorem
⊢ ∀f. (∀x. f x ≠ +∞) ∨ (∀x. f x ≠ −∞) ⇒
∀e s. FINITE s ⇒ ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
[EXTREAL_SUM_IMAGE_INTER_ELIM] Theorem
⊢ ∀s. FINITE s ⇒
∀f s'.
((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ∧
(∀x. x ∉ s' ⇒ f x = 0) ⇒
∑ f (s ∩ s') = ∑ f s
[EXTREAL_SUM_IMAGE_INTER_NONZERO] Theorem
⊢ ∀s. FINITE s ⇒
∀f. (∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
∑ f (s ∩ (λp. f p ≠ 0)) = ∑ f s
[EXTREAL_SUM_IMAGE_INV_CARD_EQ_1] Theorem
⊢ ∀s. s ≠ ∅ ∧ FINITE s ⇒
∑ (λx. if x ∈ s then (&CARD s)⁻¹ else 0) s = 1
[EXTREAL_SUM_IMAGE_IN_IF] Theorem
⊢ ∀s. FINITE s ⇒
∀f. (∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
∑ f s = ∑ (λx. if x ∈ s then f x else 0) s
[EXTREAL_SUM_IMAGE_IN_IF_ALT] Theorem
⊢ ∀s f z.
FINITE s ∧ ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
∑ f s = ∑ (λx. if x ∈ s then f x else z) s
[EXTREAL_SUM_IMAGE_MONO] Theorem
⊢ ∀s. FINITE s ⇒
∀f f'.
((∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ∧ (∀x. x ∈ s ⇒ f x ≤ f' x) ⇒
∑ f s ≤ ∑ f' s
[EXTREAL_SUM_IMAGE_MONO_SET] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
∑ f s ≤ ∑ f t
[EXTREAL_SUM_IMAGE_NEG] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ ∑ f s ≤ 0
[EXTREAL_SUM_IMAGE_NORMAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∑ (λx. Normal (f x)) s = Normal (∑ f s)
[EXTREAL_SUM_IMAGE_NOT_INFTY] Theorem
⊢ ∀f s.
(FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞) ⇒ ∑ f s ≠ −∞) ∧
(FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒ ∑ f s ≠ +∞)
[EXTREAL_SUM_IMAGE_NOT_NEGINF] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞) ⇒ ∑ f s ≠ −∞
[EXTREAL_SUM_IMAGE_NOT_POSINF] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒ ∑ f s ≠ +∞
[EXTREAL_SUM_IMAGE_PERMUTES] Theorem
⊢ ∀s. FINITE s ⇒
∀g. g PERMUTES s ⇒
∀f. (∀x. x ∈ IMAGE g s ⇒ f x ≠ −∞) ∨
(∀x. x ∈ IMAGE g s ⇒ f x ≠ +∞) ⇒
∑ (f ∘ g) s = ∑ f s
[EXTREAL_SUM_IMAGE_POS] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∑ f s
[EXTREAL_SUM_IMAGE_POS_MEM_LE] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ s ⇒ f x ≤ ∑ f s
[EXTREAL_SUM_IMAGE_POW] Theorem
⊢ ∀f s.
FINITE s ⇒
(∀x. x ∈ s ⇒ f x ≠ −∞) ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
(∑ f s)² = ∑ (λ(i,j). f i * f j) (s × s)
[EXTREAL_SUM_IMAGE_PROPERTY] Theorem
⊢ ∀f s.
FINITE s ⇒
∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ∨
(∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ⇒
∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
[EXTREAL_SUM_IMAGE_PROPERTY_NEG] Theorem
⊢ ∀f s.
FINITE s ⇒
∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ⇒
∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
[EXTREAL_SUM_IMAGE_PROPERTY_POS] Theorem
⊢ ∀f s.
FINITE s ⇒
∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ⇒
∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
[EXTREAL_SUM_IMAGE_SING] Theorem
⊢ ∀f e. ∑ f {e} = f e
[EXTREAL_SUM_IMAGE_SNEG] Theorem
⊢ ∀f s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < 0) ⇒ ∑ f s < 0
[EXTREAL_SUM_IMAGE_SPOS] Theorem
⊢ ∀f s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < ∑ f s
[EXTREAL_SUM_IMAGE_SUB] Theorem
⊢ ∀s. FINITE s ⇒
∀f f'.
(∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ +∞) ∨
(∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ −∞) ⇒
∑ (λx. f x − f' x) s = ∑ f s − ∑ f' s
[EXTREAL_SUM_IMAGE_SUM_IMAGE] Theorem
⊢ ∀s s' f.
FINITE s ∧ FINITE s' ∧
((∀x. x ∈ s × s' ⇒ f (FST x) (SND x) ≠ −∞) ∨
∀x. x ∈ s × s' ⇒ f (FST x) (SND x) ≠ +∞) ⇒
∑ (λx. ∑ (f x) s') s = ∑ (λx. f (FST x) (SND x)) (s × s')
[EXTREAL_SUM_IMAGE_SUM_IMAGE_MONO] Theorem
⊢ ∀f a b c d.
(∀m n. 0 ≤ f m n) ∧ a ≤ c ∧ b ≤ d ⇒
∑ (λi. ∑ (f i) (count a)) (count b) ≤
∑ (λi. ∑ (f i) (count c)) (count d)
[EXTREAL_SUM_IMAGE_THM] Theorem
⊢ ∀f. ∑ f ∅ = 0 ∧ (∀e. ∑ f {e} = f e) ∧
∀e s.
FINITE s ∧
((∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ∨
∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ⇒
∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
[EXTREAL_SUM_IMAGE_ZERO] Theorem
⊢ ∀s. FINITE s ⇒ ∑ (λx. 0) s = 0
[EXTREAL_SUM_IMAGE_ZERO_DIFF] Theorem
⊢ ∀s. FINITE s ⇒
∀f t.
((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ∧
(∀x. x ∈ t ⇒ f x = 0) ⇒
∑ f s = ∑ f (s DIFF t)
[EXTREAL_SUM_IMAGE_le_suminf] Theorem
⊢ ∀f n. (∀n. 0 ≤ f n) ⇒ ∑ f (count n) ≤ suminf f
[EXTREAL_SUP_FUN_SEQ_IMAGE] Theorem
⊢ ∀P P' f.
(∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ⇒
∃g. (∀n. g n ∈ P') ∧ sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P
[EXTREAL_SUP_FUN_SEQ_MONO_IMAGE] Theorem
⊢ ∀f P P'.
(∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ∧
(∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ∧ (∀x. g1 x ≤ g2 x) ⇒ f g1 ≤ f g2) ∧
(∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ⇒ (λx. max (g1 x) (g2 x)) ∈ P') ⇒
∃g. (∀n. g n ∈ P') ∧ (∀x n. g n x ≤ g (SUC n) x) ∧
sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P
[EXTREAL_SUP_SEQ] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ⇒
∃x. (∀n. x n ∈ P) ∧ (∀n. x n ≤ x (SUC n)) ∧
sup (IMAGE x 𝕌(:num)) = sup P
[INV_IN_Q] Theorem
⊢ ∀x. x ∈ ℚ ∧ x ≠ 0 ⇒ 1 / x ∈ ℚ
[MUL_IN_Q] Theorem
⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x * y ∈ ℚ
[NESTED_EXTREAL_SUM_IMAGE_REVERSE] Theorem
⊢ ∀f s s'.
FINITE s ∧ FINITE s' ∧ (∀x y. x ∈ s ∧ y ∈ s' ⇒ f x y ≠ −∞) ⇒
∑ (λx. ∑ (f x) s') s = ∑ (λx. ∑ (λy. f y x) s) s'
[NUM_IN_Q] Theorem
⊢ ∀n. &n ∈ ℚ ∧ -&n ∈ ℚ
[OPP_IN_Q] Theorem
⊢ ∀x. x ∈ ℚ ⇒ -x ∈ ℚ
[Q_COUNTABLE] Theorem
⊢ COUNTABLE ℚ
[Q_DENSE_IN_R] Theorem
⊢ ∀x y. x < y ⇒ ∃r. r ∈ ℚ ∧ x < r ∧ r < y
[Q_DENSE_IN_R_LEMMA] Theorem
⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ ℚ ∧ x < r ∧ r < y
[Q_INFINITE] Theorem
⊢ INFINITE ℚ
[Q_not_infty] Theorem
⊢ ∀x. x ∈ ℚ ⇒ ∃y. x = Normal y
[REAL_LE_MUL_EPSILON] Theorem
⊢ ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
[REAL_LE_RSUB_GE0] Theorem
⊢ ∀x y. x ≤ y ⇔ 0 ≤ y − x
[SIMP_EXTREAL_ARCH] Theorem
⊢ ∀x. x ≠ +∞ ⇒ ∃n. x ≤ &n
[SIMP_EXTREAL_ARCH_NEG] Theorem
⊢ ∀x. x ≠ −∞ ⇒ ∃n. -&n ≤ x
[SUB_IN_Q] Theorem
⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x − y ∈ ℚ
[abs_0] Theorem
⊢ abs 0 = 0
[abs_abs] Theorem
⊢ ∀x. abs (abs x) = abs x
[abs_bounds] Theorem
⊢ ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k
[abs_bounds_lt] Theorem
⊢ ∀x k. abs x < k ⇔ -k < x ∧ x < k
[abs_div] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ 0 ⇒ abs (x / y) = abs x / abs y
[abs_eq_0] Theorem
⊢ ∀x. abs x = 0 ⇔ x = 0
[abs_gt_0] Theorem
⊢ ∀x. 0 < abs x ⇔ x ≠ 0
[abs_le_0] Theorem
⊢ ∀x. abs x ≤ 0 ⇔ x = 0
[abs_le_half_pow2] Theorem
⊢ ∀x y. abs (x * y) ≤ Normal (1 / 2) * (x² + y²)
[abs_le_square_plus1] Theorem
⊢ ∀x. abs x ≤ x² + 1
[abs_max] Theorem
⊢ ∀x. abs x = max x (-x)
[abs_mul] Theorem
⊢ ∀x y. abs (x * y) = abs x * abs y
[abs_neg] Theorem
⊢ ∀x. x < 0 ⇒ abs x = -x
[abs_not_infty] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞
[abs_pos] Theorem
⊢ ∀x. 0 ≤ abs x
[abs_pow2] Theorem
⊢ ∀x. (abs x)² = x²
[abs_pow_le_mono] Theorem
⊢ ∀x n m. n ≤ m ⇒ abs x pow n ≤ 1 + abs x pow m
[abs_refl] Theorem
⊢ ∀x. abs x = x ⇔ 0 ≤ x
[abs_triangle] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y
[abs_triangle_sub] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (x − y)
[abs_unbounds] Theorem
⊢ ∀x k. 0 ≤ k ⇒ (k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x)
[add2_sub2] Theorem
⊢ ∀a b c d.
a ≠ +∞ ∧ b ≠ +∞ ∧ c ≠ +∞ ∧ d ≠ +∞ ∧ a ≠ −∞ ∧ b ≠ −∞ ∧ c ≠ −∞ ∧
d ≠ −∞ ⇒
a − b + (c − d) = a + c − (b + d)
[add_assoc] Theorem
⊢ ∀x y z.
x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ +∞ ⇒
x + (y + z) = x + y + z
[add_comm] Theorem
⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y = y + x
[add_comm_normal] Theorem
⊢ ∀x y. Normal x + y = y + Normal x
[add_infty] Theorem
⊢ (∀x. x ≠ −∞ ⇒ x + +∞ = +∞ ∧ +∞ + x = +∞) ∧
∀x. x ≠ +∞ ⇒ x + −∞ = −∞ ∧ −∞ + x = −∞
[add_ldistrib] Theorem
⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z
[add_ldistrib_neg] Theorem
⊢ ∀x y z. y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z
[add_ldistrib_normal] Theorem
⊢ ∀r y z.
y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
Normal r * (y + z) = Normal r * y + Normal r * z
[add_ldistrib_normal2] Theorem
⊢ ∀r y z.
y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
Normal r * (y + z) = Normal r * y + Normal r * z
[add_ldistrib_pos] Theorem
⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ⇒ x * (y + z) = x * y + x * z
[add_lzero] Theorem
⊢ ∀x. 0 + x = x
[add_not_infty] Theorem
⊢ ∀x y.
(x ≠ −∞ ∧ y ≠ −∞ ⇒ x + y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y ≠ +∞)
[add_pow2] Theorem
⊢ ∀x y.
x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒
(x + y)² = x² + y² + 2 * x * y
[add_pow2_pos] Theorem
⊢ ∀x y. 0 < x ∧ x ≠ +∞ ∧ 0 ≤ y ⇒ (x + y)² = x² + y² + 2 * x * y
[add_rdistrib] Theorem
⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ (y + z) * x = y * x + z * x
[add_rdistrib_normal] Theorem
⊢ ∀x y z.
y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
(y + z) * Normal x = y * Normal x + z * Normal x
[add_rdistrib_normal2] Theorem
⊢ ∀x y z.
y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
(y + z) * Normal x = y * Normal x + z * Normal x
[add_rzero] Theorem
⊢ ∀x. x + 0 = x
[add_sub] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x + y − y = x
[add_sub2] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ y + x − y = x
[datatype_extreal] Theorem
⊢ DATATYPE (extreal −∞ +∞ Normal)
[div_add] Theorem
⊢ ∀x y z.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒
x / z + y / z = (x + y) / z
[div_add2] Theorem
⊢ ∀x y z.
(x ≠ +∞ ∧ y ≠ +∞ ∨ x ≠ −∞ ∧ y ≠ −∞) ∧ z ≠ 0 ∧ z ≠ +∞ ∧ z ≠ −∞ ⇒
x / z + y / z = (x + y) / z
[div_eq_mul_linv] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = y⁻¹ * x
[div_infty] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ x / +∞ = 0 ∧ x / −∞ = 0
[div_mul_refl] Theorem
⊢ ∀x r. r ≠ 0 ⇒ x = x / Normal r * Normal r
[div_not_infty] Theorem
⊢ ∀x y. y ≠ 0 ⇒ Normal x / y ≠ +∞ ∧ Normal x / y ≠ −∞
[div_one] Theorem
⊢ ∀x. x / 1 = x
[div_refl] Theorem
⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x / x = 1
[div_refl_pos] Theorem
⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x / x = 1
[entire] Theorem
⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
[eq_add_sub_switch] Theorem
⊢ ∀a b c d.
b ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ c ≠ +∞ ⇒
(a + b = c + d ⇔ a − c = d − b)
[eq_neg] Theorem
⊢ ∀x y. -x = -y ⇔ x = y
[eq_sub_ladd] Theorem
⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x = y − z ⇔ x + z = y)
[eq_sub_ladd_normal] Theorem
⊢ ∀x y z. x = y − Normal z ⇔ x + Normal z = y
[eq_sub_radd] Theorem
⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y = z ⇔ x = z + y)
[eq_sub_switch] Theorem
⊢ ∀x y z. x = Normal z − y ⇔ y = Normal z − x
[exp_0] Theorem
⊢ exp 0 = 1
[exp_pos] Theorem
⊢ ∀x. 0 ≤ exp x
[ext_mono_decreasing_suc] Theorem
⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n
[ext_mono_increasing_suc] Theorem
⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)
[ext_suminf_0] Theorem
⊢ suminf (λn. 0) = 0
[ext_suminf_2d] Theorem
⊢ ∀f g h.
(∀m n. 0 ≤ f m n) ∧ (∀n. suminf (f n) = g n) ∧ suminf g < +∞ ∧
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
suminf (UNCURRY f ∘ h) = suminf g
[ext_suminf_2d_full] Theorem
⊢ ∀f g h.
(∀m n. 0 ≤ f m n) ∧ (∀n. suminf (f n) = g n) ∧
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
suminf (UNCURRY f ∘ h) = suminf g
[ext_suminf_add] Theorem
⊢ ∀f g.
(∀n. 0 ≤ f n ∧ 0 ≤ g n) ⇒
suminf (λn. f n + g n) = suminf f + suminf g
[ext_suminf_alt] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ⇒
suminf (λx. f x) = sup {∑ (λi. f i) (count n) | n ∈ 𝕌(:num)}
[ext_suminf_alt'] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ⇒ suminf (λx. f x) = sup {∑ f (count n) | n | T}
[ext_suminf_cmul] Theorem
⊢ ∀f c. 0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒ suminf (λn. c * f n) = c * suminf f
[ext_suminf_cmul_alt] Theorem
⊢ ∀f c.
0 ≤ c ∧ (∀n. 0 ≤ f n) ∧ (∀n. f n < +∞) ⇒
suminf (λn. Normal c * f n) = Normal c * suminf f
[ext_suminf_eq] Theorem
⊢ ∀f g. (∀n. f n = g n) ⇒ suminf f = suminf g
[ext_suminf_eq_infty] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)) ⇒
suminf f = +∞
[ext_suminf_eq_infty_imp] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f = +∞ ⇒
∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)
[ext_suminf_lt_infty] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f < +∞ ⇒ ∀n. f n < +∞
[ext_suminf_mono] Theorem
⊢ ∀f g. (∀n. 0 ≤ g n) ∧ (∀n. g n ≤ f n) ⇒ suminf g ≤ suminf f
[ext_suminf_pos] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
[ext_suminf_posinf] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃n. f n = +∞) ⇒ suminf f = +∞
[ext_suminf_real_suminf] Theorem
⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒
suminf (real ∘ g) = real (suminf g)
[ext_suminf_sigma] Theorem
⊢ ∀f n.
(∀i x. i < n ⇒ 0 ≤ f i x) ⇒
∑ (suminf ∘ f) (count n) = suminf (λx. ∑ (λi. f i x) (count n))
[ext_suminf_sigma'] Theorem
⊢ ∀f n.
(∀i x. i < n ⇒ 0 ≤ f i x) ⇒
∑ (λx. suminf (f x)) (count n) =
suminf (λx. ∑ (λi. f i x) (count n))
[ext_suminf_sing] Theorem
⊢ ∀r. 0 ≤ r ⇒ suminf (λn. if n = 0 then r else 0) = r
[ext_suminf_sub] Theorem
⊢ ∀f g.
(∀n. 0 ≤ g n ∧ g n ≤ f n) ∧ suminf f ≠ +∞ ⇒
suminf (λi. f i − g i) = suminf f − suminf g
[ext_suminf_sum] Theorem
⊢ ∀f n.
(∀n. 0 ≤ f n) ∧ (∀m. n ≤ m ⇒ f m = 0) ⇒ suminf f = ∑ f (count n)
[ext_suminf_suminf] Theorem
⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (λn. Normal (r n)) ≠ +∞ ⇒
suminf (λn. Normal (r n)) = Normal (suminf r)
[ext_suminf_suminf'] Theorem
⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (Normal ∘ r) < +∞ ⇒
suminf (Normal ∘ r) = Normal (suminf r)
[ext_suminf_summable] Theorem
⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒ summable (real ∘ g)
[ext_suminf_sup_eq] Theorem
⊢ ∀f. (∀i m n. m ≤ n ⇒ (λx. f x i) m ≤ (λx. f x i) n) ∧
(∀n i. 0 ≤ f n i) ⇒
suminf (λi. sup {f n i | n ∈ 𝕌(:num)}) =
sup {suminf (λi. f n i) | n ∈ 𝕌(:num)}
[ext_suminf_zero] Theorem
⊢ ∀f. (∀n. f n = 0) ⇒ suminf f = 0
[extreal_11] Theorem
⊢ ∀a a'. Normal a = Normal a' ⇔ a = a'
[extreal_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn. fn −∞ = f0 ∧ fn +∞ = f1 ∧ ∀a. fn (Normal a) = f2 a
[extreal_abs_def] Theorem
⊢ abs (Normal x) = Normal (abs x) ∧ abs −∞ = +∞ ∧ abs +∞ = +∞
[extreal_abs_ind] Theorem
⊢ ∀P. (∀x. P (Normal x)) ∧ P −∞ ∧ P +∞ ⇒ ∀v. P v
[extreal_add_def] Theorem
⊢ Normal x + Normal y = Normal (x + y) ∧ Normal v0 + −∞ = −∞ ∧
Normal v0 + +∞ = +∞ ∧ −∞ + Normal v1 = −∞ ∧ +∞ + Normal v1 = +∞ ∧
−∞ + −∞ = −∞ ∧ +∞ + +∞ = +∞
[extreal_add_eq] Theorem
⊢ ∀x y. Normal x + Normal y = Normal (x + y)
[extreal_add_ind] Theorem
⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P (Normal v0) −∞) ∧
(∀v0. P (Normal v0) +∞) ∧ (∀v1. P −∞ (Normal v1)) ∧
(∀v1. P +∞ (Normal v1)) ∧ P −∞ −∞ ∧ P +∞ +∞ ∧ P −∞ +∞ ∧ P +∞ −∞ ⇒
∀v v1. P v v1
[extreal_case_cong] Theorem
⊢ ∀M M' v v1 f.
M = M' ∧ (M' = −∞ ⇒ v = v') ∧ (M' = +∞ ⇒ v1 = v1') ∧
(∀a. M' = Normal a ⇒ f a = f' a) ⇒
extreal_CASE M v v1 f = extreal_CASE M' v' v1' f'
[extreal_case_eq] Theorem
⊢ extreal_CASE x v v1 f = v' ⇔
x = −∞ ∧ v = v' ∨ x = +∞ ∧ v1 = v' ∨ ∃r. x = Normal r ∧ f r = v'
[extreal_cases] Theorem
⊢ ∀x. x = −∞ ∨ x = +∞ ∨ ∃r. x = Normal r
[extreal_distinct] Theorem
⊢ −∞ ≠ +∞ ∧ (∀a. −∞ ≠ Normal a) ∧ ∀a. +∞ ≠ Normal a
[extreal_div_eq] Theorem
⊢ ∀x y. y ≠ 0 ⇒ Normal x / Normal y = Normal (x / y)
[extreal_eq_zero] Theorem
⊢ ∀x. Normal x = 0 ⇔ x = 0
[extreal_induction] Theorem
⊢ ∀P. P −∞ ∧ P +∞ ∧ (∀r. P (Normal r)) ⇒ ∀e. P e
[extreal_inv_eq] Theorem
⊢ ∀x. x ≠ 0 ⇒ (Normal x)⁻¹ = Normal x⁻¹
[extreal_le_def] Theorem
⊢ (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (−∞ ≤ v0 ⇔ T) ∧ (+∞ ≤ +∞ ⇔ T) ∧
(Normal v5 ≤ +∞ ⇔ T) ∧ (+∞ ≤ −∞ ⇔ F) ∧ (Normal v6 ≤ −∞ ⇔ F) ∧
(+∞ ≤ Normal v8 ⇔ F)
[extreal_le_eq] Theorem
⊢ ∀x y. Normal x ≤ Normal y ⇔ x ≤ y
[extreal_le_ind] Theorem
⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P −∞ v0) ∧ P +∞ +∞ ∧
(∀v5. P (Normal v5) +∞) ∧ P +∞ −∞ ∧ (∀v6. P (Normal v6) −∞) ∧
(∀v8. P +∞ (Normal v8)) ⇒
∀v v1. P v v1
[extreal_lt_eq] Theorem
⊢ ∀x y. Normal x < Normal y ⇔ x < y
[extreal_mean] Theorem
⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
[extreal_mul_def] Theorem
⊢ −∞ * −∞ = +∞ ∧ −∞ * +∞ = −∞ ∧ +∞ * −∞ = −∞ ∧ +∞ * +∞ = +∞ ∧
Normal x * −∞ =
(if x = 0 then Normal 0 else if 0 < x then −∞ else +∞) ∧
−∞ * Normal y =
(if y = 0 then Normal 0 else if 0 < y then −∞ else +∞) ∧
Normal x * +∞ =
(if x = 0 then Normal 0 else if 0 < x then +∞ else −∞) ∧
+∞ * Normal y =
(if y = 0 then Normal 0 else if 0 < y then +∞ else −∞) ∧
Normal x * Normal y = Normal (x * y)
[extreal_mul_ind] Theorem
⊢ ∀P. P −∞ −∞ ∧ P −∞ +∞ ∧ P +∞ −∞ ∧ P +∞ +∞ ∧ (∀x. P (Normal x) −∞) ∧
(∀y. P −∞ (Normal y)) ∧ (∀x. P (Normal x) +∞) ∧
(∀y. P +∞ (Normal y)) ∧ (∀x y. P (Normal x) (Normal y)) ⇒
∀v v1. P v v1
[extreal_nchotomy] Theorem
⊢ ∀ee. ee = −∞ ∨ ee = +∞ ∨ ∃r. ee = Normal r
[extreal_not_infty] Theorem
⊢ ∀x. Normal x ≠ −∞ ∧ Normal x ≠ +∞
[extreal_not_lt] Theorem
⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
[extreal_sub_add] Theorem
⊢ ∀x y. x ≠ −∞ ∧ y ≠ +∞ ∨ x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y = x + -y
[extreal_sub_def] Theorem
⊢ Normal x − Normal y = Normal (x − y) ∧ −∞ − Normal v0 = −∞ ∧
+∞ − Normal v0 = +∞ ∧ Normal v1 − −∞ = +∞ ∧ Normal v2 − +∞ = −∞ ∧
−∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞
[extreal_sub_eq] Theorem
⊢ ∀x y. Normal x − Normal y = Normal (x − y)
[extreal_sub_ind] Theorem
⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P −∞ (Normal v0)) ∧
(∀v0. P +∞ (Normal v0)) ∧ (∀v1. P (Normal v1) −∞) ∧
(∀v2. P (Normal v2) +∞) ∧ P −∞ +∞ ∧ P +∞ −∞ ∧ P −∞ −∞ ∧ P +∞ +∞ ⇒
∀v v1. P v v1
[fourth_cancel] Theorem
⊢ 4 * (1 / 4) = 1
[fourths_between] Theorem
⊢ ((0 < 1 / 4 ∧ 1 / 4 < 1) ∧ 0 < 3 / 4 ∧ 3 / 4 < 1) ∧
(0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1) ∧ 0 ≤ 3 / 4 ∧ 3 / 4 ≤ 1
[gen_powr] Theorem
⊢ ∀a n. 0 ≤ a ⇒ a pow n = a powr &n
[half_between] Theorem
⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
[half_cancel] Theorem
⊢ 2 * (1 / 2) = 1
[half_not_infty] Theorem
⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞
[harmonic_series_pow_2] Theorem
⊢ suminf (λn. (&SUC n)² ⁻¹) < +∞
[inf_cminus] Theorem
⊢ ∀f c.
Normal c − inf (IMAGE f 𝕌(:α)) =
sup (IMAGE (λn. Normal c − f n) 𝕌(:α))
[inf_const] Theorem
⊢ ∀x. inf (λy. y = x) = x
[inf_const_alt] Theorem
⊢ ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ x = z) ⇒ inf p = z
[inf_const_over_set] Theorem
⊢ ∀s k. s ≠ ∅ ⇒ inf (IMAGE (λx. k) s) = k
[inf_empty] Theorem
⊢ inf ∅ = +∞
[inf_eq] Theorem
⊢ ∀p x. inf p = x ⇔ (∀y. p y ⇒ x ≤ y) ∧ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
[inf_eq'] Theorem
⊢ ∀p x.
inf p = x ⇔ (∀y. y ∈ p ⇒ x ≤ y) ∧ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x
[inf_le] Theorem
⊢ ∀p x. inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
[inf_le'] Theorem
⊢ ∀p x. inf p ≤ x ⇔ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x
[inf_le_imp] Theorem
⊢ ∀p x. p x ⇒ inf p ≤ x
[inf_le_imp'] Theorem
⊢ ∀p x. x ∈ p ⇒ inf p ≤ x
[inf_lt] Theorem
⊢ ∀P y. (∃x. P x ∧ x < y) ⇔ inf P < y
[inf_lt'] Theorem
⊢ ∀P y. (∃x. x ∈ P ∧ x < y) ⇔ inf P < y
[inf_lt_infty] Theorem
⊢ ∀p. −∞ < inf p ⇒ ∀x. p x ⇒ −∞ < x
[inf_min] Theorem
⊢ ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ inf p = z
[inf_minimal] Theorem
⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ inf p ∈ p
[inf_mono_subset] Theorem
⊢ ∀p q. p ⊆ q ⇒ inf q ≤ inf p
[inf_seq] Theorem
⊢ ∀f l.
mono_decreasing f ⇒
(f ⟶ l ⇔ inf (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
[inf_sing] Theorem
⊢ ∀a. inf {a} = a
[inf_suc] Theorem
⊢ ∀f. (∀m n. m ≤ n ⇒ f n ≤ f m) ⇒
inf (IMAGE (λn. f (SUC n)) 𝕌(:num)) = inf (IMAGE f 𝕌(:num))
[inf_univ] Theorem
⊢ inf 𝕌(:extreal) = −∞
[infty_div] Theorem
⊢ ∀r. 0 < r ⇒ +∞ / Normal r = +∞ ∧ −∞ / Normal r = −∞
[inv_1over] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ = 1 / x
[inv_inj] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)
[inv_le_antimono] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)
[inv_lt_antimono] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)
[inv_mul] Theorem
⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x * y)⁻¹ = x⁻¹ * y⁻¹
[inv_not_infty] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ≠ +∞ ∧ x⁻¹ ≠ −∞
[inv_one] Theorem
⊢ 1⁻¹ = 1
[inv_pos] Theorem
⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < 1 / x
[inv_pos'] Theorem
⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < x⁻¹
[inv_pos_eq] Theorem
⊢ ∀x. x ≠ 0 ⇒ (0 < x⁻¹ ⇔ x ≠ +∞ ∧ 0 ≤ x)
[ldiv_eq] Theorem
⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x / z = y ⇔ x = y * z)
[ldiv_le_imp] Theorem
⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ∧ x ≤ y ⇒ x / z ≤ y / z
[le_01] Theorem
⊢ 0 ≤ 1
[le_02] Theorem
⊢ 0 ≤ 2
[le_abs] Theorem
⊢ ∀x. x ≤ abs x ∧ -x ≤ abs x
[le_abs_bounds] Theorem
⊢ ∀k x. k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x
[le_add] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
[le_add2] Theorem
⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
[le_add_neg] Theorem
⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ x + y ≤ 0
[le_addl_imp] Theorem
⊢ ∀x y. 0 ≤ x ⇒ y ≤ x + y
[le_addr] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ x + y ⇔ 0 ≤ y)
[le_addr_imp] Theorem
⊢ ∀x y. 0 ≤ y ⇒ x ≤ x + y
[le_antisym] Theorem
⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
[le_div] Theorem
⊢ ∀y z. 0 ≤ y ∧ 0 < z ⇒ 0 ≤ y / Normal z
[le_epsilon] Theorem
⊢ ∀x y. (∀e. 0 < e ∧ e ≠ +∞ ⇒ x ≤ y + e) ⇒ x ≤ y
[le_inf] Theorem
⊢ ∀p x. x ≤ inf p ⇔ ∀y. p y ⇒ x ≤ y
[le_inf'] Theorem
⊢ ∀p x. x ≤ inf p ⇔ ∀y. y ∈ p ⇒ x ≤ y
[le_inf_epsilon_set] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒
∃x. x ∈ P ∧ x ≤ inf P + e
[le_infty] Theorem
⊢ (∀x. −∞ ≤ x ∧ x ≤ +∞) ∧ (∀x. x ≤ −∞ ⇔ x = −∞) ∧ ∀x. +∞ ≤ x ⇔ x = +∞
[le_inv] Theorem
⊢ ∀x. 0 < x ⇒ 0 ≤ x⁻¹
[le_ladd] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y ≤ x + z ⇔ y ≤ z)
[le_ladd_imp] Theorem
⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
[le_ldiv] Theorem
⊢ ∀x y z. 0 < x ⇒ (y ≤ z * Normal x ⇔ y / Normal x ≤ z)
[le_lmul_imp] Theorem
⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ z * x ≤ z * y
[le_lneg] Theorem
⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ (-x ≤ y ⇔ 0 ≤ x + y)
[le_lsub_imp] Theorem
⊢ ∀x y z. y ≤ z ⇒ x − z ≤ x − y
[le_lt] Theorem
⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y
[le_max] Theorem
⊢ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
[le_max1] Theorem
⊢ ∀x y. x ≤ max x y
[le_max2] Theorem
⊢ ∀x y. y ≤ max x y
[le_min] Theorem
⊢ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
[le_mul] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[le_mul_epsilon] Theorem
⊢ ∀x y. (∀z. 0 ≤ z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
[le_mul_neg] Theorem
⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y
[le_neg] Theorem
⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
[le_not_infty] Theorem
⊢ ∀x. (0 ≤ x ⇒ x ≠ −∞) ∧ (x ≤ 0 ⇒ x ≠ +∞)
[le_num] Theorem
⊢ ∀n. 0 ≤ &n
[le_pow2] Theorem
⊢ ∀x. 0 ≤ x²
[le_radd] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x ≤ z + x ⇔ y ≤ z)
[le_radd_imp] Theorem
⊢ ∀x y z. y ≤ z ⇒ y + x ≤ z + x
[le_rdiv] Theorem
⊢ ∀x y z. 0 < x ⇒ (y * Normal x ≤ z ⇔ y ≤ z / Normal x)
[le_refl] Theorem
⊢ ∀x. x ≤ x
[le_rmul_imp] Theorem
⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ x * z ≤ y * z
[le_rsub_imp] Theorem
⊢ ∀x y z. x ≤ y ⇒ x − z ≤ y − z
[le_sub_eq] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)
[le_sub_eq2] Theorem
⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ −∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)
[le_sub_imp] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x
[le_sub_imp2] Theorem
⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x
[le_sup] Theorem
⊢ ∀p x. x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
[le_sup'] Theorem
⊢ ∀p x. x ≤ sup p ⇔ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y
[le_sup_imp] Theorem
⊢ ∀p x. p x ⇒ x ≤ sup p
[le_sup_imp'] Theorem
⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
[le_sup_imp2] Theorem
⊢ ∀p z. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ z ≤ x) ⇒ z ≤ sup p
[le_total] Theorem
⊢ ∀x y. x ≤ y ∨ y ≤ x
[le_trans] Theorem
⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
[let_add] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
[let_add2] Theorem
⊢ ∀w x y z. w ≠ −∞ ∧ w ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
[let_add2_alt] Theorem
⊢ ∀w x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
[let_antisym] Theorem
⊢ ∀x y. ¬(x < y ∧ y ≤ x)
[let_mul] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
[let_total] Theorem
⊢ ∀x y. x ≤ y ∨ y < x
[let_trans] Theorem
⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
[linv_uniq] Theorem
⊢ ∀x y. x * y = 1 ⇒ x = y⁻¹
[logr_not_infty] Theorem
⊢ ∀x b. x ≠ −∞ ∧ x ≠ +∞ ⇒ logr b x ≠ −∞ ∧ logr b x ≠ +∞
[lt_01] Theorem
⊢ 0 < 1
[lt_02] Theorem
⊢ 0 < 2
[lt_10] Theorem
⊢ -1 < 0
[lt_abs_bounds] Theorem
⊢ ∀k x. k < abs x ⇔ x < -k ∨ k < x
[lt_add] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
[lt_add2] Theorem
⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
[lt_add_neg] Theorem
⊢ ∀x y. x < 0 ∧ y < 0 ⇒ x + y < 0
[lt_addl] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y < x + y ⇔ 0 < x)
[lt_addr_imp] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y ⇒ x < x + y
[lt_antisym] Theorem
⊢ ∀x y. ¬(x < y ∧ y < x)
[lt_div] Theorem
⊢ ∀y z. 0 < y ∧ 0 < z ⇒ 0 < y / Normal z
[lt_imp_le] Theorem
⊢ ∀x y. x < y ⇒ x ≤ y
[lt_imp_ne] Theorem
⊢ ∀x y. x < y ⇒ x ≠ y
[lt_inf_epsilon] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. P x ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. P x ∧ x < inf P + e
[lt_inf_epsilon_set] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒
∃x. x ∈ P ∧ x < inf P + e
[lt_infty] Theorem
⊢ ∀x y.
−∞ < Normal y ∧ Normal y < +∞ ∧ −∞ < +∞ ∧ ¬(x < −∞) ∧ ¬(+∞ < x) ∧
(x ≠ +∞ ⇔ x < +∞) ∧ (x ≠ −∞ ⇔ −∞ < x)
[lt_ladd] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y < x + z ⇔ y < z)
[lt_ldiv] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / Normal z < y ⇔ x < y * Normal z)
[lt_le] Theorem
⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
[lt_lmul] Theorem
⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y < x * z ⇔ y < z)
[lt_max_between] Theorem
⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
[lt_mul] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
[lt_mul2] Theorem
⊢ ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≠ +∞ ∧ y1 ≠ +∞ ∧ x1 < x2 ∧ y1 < y2 ⇒
x1 * y1 < x2 * y2
[lt_mul_neg] Theorem
⊢ ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y
[lt_neg] Theorem
⊢ ∀x y. -x < -y ⇔ y < x
[lt_radd] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x < z + x ⇔ y < z)
[lt_rdiv] Theorem
⊢ ∀x y z. 0 < z ⇒ (x < y / Normal z ⇔ x * Normal z < y)
[lt_rdiv_neg] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / Normal z < x ⇔ x * Normal z < y)
[lt_refl] Theorem
⊢ ∀x. ¬(x < x)
[lt_rmul] Theorem
⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z < y * z ⇔ x < y)
[lt_sub] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)
[lt_sub'] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)
[lt_sub_imp] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ y + x < z ⇒ y < z − x
[lt_sub_imp'] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ y + x < z ⇒ y < z − x
[lt_sub_imp2] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x < z ⇒ y < z − x
[lt_sup] Theorem
⊢ ∀a s. a < sup s ⇔ ∃x. x ∈ s ∧ a < x
[lt_total] Theorem
⊢ ∀x y. x = y ∨ x < y ∨ y < x
[lt_trans] Theorem
⊢ ∀x y z. x < y ∧ y < z ⇒ x < z
[lte_add] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
[lte_mul] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[lte_total] Theorem
⊢ ∀x y. x < y ∨ y ≤ x
[lte_trans] Theorem
⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
[max_comm] Theorem
⊢ ∀x y. max x y = max y x
[max_fn_seq_compute] Theorem
⊢ (∀g x. max_fn_seq g 0 x = g 0 x) ∧
(∀g n x.
max_fn_seq g (NUMERAL (BIT1 n)) x =
max (max_fn_seq g (NUMERAL (BIT1 n) − 1) x)
(g (NUMERAL (BIT1 n)) x)) ∧
∀g n x.
max_fn_seq g (NUMERAL (BIT2 n)) x =
max (max_fn_seq g (NUMERAL (BIT1 n)) x) (g (NUMERAL (BIT2 n)) x)
[max_fn_seq_mono] Theorem
⊢ ∀g n x. max_fn_seq g n x ≤ max_fn_seq g (SUC n) x
[max_infty] Theorem
⊢ ∀x. max x +∞ = +∞ ∧ max +∞ x = +∞ ∧ max −∞ x = x ∧ max x −∞ = x
[max_le] Theorem
⊢ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
[max_le2_imp] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
[max_reduce] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y
[max_refl] Theorem
⊢ ∀x. max x x = x
[min_comm] Theorem
⊢ ∀x y. min x y = min y x
[min_infty] Theorem
⊢ ∀x. min x +∞ = x ∧ min +∞ x = x ∧ min −∞ x = −∞ ∧ min x −∞ = −∞
[min_le] Theorem
⊢ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
[min_le1] Theorem
⊢ ∀x y. min x y ≤ x
[min_le2] Theorem
⊢ ∀x y. min x y ≤ y
[min_le2_imp] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
[min_le_between] Theorem
⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x
[min_reduce] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x
[min_refl] Theorem
⊢ ∀x. min x x = x
[mul_assoc] Theorem
⊢ ∀x y z. x * (y * z) = x * y * z
[mul_comm] Theorem
⊢ ∀x y. x * y = y * x
[mul_div_refl] Theorem
⊢ ∀x r. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < r ⇒ x = x * Normal r / Normal r
[mul_infty] Theorem
⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞
[mul_lcancel] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (x * y = x * z ⇔ x = 0 ∨ y = z)
[mul_le] Theorem
⊢ ∀x y. 0 ≤ x ∧ y ≤ 0 ⇒ x * y ≤ 0
[mul_le2] Theorem
⊢ ∀x y. x ≤ 0 ∧ 0 ≤ y ⇒ x * y ≤ 0
[mul_let] Theorem
⊢ ∀x y. 0 ≤ x ∧ y < 0 ⇒ x * y ≤ 0
[mul_linv] Theorem
⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ * x = 1
[mul_linv_pos] Theorem
⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x⁻¹ * x = 1
[mul_lneg] Theorem
⊢ ∀x y. -x * y = -(x * y)
[mul_lone] Theorem
⊢ ∀x. 1 * x = x
[mul_lposinf] Theorem
⊢ ∀x. 0 < x ⇒ +∞ * x = +∞
[mul_lt] Theorem
⊢ ∀x y. 0 < x ∧ y < 0 ⇒ x * y < 0
[mul_lt2] Theorem
⊢ ∀x y. x < 0 ∧ 0 < y ⇒ x * y < 0
[mul_lte] Theorem
⊢ ∀x y. 0 < x ∧ y ≤ 0 ⇒ x * y ≤ 0
[mul_lzero] Theorem
⊢ ∀x. 0 * x = 0
[mul_not_infty] Theorem
⊢ (∀c y. 0 ≤ c ∧ y ≠ −∞ ⇒ Normal c * y ≠ −∞) ∧
(∀c y. 0 ≤ c ∧ y ≠ +∞ ⇒ Normal c * y ≠ +∞) ∧
(∀c y. c ≤ 0 ∧ y ≠ −∞ ⇒ Normal c * y ≠ +∞) ∧
∀c y. c ≤ 0 ∧ y ≠ +∞ ⇒ Normal c * y ≠ −∞
[mul_not_infty2] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ x * y ≠ −∞ ∧ x * y ≠ +∞
[mul_rneg] Theorem
⊢ ∀x y. x * -y = -(x * y)
[mul_rone] Theorem
⊢ ∀x. x * 1 = x
[mul_rposinf] Theorem
⊢ ∀x. 0 < x ⇒ x * +∞ = +∞
[mul_rzero] Theorem
⊢ ∀x. x * 0 = 0
[ne_01] Theorem
⊢ 0 ≠ 1
[ne_02] Theorem
⊢ 0 ≠ 2
[neg_0] Theorem
⊢ -0 = 0
[neg_add] Theorem
⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -(x + y) = -x + -y
[neg_eq0] Theorem
⊢ ∀x. -x = 0 ⇔ x = 0
[neg_minus1] Theorem
⊢ ∀x. -x = -1 * x
[neg_mul2] Theorem
⊢ ∀x y. -x * -y = x * y
[neg_neg] Theorem
⊢ ∀x. --x = x
[neg_not_posinf] Theorem
⊢ ∀x. x ≤ 0 ⇒ x ≠ +∞
[neg_sub] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∨ y ≠ −∞ ∧ y ≠ +∞ ⇒ -(x − y) = y − x
[normal_exp] Theorem
⊢ ∀r. exp (Normal r) = Normal (exp r)
[normal_inv_eq] Theorem
⊢ ∀x. x ≠ 0 ⇒ Normal x⁻¹ = (Normal x)⁻¹
[normal_powr] Theorem
⊢ ∀r a. 0 < r ∧ 0 < a ⇒ Normal r powr Normal a = Normal (r powr a)
[normal_real] Theorem
⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ Normal (real x) = x
[normal_real_set] Theorem
⊢ ∀s. s ∩ IMAGE Normal 𝕌(:real) = IMAGE Normal (real_set s)
[num_lt_infty] Theorem
⊢ ∀n. &n < +∞
[num_not_infty] Theorem
⊢ ∀n. &n ≠ −∞ ∧ &n ≠ +∞
[one_pow] Theorem
⊢ ∀n. 1 pow n = 1
[pos_not_neginf] Theorem
⊢ ∀x. 0 ≤ x ⇒ x ≠ −∞
[pos_summable] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃r. ∀n. ∑ f (count n) ≤ Normal r) ⇒
suminf f < +∞
[pow2_le_eq] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x² ≤ y²)
[pow2_sqrt] Theorem
⊢ ∀x. 0 ≤ x ⇒ sqrt x² = x
[pow_0] Theorem
⊢ ∀x. x pow 0 = 1
[pow_1] Theorem
⊢ ∀x. x pow 1 = x
[pow_2] Theorem
⊢ ∀x. x² = x * x
[pow_add] Theorem
⊢ ∀x n m. x pow (n + m) = x pow n * x pow m
[pow_div] Theorem
⊢ ∀n x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ (x / y) pow n = x pow n / y pow n
[pow_half_pos_le] Theorem
⊢ ∀n. 0 ≤ (1 / 2) pow (n + 1)
[pow_half_pos_lt] Theorem
⊢ ∀n. 0 < (1 / 2) pow (n + 1)
[pow_half_ser] Theorem
⊢ suminf (λn. (1 / 2) pow (n + 1)) = 1
[pow_half_ser'] Theorem
⊢ suminf (λn. (1 / 2) pow SUC n) = 1
[pow_half_ser_by_e] Theorem
⊢ ∀e. 0 < e ∧ e ≠ +∞ ⇒ e = suminf (λn. e * (1 / 2) pow (n + 1))
[pow_inv] Theorem
⊢ ∀n y. y ≠ 0 ⇒ (y pow n)⁻¹ = y⁻¹ pow n
[pow_le] Theorem
⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n
[pow_le_full] Theorem
⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x pow n ≤ y pow n)
[pow_le_mono] Theorem
⊢ ∀x n m. 1 ≤ x ∧ n ≤ m ⇒ x pow n ≤ x pow m
[pow_lt] Theorem
⊢ ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n
[pow_lt2] Theorem
⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n
[pow_minus1] Theorem
⊢ ∀n. -1 pow (2 * n) = 1
[pow_mul] Theorem
⊢ ∀n x y. (x * y) pow n = x pow n * y pow n
[pow_neg_odd] Theorem
⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
[pow_not_infty] Theorem
⊢ ∀n x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x pow n ≠ −∞ ∧ x pow n ≠ +∞
[pow_pos_even] Theorem
⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
[pow_pos_le] Theorem
⊢ ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n
[pow_pos_lt] Theorem
⊢ ∀x n. 0 < x ⇒ 0 < x pow n
[pow_zero] Theorem
⊢ ∀n x. x pow SUC n = 0 ⇔ x = 0
[pow_zero_imp] Theorem
⊢ ∀n x. x pow n = 0 ⇒ x = 0
[powr_0] Theorem
⊢ ∀x. x powr 0 = 1
[powr_pos] Theorem
⊢ ∀x a. 0 ≤ x powr a
[quotient_normal] Theorem
⊢ ∀n m. m ≠ 0 ⇒ &n / &m = Normal (&n / &m)
[rat_not_infty] Theorem
⊢ ∀r. r ∈ ℚ ⇒ r ≠ −∞ ∧ r ≠ +∞
[rdiv_eq] Theorem
⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x = y / z ⇔ x * z = y)
[real_normal] Theorem
⊢ ∀x. real (Normal x) = x
[rinv_uniq] Theorem
⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹
[seq_sup_compute] Theorem
⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
(∀P n.
seq_sup P (NUMERAL (BIT1 n)) =
@r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT1 n)) ∧
seq_sup P (NUMERAL (BIT1 n) − 1) < r ∧ r < sup P) ∧
∀P n.
seq_sup P (NUMERAL (BIT2 n)) =
@r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT2 n)) ∧
seq_sup P (NUMERAL (BIT1 n)) < r ∧ r < sup P
[sqrt_mono_le] Theorem
⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
[sqrt_pos_le] Theorem
⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x
[sqrt_pos_lt] Theorem
⊢ ∀x. 0 < x ⇒ 0 < sqrt x
[sqrt_pow2] Theorem
⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x
[sub_0] Theorem
⊢ ∀x y. x − y = 0 ⇒ x = y
[sub_add] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x − y + y = x
[sub_add2] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ x + (y − x) = y
[sub_eq_0] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ x = y ⇒ x − y = 0
[sub_infty] Theorem
⊢ (∀x. x ≠ −∞ ⇒ x − −∞ = +∞) ∧ (∀x. x ≠ +∞ ⇒ x − +∞ = −∞) ∧
(∀x. x ≠ +∞ ⇒ +∞ − x = +∞) ∧ ∀x. x ≠ −∞ ⇒ −∞ − x = −∞
[sub_ldistrib] Theorem
⊢ ∀x y z.
x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
x * (y − z) = x * y − x * z
[sub_le_eq] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)
[sub_le_eq2] Theorem
⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ x ≠ −∞ ∧ z ≠ −∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)
[sub_le_imp] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z
[sub_le_imp2] Theorem
⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z
[sub_le_switch] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)
[sub_le_switch2] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)
[sub_le_zero] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x ≤ y ⇔ x − y ≤ 0)
[sub_lneg] Theorem
⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -x − y = -(x + y)
[sub_lt_eq] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x < z ⇔ y < z + x)
[sub_lt_imp] Theorem
⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y < z + x ⇒ y − x < z
[sub_lt_imp2] Theorem
⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y < z + x ⇒ y − x < z
[sub_lt_zero] Theorem
⊢ ∀x y. x < y ⇒ x − y < 0
[sub_lt_zero2] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ∧ x − y < 0 ⇒ x < y
[sub_lzero] Theorem
⊢ ∀x. 0 − x = -x
[sub_not_infty] Theorem
⊢ ∀x y.
(x ≠ −∞ ∧ y ≠ +∞ ⇒ x − y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y ≠ +∞)
[sub_pow2] Theorem
⊢ ∀x y.
x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒
(x − y)² = x² + y² − 2 * x * y
[sub_rdistrib] Theorem
⊢ ∀x y z.
x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
(x − y) * z = x * z − y * z
[sub_refl] Theorem
⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x − x = 0
[sub_rneg] Theorem
⊢ ∀c x. Normal c − -x = Normal c + x
[sub_rzero] Theorem
⊢ ∀x. x − 0 = x
[sub_zero_le] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ y ⇔ 0 ≤ y − x)
[sub_zero_lt] Theorem
⊢ ∀x y. x < y ⇒ 0 < y − x
[sub_zero_lt2] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y − x ⇒ x < y
[summable_ext_suminf] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ suminf (Normal ∘ f) < +∞
[summable_ext_suminf_suminf] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒
suminf (Normal ∘ f) = Normal (suminf f)
[sup_add_mono] Theorem
⊢ ∀f g.
(∀n. 0 ≤ f n) ∧ (∀n. f n ≤ f (SUC n)) ∧ (∀n. 0 ≤ g n) ∧
(∀n. g n ≤ g (SUC n)) ⇒
sup (IMAGE (λn. f n + g n) 𝕌(:num)) =
sup (IMAGE f 𝕌(:num)) + sup (IMAGE g 𝕌(:num))
[sup_close] Theorem
⊢ ∀e s. 0 < e ∧ abs (sup s) ≠ +∞ ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ sup s − e < x
[sup_cmul] Theorem
⊢ ∀f c.
0 ≤ c ⇒
sup (IMAGE (λn. Normal c * f n) 𝕌(:α)) =
Normal c * sup (IMAGE f 𝕌(:α))
[sup_cmult] Theorem
⊢ ∀f c.
0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒
sup (IMAGE (λn. c * f n) 𝕌(:α)) = c * sup (IMAGE f 𝕌(:α))
[sup_comm] Theorem
⊢ ∀f. sup {sup {f i j | j ∈ 𝕌(:num)} | i ∈ 𝕌(:num)} =
sup {sup {f i j | i ∈ 𝕌(:num)} | j ∈ 𝕌(:num)}
[sup_const] Theorem
⊢ ∀x. sup (λy. y = x) = x
[sup_const_alt] Theorem
⊢ ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ x = z) ⇒ sup p = z
[sup_const_alt'] Theorem
⊢ ∀p z. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ x = z) ⇒ sup p = z
[sup_const_over_set] Theorem
⊢ ∀s k. s ≠ ∅ ⇒ sup (IMAGE (λx. k) s) = k
[sup_const_over_univ] Theorem
⊢ ∀k. sup (IMAGE (λx. k) 𝕌(:α)) = k
[sup_countable_seq] Theorem
⊢ ∀A. A ≠ ∅ ⇒
∃f. IMAGE f 𝕌(:num) ⊆ A ∧ sup A = sup {f n | n ∈ 𝕌(:num)}
[sup_empty] Theorem
⊢ sup ∅ = −∞
[sup_eq] Theorem
⊢ ∀p x. sup p = x ⇔ (∀y. p y ⇒ y ≤ x) ∧ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
[sup_eq'] Theorem
⊢ ∀p x.
sup p = x ⇔ (∀y. y ∈ p ⇒ y ≤ x) ∧ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y
[sup_le] Theorem
⊢ ∀p x. sup p ≤ x ⇔ ∀y. p y ⇒ y ≤ x
[sup_le'] Theorem
⊢ ∀p x. sup p ≤ x ⇔ ∀y. y ∈ p ⇒ y ≤ x
[sup_le_mono] Theorem
⊢ ∀f z.
(∀n. f n ≤ f (SUC n)) ∧ z < sup (IMAGE f 𝕌(:num)) ⇒ ∃n. z ≤ f n
[sup_le_sup_imp] Theorem
⊢ ∀p q. (∀x. p x ⇒ ∃y. q y ∧ x ≤ y) ⇒ sup p ≤ sup q
[sup_le_sup_imp'] Theorem
⊢ ∀p q. (∀x. x ∈ p ⇒ ∃y. y ∈ q ∧ x ≤ y) ⇒ sup p ≤ sup q
[sup_lt] Theorem
⊢ ∀P y. (∃x. P x ∧ y < x) ⇔ y < sup P
[sup_lt'] Theorem
⊢ ∀P y. (∃x. x ∈ P ∧ y < x) ⇔ y < sup P
[sup_lt_epsilon] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. P x ∧ x ≠ −∞) ∧ sup P ≠ +∞ ⇒ ∃x. P x ∧ sup P < x + e
[sup_lt_infty] Theorem
⊢ ∀p. sup p < +∞ ⇒ ∀x. p x ⇒ x < +∞
[sup_max] Theorem
⊢ ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ sup p = z
[sup_maximal] Theorem
⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ sup p ∈ p
[sup_mono] Theorem
⊢ ∀p q.
(∀n. p n ≤ q n) ⇒ sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))
[sup_mono_ext] Theorem
⊢ ∀f g A B.
(∀n. n ∈ A ⇒ ∃m. m ∈ B ∧ f n ≤ g m) ⇒
sup {f n | n ∈ A} ≤ sup {g n | n ∈ B}
[sup_mono_subset] Theorem
⊢ ∀p q. p ⊆ q ⇒ sup p ≤ sup q
[sup_num] Theorem
⊢ sup (λx. ∃n. x = &n) = +∞
[sup_seq] Theorem
⊢ ∀f l.
mono_increasing f ⇒
(f ⟶ l ⇔ sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
[sup_seq_countable_seq] Theorem
⊢ ∀A g.
A ≠ ∅ ⇒
∃f. IMAGE f 𝕌(:num) ⊆ IMAGE g A ∧
sup {g n | n ∈ A} = sup {f n | n ∈ 𝕌(:num)}
[sup_shift] Theorem
⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
∀N. sup (IMAGE (λn. f (n + N)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))
[sup_sing] Theorem
⊢ ∀a. sup {a} = a
[sup_suc] Theorem
⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
sup (IMAGE (λn. f (SUC n)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))
[sup_sum_mono] Theorem
⊢ ∀f s.
FINITE s ∧ (∀i. i ∈ s ⇒ ∀n. 0 ≤ f i n) ∧
(∀i. i ∈ s ⇒ ∀n. f i n ≤ f i (SUC n)) ⇒
sup (IMAGE (λn. ∑ (λi. f i n) s) 𝕌(:num)) =
∑ (λi. sup (IMAGE (f i) 𝕌(:num))) s
[sup_univ] Theorem
⊢ sup 𝕌(:extreal) = +∞
[third_cancel] Theorem
⊢ 3 * (1 / 3) = 1
[thirds_between] Theorem
⊢ ((0 < 1 / 3 ∧ 1 / 3 < 1) ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧
(0 ≤ 1 / 3 ∧ 1 / 3 ≤ 1) ∧ 0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1
[zero_div] Theorem
⊢ ∀x. x ≠ 0 ⇒ 0 / x = 0
[zero_pow] Theorem
⊢ ∀n. 0 < n ⇒ 0 pow n = 0
[zero_rpow] Theorem
⊢ ∀x. 0 < x ⇒ 0 powr x = 0
*)
end
HOL 4, Kananaskis-14