Structure extreal_baseTheory
signature extreal_baseTheory =
sig
type thm = Thm.thm
(* Definitions *)
val extreal_TY_DEF : thm
val extreal_abs_def_primitive : thm
val extreal_ainv_def : thm
val extreal_case_def : thm
val extreal_div_def : thm
val extreal_inv_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_size_def : thm
val extreal_sqrt_def : thm
val extreal_sub : thm
val real_def : thm
(* Theorems *)
val EXTREAL_ARCH : thm
val EXTREAL_ARCH_INV : thm
val EXTREAL_ARCH_INV' : thm
val EXTREAL_EQ_LADD : thm
val EXTREAL_EQ_RADD : thm
val SIMP_EXTREAL_ARCH : thm
val SIMP_EXTREAL_ARCH_NEG : thm
val abs_0 : thm
val abs_abs : thm
val abs_bounds : thm
val abs_bounds_lt : thm
val abs_div : thm
val abs_div_normal : 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_neg' : thm
val abs_neg_eq : thm
val abs_not_infty : thm
val abs_not_zero : thm
val abs_pos : thm
val abs_pow2 : thm
val abs_pow_le_mono : thm
val abs_real : thm
val abs_refl : thm
val abs_sub : thm
val abs_sub' : thm
val abs_triangle : thm
val abs_triangle_full : thm
val abs_triangle_neg : thm
val abs_triangle_neg_full : thm
val abs_triangle_sub : thm
val abs_triangle_sub' : thm
val abs_triangle_sub_full : thm
val abs_triangle_sub_full' : 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 add_sub_normal : thm
val datatype_extreal : thm
val div_add : thm
val div_add2 : thm
val div_eq_mul_linv : thm
val div_eq_mul_rinv : 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 div_sub : 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 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_double : 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_eq : thm
val extreal_mul_ind : thm
val extreal_nchotomy : thm
val extreal_not_infty : thm
val extreal_not_lt : thm
val extreal_pow : thm
val extreal_sub_add : thm
val extreal_sub_def : thm
val extreal_sub_eq : thm
val fourth_cancel : thm
val fourths_between : thm
val half_between : thm
val half_cancel : thm
val half_double : thm
val half_not_infty : thm
val infty_div : thm
val infty_pow2 : thm
val inv_1over : thm
val inv_infty : thm
val inv_inj : thm
val inv_inv : thm
val inv_le_antimono : thm
val inv_le_antimono_imp : 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 : 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_infty : thm
val le_inv : thm
val le_ladd : thm
val le_ladd_imp : thm
val le_ldiv : thm
val le_lmul : 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_mul2 : 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 : 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_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 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 : 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_infty : thm
val lt_ladd : thm
val lt_ldiv : thm
val lt_le : thm
val lt_lmul : thm
val lt_lmul_imp : thm
val lt_lsub_imp : thm
val lt_max : 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_rmul_imp : thm
val lt_rsub_imp : 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_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_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_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_rcancel : 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_inv_eq : thm
val normal_real : thm
val num_lt_infty : thm
val num_not_infty : thm
val one_pow : thm
val pos_not_neginf : thm
val pow2_le_eq : thm
val pow2_sqrt : thm
val pow_0 : thm
val pow_1 : thm
val pow_2 : thm
val pow_2_abs : thm
val pow_add : thm
val pow_div : thm
val pow_eq : 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_pow : thm
val pow_zero : thm
val pow_zero_imp : thm
val quotient_normal : thm
val rdiv_eq : thm
val real_0 : thm
val real_normal : thm
val rinv_uniq : thm
val sqrt_0 : thm
val sqrt_1 : thm
val sqrt_le_n : thm
val sqrt_le_x : thm
val sqrt_mono_le : thm
val sqrt_mul : thm
val sqrt_pos_le : thm
val sqrt_pos_lt : thm
val sqrt_pos_ne : thm
val sqrt_pow2 : thm
val sub_0 : thm
val sub_add : thm
val sub_add2 : thm
val sub_add_normal : 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 third_cancel : thm
val thirds_between : thm
val x_half_half : thm
val zero_div : thm
val zero_pow : thm
val extreal_base_grammars : type_grammar.grammar * term_grammar.grammar
(*
[iterate] Parent theory of "extreal_base"
[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_def_primitive] 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_inv_def] Definition
⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹
[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_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_sub] Definition
⊢ ∀x y. x − y = x + -y
[real_def] Definition
⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r
[EXTREAL_ARCH] Theorem
⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x
[EXTREAL_ARCH_INV] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x
[EXTREAL_ARCH_INV'] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ ≤ x
[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)
[SIMP_EXTREAL_ARCH] Theorem
⊢ ∀x. x ≠ +∞ ⇒ ∃n. x ≤ &n
[SIMP_EXTREAL_ARCH_NEG] Theorem
⊢ ∀x. x ≠ −∞ ⇒ ∃n. -&n ≤ x
[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_div_normal] Theorem
⊢ ∀x y. y ≠ 0 ⇒ abs (x / Normal y) = abs x / Normal (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_neg'] Theorem
⊢ ∀x. x ≤ 0 ⇒ abs x = -x
[abs_neg_eq] Theorem
⊢ ∀x. abs (-x) = abs x
[abs_not_infty] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞
[abs_not_zero] Theorem
⊢ ∀x. abs x ≠ 0 ⇔ x ≠ 0
[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_real] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs (real x) = real (abs x)
[abs_refl] Theorem
⊢ ∀x. abs x = x ⇔ 0 ≤ x
[abs_sub] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) = abs (y − x)
[abs_sub'] Theorem
⊢ ∀x y. abs (x − y) = abs (y − x)
[abs_triangle] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y
[abs_triangle_full] Theorem
⊢ ∀x y. abs (x + y) ≤ abs x + abs y
[abs_triangle_neg] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) ≤ abs x + abs y
[abs_triangle_neg_full] Theorem
⊢ ∀x 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_triangle_sub'] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (y − x)
[abs_triangle_sub_full] Theorem
⊢ ∀x y. abs x ≤ abs y + abs (x − y)
[abs_triangle_sub_full'] Theorem
⊢ ∀x y. abs x ≤ abs y + abs (y − x)
[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 + 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
[add_sub_normal] Theorem
⊢ ∀x r. x + Normal r − Normal r = 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_eq_mul_rinv] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = x * y⁻¹
[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
[div_sub] Theorem
⊢ ∀x y z.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒
x / z − y / z = (x − y) / z
[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
[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_double] Theorem
⊢ ∀x. x + x = 2 * x
[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_eq] Theorem
⊢ ∀x y. 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_pow] Theorem
⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n
[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 x = +∞ ∧
−∞ − Normal x = −∞ ∧ Normal x − −∞ = +∞ ∧ Normal x − +∞ = −∞ ∧
−∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞
[extreal_sub_eq] Theorem
⊢ ∀x y. Normal x − Normal y = Normal (x − y)
[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
[half_between] Theorem
⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
[half_cancel] Theorem
⊢ 2 * (1 / 2) = 1
[half_double] Theorem
⊢ ∀x. x / 2 + x / 2 = x
[half_not_infty] Theorem
⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞
[infty_div] Theorem
⊢ ∀r. 0 < r ⇒ +∞ / Normal r = +∞ ∧ −∞ / Normal r = −∞
[infty_pow2] Theorem
⊢ +∞ ² = +∞ ∧ −∞ ² = +∞
[inv_1over] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ = 1 / x
[inv_infty] Theorem
⊢ +∞ ⁻¹ = 0 ∧ −∞ ⁻¹ = 0
[inv_inj] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)
[inv_inv] Theorem
⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ ⁻¹ = x
[inv_le_antimono] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)
[inv_le_antimono_imp] Theorem
⊢ ∀x y. 0 < y ∧ y ≤ x ⇒ x⁻¹ ≤ y⁻¹
[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] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y ≤ x + y ⇔ 0 ≤ x)
[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_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] Theorem
⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y ≤ x * z ⇔ y ≤ 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_mul2] Theorem
⊢ ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2
[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. 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] Theorem
⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z ≤ y * z ⇔ x ≤ y)
[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_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⁻¹
[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] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x < x + y ⇔ 0 < y)
[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_infty] Theorem
⊢ −∞ < +∞ ∧ (∀x. −∞ < Normal x ∧ Normal x < +∞) ∧
(∀x. ¬(x < −∞) ∧ ¬(+∞ < x)) ∧ (∀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_lmul_imp] Theorem
⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ∧ y < z ⇒ x * y < x * z
[lt_lsub_imp] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ∧ y < z ⇒ x − z < x − y
[lt_max] Theorem
⊢ ∀x y z. x < max y z ⇔ x < y ∨ x < 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_rmul_imp] Theorem
⊢ ∀x y z. x < y ∧ 0 < z ∧ z ≠ +∞ ⇒ x * z < y * z
[lt_rsub_imp] Theorem
⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ∧ x < y ⇒ x − z < y − z
[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_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_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. r ≠ 0 ⇒ x = x * Normal r / Normal r
[mul_infty] Theorem
⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞
[mul_infty'] Theorem
⊢ ∀x. x < 0 ⇒ +∞ * 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_rcancel] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (y * x = z * x ⇔ x = 0 ∨ y = z)
[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_inv_eq] Theorem
⊢ ∀x. x ≠ 0 ⇒ Normal x⁻¹ = (Normal x)⁻¹
[normal_real] Theorem
⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ Normal (real x) = x
[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 ≠ −∞
[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_2_abs] Theorem
⊢ ∀x. x² = abs x * abs 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_eq] Theorem
⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x = y ⇔ x pow n = y pow n)
[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
⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ x pow n
[pow_pos_lt] Theorem
⊢ ∀n x. 0 < x ⇒ 0 < x pow n
[pow_pow] Theorem
⊢ ∀x m n. (x pow m) pow n = x pow (m * 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
[quotient_normal] Theorem
⊢ ∀n m. m ≠ 0 ⇒ &n / &m = Normal (&n / &m)
[rdiv_eq] Theorem
⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x = y / z ⇔ x * z = y)
[real_0] Theorem
⊢ real 0 = 0
[real_normal] Theorem
⊢ ∀x. real (Normal x) = x
[rinv_uniq] Theorem
⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹
[sqrt_0] Theorem
⊢ sqrt 0 = 0
[sqrt_1] Theorem
⊢ sqrt 1 = 1
[sqrt_le_n] Theorem
⊢ ∀n. sqrt (&n) ≤ &n
[sqrt_le_x] Theorem
⊢ ∀x. 1 ≤ x ⇒ sqrt x ≤ x
[sqrt_mono_le] Theorem
⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
[sqrt_mul] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (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_pos_ne] Theorem
⊢ ∀x. 0 < x ⇒ sqrt x ≠ 0
[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_add_normal] Theorem
⊢ ∀x r. x − Normal r + Normal r = x
[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
⊢ ∀x y. x − -y = x + y
[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
[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
[x_half_half] Theorem
⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x
[zero_div] Theorem
⊢ ∀x. x ≠ 0 ⇒ 0 / x = 0
[zero_pow] Theorem
⊢ ∀n. 0 < n ⇒ 0 pow n = 0
*)
end
HOL 4, Trindemossen-1