Structure realTheory
signature realTheory =
sig
type thm = Thm.thm
(* Definitions *)
val NUM_CEILING_def : thm
val NUM_FLOOR_def : thm
val inf_def : thm
val nonzerop_def : thm
val pos_def : thm
val real_sgn : thm
val sqrt_def : thm
val sup : thm
(* Theorems *)
val ABS_0 : thm
val ABS_1 : thm
val ABS_ABS : thm
val ABS_BETWEEN : thm
val ABS_BETWEEN1 : thm
val ABS_BETWEEN2 : thm
val ABS_BOUND : thm
val ABS_BOUNDS : thm
val ABS_BOUNDS_LT : thm
val ABS_BOUNDS_MIN_MAX : thm
val ABS_CASES : thm
val ABS_CIRCLE : thm
val ABS_DIV : thm
val ABS_INV : thm
val ABS_LE : thm
val ABS_LT_MUL2 : thm
val ABS_MUL : thm
val ABS_N : thm
val ABS_NEG : thm
val ABS_NZ : thm
val ABS_NZ' : thm
val ABS_POS : thm
val ABS_POW2 : thm
val ABS_REFL : thm
val ABS_SIGN : thm
val ABS_SIGN2 : thm
val ABS_STILLNZ : thm
val ABS_SUB : thm
val ABS_SUB_ABS : thm
val ABS_SUM : thm
val ABS_TRIANGLE : thm
val ABS_TRIANGLE_LT : thm
val ABS_TRIANGLE_NEG : thm
val ABS_TRIANGLE_SUB : thm
val ABS_ZERO : thm
val ADD_POW_2 : thm
val CLG_UBOUND : thm
val HALF_CANCEL : thm
val HALF_LT_1 : thm
val HALF_POS : thm
val INFINITE_REAL_UNIV : thm
val LE_NUM_CEILING : thm
val NEGATED_POW : thm
val NUM_CEILING_LE : thm
val NUM_CEILING_NUM_FLOOR : thm
val NUM_CEILING_UPPER_BOUND : thm
val NUM_FLOOR_BASE : thm
val NUM_FLOOR_DIV : thm
val NUM_FLOOR_DIV_LOWERBOUND : thm
val NUM_FLOOR_EQNS : thm
val NUM_FLOOR_LE : thm
val NUM_FLOOR_LE2 : thm
val NUM_FLOOR_LET : thm
val NUM_FLOOR_LOWER_BOUND : thm
val NUM_FLOOR_LT : thm
val NUM_FLOOR_MONO : thm
val NUM_FLOOR_MUL_LOWERBOUND : thm
val NUM_FLOOR_lower_bound : thm
val NUM_FLOOR_upper_bound : thm
val ONE_MINUS_HALF : thm
val POW_0 : thm
val POW_0' : thm
val POW_1 : thm
val POW_2 : thm
val POW_2_LE1 : thm
val POW_2_LT : thm
val POW_2_SQRT : thm
val POW_ABS : thm
val POW_ADD : thm
val POW_EQ : thm
val POW_HALF_POS : thm
val POW_INV : thm
val POW_LE : thm
val POW_LT : thm
val POW_M1 : thm
val POW_MINUS1 : thm
val POW_MINUS1_ODD : thm
val POW_MUL : thm
val POW_NZ : thm
val POW_ONE : thm
val POW_PLUS1 : thm
val POW_POS : thm
val POW_POS_LT : thm
val POW_ZERO : thm
val POW_ZERO_EQ : thm
val RAT_LEMMA1 : thm
val RAT_LEMMA2 : thm
val RAT_LEMMA3 : thm
val RAT_LEMMA4 : thm
val RAT_LEMMA5 : thm
val RAT_LEMMA5_BETTER : thm
val REAL : thm
val REAL_0 : thm
val REAL_1 : thm
val REAL_10 : thm
val REAL_ABS_0 : thm
val REAL_ABS_DIV : thm
val REAL_ABS_LE0 : thm
val REAL_ABS_MUL : thm
val REAL_ABS_POS : thm
val REAL_ABS_SGN : thm
val REAL_ABS_TRIANGLE : thm
val REAL_ADD : thm
val REAL_ADD2_SUB2 : thm
val REAL_ADD_ASSOC : thm
val REAL_ADD_COMM : thm
val REAL_ADD_LDISTRIB : thm
val REAL_ADD_LID : thm
val REAL_ADD_LID_UNIQ : thm
val REAL_ADD_LINV : thm
val REAL_ADD_RAT : thm
val REAL_ADD_RDISTRIB : thm
val REAL_ADD_RID : thm
val REAL_ADD_RID_UNIQ : thm
val REAL_ADD_RINV : thm
val REAL_ADD_SUB : thm
val REAL_ADD_SUB2 : thm
val REAL_ADD_SUB_ALT : thm
val REAL_ADD_SYM : thm
val REAL_ARCH : thm
val REAL_ARCH_INV : thm
val REAL_ARCH_LEAST : thm
val REAL_ARCH_POW : thm
val REAL_ARCH_POW2 : thm
val REAL_ARCH_POW_INV : thm
val REAL_BIGNUM : thm
val REAL_DIFFSQ : thm
val REAL_DIV_ADD : thm
val REAL_DIV_DENOM_CANCEL : thm
val REAL_DIV_DENOM_CANCEL2 : thm
val REAL_DIV_DENOM_CANCEL3 : thm
val REAL_DIV_INNER_CANCEL : thm
val REAL_DIV_INNER_CANCEL2 : thm
val REAL_DIV_INNER_CANCEL3 : thm
val REAL_DIV_LMUL : thm
val REAL_DIV_LMUL_CANCEL : thm
val REAL_DIV_LT : thm
val REAL_DIV_LZERO : thm
val REAL_DIV_MUL2 : thm
val REAL_DIV_OUTER_CANCEL : thm
val REAL_DIV_OUTER_CANCEL2 : thm
val REAL_DIV_OUTER_CANCEL3 : thm
val REAL_DIV_PROD : thm
val REAL_DIV_REFL : thm
val REAL_DIV_REFL2 : thm
val REAL_DIV_REFL3 : thm
val REAL_DIV_RMUL : thm
val REAL_DIV_RMUL_CANCEL : thm
val REAL_DIV_SUB : thm
val REAL_DIV_ZERO : thm
val REAL_DOUBLE : thm
val REAL_DOWN : thm
val REAL_DOWN2 : thm
val REAL_ENTIRE : thm
val REAL_EQ_IMP_LE : thm
val REAL_EQ_LADD : thm
val REAL_EQ_LDIV_EQ : thm
val REAL_EQ_LMUL : thm
val REAL_EQ_LMUL2 : thm
val REAL_EQ_LMUL_IMP : thm
val REAL_EQ_MUL_LCANCEL : thm
val REAL_EQ_NEG : thm
val REAL_EQ_RADD : thm
val REAL_EQ_RDIV_EQ : thm
val REAL_EQ_RMUL : thm
val REAL_EQ_RMUL_IMP : thm
val REAL_EQ_SGN_ABS : thm
val REAL_EQ_SUB_LADD : thm
val REAL_EQ_SUB_RADD : thm
val REAL_FACT_NZ : thm
val REAL_HALF_BETWEEN : thm
val REAL_HALF_DOUBLE : thm
val REAL_IMP_INF_LE : thm
val REAL_IMP_LE_INF : thm
val REAL_IMP_LE_SUP : thm
val REAL_IMP_LT_SUP : thm
val REAL_IMP_MAX_LE2 : thm
val REAL_IMP_MIN_LE2 : thm
val REAL_IMP_SUP_LE : thm
val REAL_INF : thm
val REAL_INF_CLOSE : thm
val REAL_INF_LE : thm
val REAL_INF_LT : thm
val REAL_INF_MIN : thm
val REAL_INJ : thm
val REAL_INV1 : thm
val REAL_INVINV : thm
val REAL_INV_0 : thm
val REAL_INV_1 : thm
val REAL_INV_1OVER : thm
val REAL_INV_1_LE : thm
val REAL_INV_DIV : thm
val REAL_INV_DIV' : thm
val REAL_INV_EQ_0 : thm
val REAL_INV_EQ_0' : thm
val REAL_INV_INJ : thm
val REAL_INV_INV : thm
val REAL_INV_LE_1 : thm
val REAL_INV_LE_ANTIMONO : thm
val REAL_INV_LE_ANTIMONO_IMPL : thm
val REAL_INV_LE_ANTIMONO_IMPR : thm
val REAL_INV_LT0 : thm
val REAL_INV_LT1 : thm
val REAL_INV_LT_ANTIMONO : thm
val REAL_INV_MUL : thm
val REAL_INV_MUL' : thm
val REAL_INV_NEG : thm
val REAL_INV_NZ : thm
val REAL_INV_POS : thm
val REAL_INV_SGN : thm
val REAL_INV_nonzerop : thm
val REAL_LDISTRIB : thm
val REAL_LE : thm
val REAL_LE1_POW2 : thm
val REAL_LET_ADD : thm
val REAL_LET_ADD2 : thm
val REAL_LET_ANTISYM : thm
val REAL_LET_TOTAL : thm
val REAL_LET_TRANS : thm
val REAL_LE_01 : thm
val REAL_LE_ADD : thm
val REAL_LE_ADD2 : thm
val REAL_LE_ADDL : thm
val REAL_LE_ADDR : thm
val REAL_LE_ANTISYM : thm
val REAL_LE_DIV : thm
val REAL_LE_DOUBLE : thm
val REAL_LE_EPSILON : thm
val REAL_LE_INV : thm
val REAL_LE_INV2 : thm
val REAL_LE_INV_EQ : thm
val REAL_LE_LADD : thm
val REAL_LE_LADD_IMP : thm
val REAL_LE_LCANCEL_IMP : thm
val REAL_LE_LDIV : thm
val REAL_LE_LDIV_EQ : thm
val REAL_LE_LMUL : thm
val REAL_LE_LMUL1 : thm
val REAL_LE_LMUL_IMP : thm
val REAL_LE_LMUL_NEG : thm
val REAL_LE_LMUL_NEG_IMP : thm
val REAL_LE_LNEG : thm
val REAL_LE_LT : thm
val REAL_LE_MAX : thm
val REAL_LE_MAX1 : thm
val REAL_LE_MAX2 : thm
val REAL_LE_MIN : thm
val REAL_LE_MUL : thm
val REAL_LE_MUL2 : thm
val REAL_LE_NEG : thm
val REAL_LE_NEG2 : thm
val REAL_LE_NEGL : thm
val REAL_LE_NEGR : thm
val REAL_LE_NEGTOTAL : thm
val REAL_LE_POW2 : thm
val REAL_LE_RADD : thm
val REAL_LE_RCANCEL_IMP : thm
val REAL_LE_RDIV : thm
val REAL_LE_RDIV_CANCEL : thm
val REAL_LE_RDIV_EQ : thm
val REAL_LE_REFL : thm
val REAL_LE_RMUL : thm
val REAL_LE_RMUL1 : thm
val REAL_LE_RMUL_IMP : thm
val REAL_LE_RNEG : thm
val REAL_LE_SQUARE : thm
val REAL_LE_SUB_CANCEL1 : thm
val REAL_LE_SUB_CANCEL2 : thm
val REAL_LE_SUB_LADD : thm
val REAL_LE_SUB_RADD : thm
val REAL_LE_SUP : thm
val REAL_LE_TOTAL : thm
val REAL_LE_TRANS : thm
val REAL_LINV_UNIQ : thm
val REAL_LIN_LE_MAX : thm
val REAL_LNEG_UNIQ : thm
val REAL_LT : thm
val REAL_LT1_POW2 : thm
val REAL_LTE_ADD : thm
val REAL_LTE_ADD2 : thm
val REAL_LTE_ANTISYM : thm
val REAL_LTE_ANTSYM : thm
val REAL_LTE_TOTAL : thm
val REAL_LTE_TRANS : thm
val REAL_LT_01 : thm
val REAL_LT_1 : thm
val REAL_LT_ADD : thm
val REAL_LT_ADD1 : thm
val REAL_LT_ADD2 : thm
val REAL_LT_ADDL : thm
val REAL_LT_ADDNEG : thm
val REAL_LT_ADDNEG2 : thm
val REAL_LT_ADDR : thm
val REAL_LT_ADD_SUB : thm
val REAL_LT_ANTISYM : thm
val REAL_LT_DIV : thm
val REAL_LT_FRACTION : thm
val REAL_LT_FRACTION_0 : thm
val REAL_LT_GT : thm
val REAL_LT_HALF1 : thm
val REAL_LT_HALF2 : thm
val REAL_LT_IADD : thm
val REAL_LT_IMP_LE : thm
val REAL_LT_IMP_NE : thm
val REAL_LT_INV : thm
val REAL_LT_INV' : thm
val REAL_LT_INV2 : thm
val REAL_LT_INV_EQ : thm
val REAL_LT_LADD : thm
val REAL_LT_LDIV_EQ : thm
val REAL_LT_LE : thm
val REAL_LT_LMUL : thm
val REAL_LT_LMUL_0 : thm
val REAL_LT_LMUL_IMP : thm
val REAL_LT_LMUL_NEG : thm
val REAL_LT_MAX : thm
val REAL_LT_MIN : thm
val REAL_LT_MUL : thm
val REAL_LT_MUL2 : thm
val REAL_LT_MULTIPLE : thm
val REAL_LT_NEG : thm
val REAL_LT_NEGTOTAL : thm
val REAL_LT_NZ : thm
val REAL_LT_RADD : thm
val REAL_LT_RDIV : thm
val REAL_LT_RDIV_0 : thm
val REAL_LT_RDIV_EQ : thm
val REAL_LT_REFL : thm
val REAL_LT_RMUL : thm
val REAL_LT_RMUL_0 : thm
val REAL_LT_RMUL_IMP : thm
val REAL_LT_RNEG : thm
val REAL_LT_SUB_LADD : thm
val REAL_LT_SUB_RADD : thm
val REAL_LT_TOTAL : thm
val REAL_LT_TRANS : thm
val REAL_MAX_ACI : thm
val REAL_MAX_ADD : thm
val REAL_MAX_ALT : thm
val REAL_MAX_LE : thm
val REAL_MAX_LT : thm
val REAL_MAX_MIN : thm
val REAL_MAX_REFL : thm
val REAL_MAX_SUB : thm
val REAL_MAX_SUB_MIN : thm
val REAL_MEAN : thm
val REAL_MIDDLE1 : thm
val REAL_MIDDLE2 : thm
val REAL_MIN_ACI : thm
val REAL_MIN_ADD : thm
val REAL_MIN_ALT : thm
val REAL_MIN_LE : thm
val REAL_MIN_LE1 : thm
val REAL_MIN_LE2 : thm
val REAL_MIN_LE_LIN : thm
val REAL_MIN_LE_MAX : thm
val REAL_MIN_LT : thm
val REAL_MIN_MAX : thm
val REAL_MIN_REFL : thm
val REAL_MIN_SUB : thm
val REAL_MUL : thm
val REAL_MUL_ASSOC : thm
val REAL_MUL_COMM : thm
val REAL_MUL_LID : thm
val REAL_MUL_LINV : thm
val REAL_MUL_LNEG : thm
val REAL_MUL_LZERO : thm
val REAL_MUL_RID : thm
val REAL_MUL_RINV : thm
val REAL_MUL_RNEG : thm
val REAL_MUL_RZERO : thm
val REAL_MUL_SIGN : thm
val REAL_MUL_SUB1_CANCEL : thm
val REAL_MUL_SUB2_CANCEL : thm
val REAL_MUL_SYM : thm
val REAL_NEGNEG : thm
val REAL_NEG_0 : thm
val REAL_NEG_ADD : thm
val REAL_NEG_EQ : thm
val REAL_NEG_EQ0 : thm
val REAL_NEG_GE0 : thm
val REAL_NEG_GT0 : thm
val REAL_NEG_HALF : thm
val REAL_NEG_INV : thm
val REAL_NEG_INV' : thm
val REAL_NEG_LE0 : thm
val REAL_NEG_LMUL : thm
val REAL_NEG_LT0 : thm
val REAL_NEG_MINUS1 : thm
val REAL_NEG_MUL2 : thm
val REAL_NEG_NEG : thm
val REAL_NEG_RMUL : thm
val REAL_NEG_SUB : thm
val REAL_NEG_THIRD : thm
val REAL_NOT_LE : thm
val REAL_NOT_LT : thm
val REAL_NZ_IMP_LT : thm
val REAL_OF_NUM_ADD : thm
val REAL_OF_NUM_EQ : thm
val REAL_OF_NUM_LE : thm
val REAL_OF_NUM_LT : thm
val REAL_OF_NUM_MUL : thm
val REAL_OF_NUM_POW : thm
val REAL_OF_NUM_SUC : thm
val REAL_OVER1 : thm
val REAL_POS : thm
val REAL_POSSQ : thm
val REAL_POS_EQ_ZERO : thm
val REAL_POS_ID : thm
val REAL_POS_INFLATE : thm
val REAL_POS_LE_ZERO : thm
val REAL_POS_LT : thm
val REAL_POS_MONO : thm
val REAL_POS_NZ : thm
val REAL_POS_POS : thm
val REAL_POW : thm
val REAL_POW2_ABS : thm
val REAL_POW_1_LE : thm
val REAL_POW_ADD : thm
val REAL_POW_ANTIMONO : thm
val REAL_POW_ANTIMONO_LT : thm
val REAL_POW_DIV : thm
val REAL_POW_EQ_0 : thm
val REAL_POW_GE0 : thm
val REAL_POW_INV : thm
val REAL_POW_LBOUND : thm
val REAL_POW_LE : thm
val REAL_POW_LE0 : thm
val REAL_POW_LE_1 : thm
val REAL_POW_LT : thm
val REAL_POW_LT2 : thm
val REAL_POW_MONO : thm
val REAL_POW_MONO_LT : thm
val REAL_POW_NEG : thm
val REAL_POW_NEG2 : thm
val REAL_POW_POS : thm
val REAL_POW_POW : thm
val REAL_RDISTRIB : thm
val REAL_RINV_UNIQ : thm
val REAL_RNEG_UNIQ : thm
val REAL_SGN : thm
val REAL_SGNS_EQ : thm
val REAL_SGNS_EQ_ALT : thm
val REAL_SGN_0 : thm
val REAL_SGN_ABS : thm
val REAL_SGN_ABS_ALT : thm
val REAL_SGN_CASES : thm
val REAL_SGN_DIV : thm
val REAL_SGN_EQ : thm
val REAL_SGN_EQ_INEQ : thm
val REAL_SGN_INEQS : thm
val REAL_SGN_INV : thm
val REAL_SGN_MUL : thm
val REAL_SGN_NEG : thm
val REAL_SGN_POW : thm
val REAL_SGN_POW_2 : thm
val REAL_SGN_REAL_SGN : thm
val REAL_SUB : thm
val REAL_SUB_0 : thm
val REAL_SUB_ABS : thm
val REAL_SUB_ADD : thm
val REAL_SUB_ADD2 : thm
val REAL_SUB_INV2 : thm
val REAL_SUB_LDISTRIB : thm
val REAL_SUB_LE : thm
val REAL_SUB_LNEG : thm
val REAL_SUB_LT : thm
val REAL_SUB_LZERO : thm
val REAL_SUB_NEG2 : thm
val REAL_SUB_RAT : thm
val REAL_SUB_RDISTRIB : thm
val REAL_SUB_REFL : thm
val REAL_SUB_RNEG : thm
val REAL_SUB_RZERO : thm
val REAL_SUB_SUB : thm
val REAL_SUB_SUB2 : thm
val REAL_SUB_TRIANGLE : thm
val REAL_SUMSQ : thm
val REAL_SUP : thm
val REAL_SUP_ALLPOS : thm
val REAL_SUP_CONST : thm
val REAL_SUP_EXISTS : thm
val REAL_SUP_EXISTS_UNIQUE : thm
val REAL_SUP_LE : thm
val REAL_SUP_MAX : thm
val REAL_SUP_SOMEPOS : thm
val REAL_SUP_UBOUND : thm
val REAL_SUP_UBOUND_LE : thm
val REAL_THIRDS_BETWEEN : thm
val SETOK_LE_LT : thm
val SIMP_REAL_ARCH : thm
val SIMP_REAL_ARCH_NEG : thm
val SQRT_0 : thm
val SQRT_1 : thm
val SQRT_DIV : thm
val SQRT_EQ : thm
val SQRT_INV : thm
val SQRT_MONO_LE : thm
val SQRT_MONO_LT : thm
val SQRT_MUL : thm
val SQRT_POS_LE : thm
val SQRT_POS_LT : thm
val SQRT_POS_NE : thm
val SQRT_POS_UNIQ : thm
val SQRT_POW2 : thm
val SQRT_POW_2 : thm
val SUB_POW_2 : thm
val SUM_0 : thm
val SUM_1 : thm
val SUM_2 : thm
val SUM_ABS : thm
val SUM_ABS_LE : thm
val SUM_ADD : thm
val SUM_BOUND : thm
val SUM_CANCEL : thm
val SUM_CMUL : thm
val SUM_DIFF : thm
val SUM_DIFFS : thm
val SUM_EQ : thm
val SUM_EQ_0 : thm
val SUM_GROUP : thm
val SUM_LE : thm
val SUM_LT : thm
val SUM_NEG : thm
val SUM_NSUB : thm
val SUM_OFFSET : thm
val SUM_PERMUTE_0 : thm
val SUM_PICK : thm
val SUM_POS : thm
val SUM_POS_GEN : thm
val SUM_REINDEX : thm
val SUM_SPLIT : thm
val SUM_SUB : thm
val SUM_SUBST : thm
val SUM_TWO : thm
val SUM_ZERO : thm
val SUP_EPSILON : thm
val SUP_LEMMA1 : thm
val SUP_LEMMA2 : thm
val SUP_LEMMA3 : thm
val SUP_LT_EPSILON : thm
val X_HALF_HALF : thm
val ZERO_LT_POW : thm
val ZERO_LT_invx : thm
val abs : thm
val add_ints : thm
val add_rat : thm
val add_ratl : thm
val add_ratr : thm
val div_rat : thm
val div_ratl : thm
val div_ratr : thm
val eq_ints : thm
val eq_rat : thm
val eq_ratl : thm
val eq_ratr : thm
val le_int : thm
val le_rat : thm
val le_ratl : thm
val le_ratr : thm
val lt_int : thm
val lt_rat : thm
val lt_ratl : thm
val lt_ratr : thm
val max_def : thm
val min_def : thm
val mult_ints : thm
val mult_rat : thm
val mult_ratl : thm
val mult_ratr : thm
val neg_rat : thm
val nonzerop_0 : thm
val nonzerop_EQ0 : thm
val nonzerop_EQ1_I : thm
val nonzerop_NUMERAL : thm
val nonzerop_inv : thm
val nonzerop_mulXX : thm
val nonzerop_mult : thm
val nonzerop_nonzero_pow : thm
val nonzerop_nonzerop : thm
val nonzerop_pow : thm
val pow : thm
val pow0 : thm
val pow_eq0 : thm
val pow_inv_eq : thm
val pow_inv_mul : thm
val pow_inv_mul_invlt : thm
val pow_inv_mul_powlt : thm
val pow_rat : thm
val real_div : thm
val real_ge : thm
val real_gt : thm
val real_lt : thm
val real_lte : thm
val real_of_num : thm
val real_sub : thm
val sum : thm
val sum_compute : thm
val sum_ind : thm
val real_grammars : type_grammar.grammar * term_grammar.grammar
(*
[realax] Parent theory of "real"
[res_quan] Parent theory of "real"
[NUM_CEILING_def] Definition
⊢ ∀x. clg x = LEAST n. x ≤ &n
[NUM_FLOOR_def] Definition
⊢ ∀x. flr x = LEAST n. &(n + 1) > x
[inf_def] Definition
⊢ ∀p. inf p = -sup (λr. p (-r))
[nonzerop_def] Definition
⊢ ∀r. NZ r = if r = 0 then 0 else 1
[pos_def] Definition
⊢ ∀x. pos x = if 0 ≤ x then x else 0
[real_sgn] Definition
⊢ ∀x. sgn x = if 0 < x then 1 else if x < 0 then -1 else 0
[sqrt_def] Definition
⊢ ∀x. sqrt x = @u. (0 < x ⇒ 0 < u) ∧ u² = x
[sup] Definition
⊢ ∀P. sup P = @s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
[ABS_0] Theorem
⊢ abs 0 = 0
[ABS_1] Theorem
⊢ abs 1 = 1
[ABS_ABS] Theorem
⊢ ∀x. abs (abs x) = abs x
[ABS_BETWEEN] Theorem
⊢ ∀x y d. 0 < d ∧ x − d < y ∧ y < x + d ⇔ abs (y − x) < d
[ABS_BETWEEN1] Theorem
⊢ ∀x y z. x < z ∧ abs (y − x) < z − x ⇒ y < z
[ABS_BETWEEN2] Theorem
⊢ ∀x0 x y0 y.
x0 < y0 ∧ abs (x − x0) < (y0 − x0) / 2 ∧
abs (y − y0) < (y0 − x0) / 2 ⇒
x < y
[ABS_BOUND] Theorem
⊢ ∀x y d. abs (x − y) < d ⇒ y < x + d
[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_BOUNDS_MIN_MAX] Theorem
⊢ ∀a b x B. abs x ≤ B ⇒ min a (-B) ≤ x ∧ x ≤ max b B
[ABS_CASES] Theorem
⊢ ∀x. x = 0 ∨ 0 < abs x
[ABS_CIRCLE] Theorem
⊢ ∀x y h. abs h < abs y − abs x ⇒ abs (x + h) < abs y
[ABS_DIV] Theorem
⊢ ∀y. y ≠ 0 ⇒ ∀x. abs (x / y) = abs x / abs y
[ABS_INV] Theorem
⊢ ∀x. x ≠ 0 ⇒ abs x⁻¹ = (abs x)⁻¹
[ABS_LE] Theorem
⊢ ∀x. x ≤ abs x
[ABS_LT_MUL2] Theorem
⊢ ∀w x y z. abs w < y ∧ abs x < z ⇒ abs (w * x) < y * z
[ABS_MUL] Theorem
⊢ ∀x y. abs (x * y) = abs x * abs y
[ABS_N] Theorem
⊢ ∀n. abs (&n) = &n
[ABS_NEG] Theorem
⊢ ∀x. abs (-x) = abs x
[ABS_NZ] Theorem
⊢ ∀x. x ≠ 0 ⇔ 0 < abs x
[ABS_NZ'] Theorem
⊢ ∀x. 0 < abs x ⇔ x ≠ 0
[ABS_POS] Theorem
⊢ ∀x. 0 ≤ abs x
[ABS_POW2] Theorem
⊢ ∀x. abs x² = x²
[ABS_REFL] Theorem
⊢ ∀x. abs x = x ⇔ 0 ≤ x
[ABS_SIGN] Theorem
⊢ ∀x y. abs (x − y) < y ⇒ 0 < x
[ABS_SIGN2] Theorem
⊢ ∀x y. abs (x − y) < -y ⇒ x < 0
[ABS_STILLNZ] Theorem
⊢ ∀x y. abs (x − y) < abs y ⇒ x ≠ 0
[ABS_SUB] Theorem
⊢ ∀x y. abs (x − y) = abs (y − x)
[ABS_SUB_ABS] Theorem
⊢ ∀x y. abs (abs x − abs y) ≤ abs (x − y)
[ABS_SUM] Theorem
⊢ ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))
[ABS_TRIANGLE] Theorem
⊢ ∀x y. abs (x + y) ≤ abs x + abs y
[ABS_TRIANGLE_LT] Theorem
⊢ ∀x y. abs x + abs y < e ⇒ abs (x + y) < e
[ABS_TRIANGLE_NEG] Theorem
⊢ ∀x y. abs (x − y) ≤ abs x + abs y
[ABS_TRIANGLE_SUB] Theorem
⊢ ∀x y. abs x ≤ abs y + abs (x − y)
[ABS_ZERO] Theorem
⊢ ∀x. abs x = 0 ⇔ x = 0
[ADD_POW_2] Theorem
⊢ ∀x y. (x + y)² = x² + y² + 2 * x * y
[CLG_UBOUND] Theorem
⊢ ∀x. 0 ≤ x ⇒ &clg x < x + 1
[HALF_CANCEL] Theorem
⊢ 2 * (1 / 2) = 1
[HALF_LT_1] Theorem
⊢ 1 / 2 < 1
[HALF_POS] Theorem
⊢ 0 < 1 / 2
[INFINITE_REAL_UNIV] Theorem
⊢ INFINITE 𝕌(:real)
[LE_NUM_CEILING] Theorem
⊢ ∀x. x ≤ &clg x
[NEGATED_POW] Theorem
⊢ -x pow NUMERAL (BIT1 n) = -(x pow NUMERAL (BIT1 n)) ∧
-x pow NUMERAL (BIT2 n) = x pow NUMERAL (BIT2 n)
[NUM_CEILING_LE] Theorem
⊢ ∀x n. x ≤ &n ⇒ clg x ≤ n
[NUM_CEILING_NUM_FLOOR] Theorem
⊢ ∀r. clg r = (let n = flr r in if r ≤ 0 ∨ r = &n then n else n + 1)
[NUM_CEILING_UPPER_BOUND] Theorem
⊢ ∀x. 0 ≤ x ⇒ &clg x < x + 1
[NUM_FLOOR_BASE] Theorem
⊢ ∀r. r < 1 ⇒ flr r = 0
[NUM_FLOOR_DIV] Theorem
⊢ 0 ≤ x ∧ 0 < y ⇒ &flr (x / y) * y ≤ x
[NUM_FLOOR_DIV_LOWERBOUND] Theorem
⊢ 0 ≤ x ∧ 0 < y ⇒ x < &(flr (x / y) + 1) * y
[NUM_FLOOR_EQNS] Theorem
⊢ flr (&n) = n ∧ flr (-&n) = 0 ∧ (0 < m ⇒ flr (&n / &m) = n DIV m) ∧
(0 < m ⇒ flr (-&n / &m) = 0)
[NUM_FLOOR_LE] Theorem
⊢ 0 ≤ x ⇒ &flr x ≤ x
[NUM_FLOOR_LE2] Theorem
⊢ 0 ≤ y ⇒ (x ≤ flr y ⇔ &x ≤ y)
[NUM_FLOOR_LET] Theorem
⊢ flr x ≤ y ⇔ x < &y + 1
[NUM_FLOOR_LOWER_BOUND] Theorem
⊢ x < &n ⇔ flr (x + 1) ≤ n
[NUM_FLOOR_LT] Theorem
⊢ ∀x. x − 1 < &flr x
[NUM_FLOOR_MONO] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ∧ x ≤ y ⇒ flr x ≤ flr y
[NUM_FLOOR_MUL_LOWERBOUND] Theorem
⊢ ∀n x. 1 < n ∧ 1 ≤ x ⇒ x < &(n * flr x)
[NUM_FLOOR_lower_bound] Theorem
⊢ ∀x. 1 ≤ x ⇒ x / 2 < &flr x
[NUM_FLOOR_upper_bound] Theorem
⊢ &n ≤ x ⇔ n < flr (x + 1)
[ONE_MINUS_HALF] Theorem
⊢ 1 − 1 / 2 = 1 / 2
[POW_0] Theorem
⊢ ∀n. 0 pow SUC n = 0
[POW_0'] Theorem
⊢ 0 < n ⇒ 0 pow n = 0
[POW_1] Theorem
⊢ ∀x. x pow 1 = x
[POW_2] Theorem
⊢ ∀x. x² = x * x
[POW_2_LE1] Theorem
⊢ ∀n. 1 ≤ 2 pow n
[POW_2_LT] Theorem
⊢ ∀n. &n < 2 pow n
[POW_2_SQRT] Theorem
⊢ 0 ≤ x ⇒ sqrt x² = x
[POW_ABS] Theorem
⊢ ∀c n. abs c pow n = abs (c pow n)
[POW_ADD] Theorem
⊢ ∀c m n. c pow (m + n) = c pow m * c pow n
[POW_EQ] Theorem
⊢ ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ x pow SUC n = y pow SUC n ⇒ x = y
[POW_HALF_POS] Theorem
⊢ ∀n. 0 < (1 / 2) pow n
[POW_INV] Theorem
⊢ ∀c. c ≠ 0 ⇒ ∀n. (c pow n)⁻¹ = c⁻¹ pow n
[POW_LE] Theorem
⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n
[POW_LT] Theorem
⊢ ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n
[POW_M1] Theorem
⊢ ∀n. abs (-1 pow n) = 1
[POW_MINUS1] Theorem
⊢ ∀n. -1 pow (2 * n) = 1
[POW_MINUS1_ODD] Theorem
⊢ ∀n. -1 pow (2 * n + 1) = -1
[POW_MUL] Theorem
⊢ ∀n x y. (x * y) pow n = x pow n * y pow n
[POW_NZ] Theorem
⊢ ∀c n. c ≠ 0 ⇒ c pow n ≠ 0
[POW_ONE] Theorem
⊢ ∀n. 1 pow n = 1
[POW_PLUS1] Theorem
⊢ ∀e. 0 < e ⇒ ∀n. 1 + &n * e ≤ (1 + e) pow n
[POW_POS] Theorem
⊢ ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n
[POW_POS_LT] Theorem
⊢ ∀x n. 0 < x ⇒ 0 < x pow SUC n
[POW_ZERO] Theorem
⊢ ∀n x. x pow n = 0 ⇒ x = 0
[POW_ZERO_EQ] Theorem
⊢ ∀n x. x pow SUC n = 0 ⇔ x = 0
[RAT_LEMMA1] Theorem
⊢ y1 ≠ 0 ∧ y2 ≠ 0 ⇒
x1 / y1 + x2 / y2 = (x1 * y2 + x2 * y1) * y1⁻¹ * y2⁻¹
[RAT_LEMMA2] Theorem
⊢ 0 < y1 ∧ 0 < y2 ⇒
x1 / y1 + x2 / y2 = (x1 * y2 + x2 * y1) * y1⁻¹ * y2⁻¹
[RAT_LEMMA3] Theorem
⊢ 0 < y1 ∧ 0 < y2 ⇒
x1 / y1 − x2 / y2 = (x1 * y2 − x2 * y1) * y1⁻¹ * y2⁻¹
[RAT_LEMMA4] Theorem
⊢ 0 < y1 ∧ 0 < y2 ⇒ (x1 / y1 ≤ x2 / y2 ⇔ x1 * y2 ≤ x2 * y1)
[RAT_LEMMA5] Theorem
⊢ 0 < y1 ∧ 0 < y2 ⇒ (x1 / y1 = x2 / y2 ⇔ x1 * y2 = x2 * y1)
[RAT_LEMMA5_BETTER] Theorem
⊢ y1 ≠ 0 ∧ y2 ≠ 0 ⇒ (x1 / y1 = x2 / y2 ⇔ x1 * y2 = x2 * y1)
[REAL] Theorem
⊢ ∀n. &SUC n = &n + 1
[REAL_0] Theorem
⊢ real_0 = 0
[REAL_1] Theorem
⊢ real_1 = 1
[REAL_10] Theorem
⊢ 1 ≠ 0
[REAL_ABS_0] Theorem
⊢ abs 0 = 0
[REAL_ABS_DIV] Theorem
⊢ ∀x y. abs (x / y) = abs x / abs y
[REAL_ABS_LE0] Theorem
⊢ ∀v. abs v ≤ 0 ⇔ v = 0
[REAL_ABS_MUL] Theorem
⊢ ∀x y. abs (x * y) = abs x * abs y
[REAL_ABS_POS] Theorem
⊢ ∀x. 0 ≤ abs x
[REAL_ABS_SGN] Theorem
⊢ ∀x. abs (sgn x) = sgn (abs x)
[REAL_ABS_TRIANGLE] Theorem
⊢ ∀x y. abs (x + y) ≤ abs x + abs y
[REAL_ADD] Theorem
⊢ ∀m n. &m + &n = &(m + n)
[REAL_ADD2_SUB2] Theorem
⊢ ∀a b c d. a + b − (c + d) = a − c + (b − d)
[REAL_ADD_ASSOC] Theorem
⊢ ∀x y z. x + (y + z) = x + y + z
[REAL_ADD_COMM] Theorem
⊢ ∀x y. x + y = y + x
[REAL_ADD_LDISTRIB] Theorem
⊢ ∀x y z. x * (y + z) = x * y + x * z
[REAL_ADD_LID] Theorem
⊢ ∀x. 0 + x = x
[REAL_ADD_LID_UNIQ] Theorem
⊢ ∀x y. x + y = y ⇔ x = 0
[REAL_ADD_LINV] Theorem
⊢ ∀x. -x + x = 0
[REAL_ADD_RAT] Theorem
⊢ ∀a b c d. b ≠ 0 ∧ d ≠ 0 ⇒ a / b + c / d = (a * d + b * c) / (b * d)
[REAL_ADD_RDISTRIB] Theorem
⊢ ∀x y z. (x + y) * z = x * z + y * z
[REAL_ADD_RID] Theorem
⊢ ∀x. x + 0 = x
[REAL_ADD_RID_UNIQ] Theorem
⊢ ∀x y. x + y = x ⇔ y = 0
[REAL_ADD_RINV] Theorem
⊢ ∀x. x + -x = 0
[REAL_ADD_SUB] Theorem
⊢ ∀x y. x + y − x = y
[REAL_ADD_SUB2] Theorem
⊢ ∀x y. x − (x + y) = -y
[REAL_ADD_SUB_ALT] Theorem
⊢ ∀x y. x + y − y = x
[REAL_ADD_SYM] Theorem
⊢ ∀x y. x + y = y + x
[REAL_ARCH] Theorem
⊢ ∀x. 0 < x ⇒ ∀y. ∃n. y < &n * x
[REAL_ARCH_INV] Theorem
⊢ ∀e. 0 < e ⇔ ∃n. n ≠ 0 ∧ 0 < (&n)⁻¹ ∧ (&n)⁻¹ < e
[REAL_ARCH_LEAST] Theorem
⊢ ∀y. 0 < y ⇒ ∀x. 0 ≤ x ⇒ ∃n. &n * y ≤ x ∧ x < &SUC n * y
[REAL_ARCH_POW] Theorem
⊢ ∀x y. 1 < x ⇒ ∃n. y < x pow n
[REAL_ARCH_POW2] Theorem
⊢ ∀x. ∃n. x < 2 pow n
[REAL_ARCH_POW_INV] Theorem
⊢ ∀x y. 0 < y ∧ x < 1 ⇒ ∃n. x pow n < y
[REAL_BIGNUM] Theorem
⊢ ∀r. ∃n. r < &n
[REAL_DIFFSQ] Theorem
⊢ ∀x y. (x + y) * (x − y) = x * x − y * y
[REAL_DIV_ADD] Theorem
⊢ ∀x y z. y / x + z / x = (y + z) / x
[REAL_DIV_DENOM_CANCEL] Theorem
⊢ ∀x y z. x ≠ 0 ⇒ y / x / (z / x) = y / z
[REAL_DIV_DENOM_CANCEL2] Theorem
⊢ ∀y z. y / 2 / (z / 2) = y / z
[REAL_DIV_DENOM_CANCEL3] Theorem
⊢ ∀y z. y / 3 / (z / 3) = y / z
[REAL_DIV_INNER_CANCEL] Theorem
⊢ ∀x y z. x ≠ 0 ⇒ y / x * (x / z) = y / z
[REAL_DIV_INNER_CANCEL2] Theorem
⊢ ∀y z. y / 2 * (2 / z) = y / z
[REAL_DIV_INNER_CANCEL3] Theorem
⊢ ∀y z. y / 3 * (3 / z) = y / z
[REAL_DIV_LMUL] Theorem
⊢ ∀x y. y ≠ 0 ⇒ y * (x / y) = x
[REAL_DIV_LMUL_CANCEL] Theorem
⊢ ∀c a b. c ≠ 0 ⇒ c * a / (c * b) = a / b
[REAL_DIV_LT] Theorem
⊢ ∀a b c d. 0 < b * d ⇒ (a / b < c / d ⇔ a * d < c * b)
[REAL_DIV_LZERO] Theorem
⊢ ∀x. 0 / x = 0
[REAL_DIV_MUL2] Theorem
⊢ ∀x z. x ≠ 0 ∧ z ≠ 0 ⇒ ∀y. y / z = x * y / (x * z)
[REAL_DIV_OUTER_CANCEL] Theorem
⊢ ∀x y z. x ≠ 0 ⇒ x / y * (z / x) = z / y
[REAL_DIV_OUTER_CANCEL2] Theorem
⊢ ∀y z. 2 / y * (z / 2) = z / y
[REAL_DIV_OUTER_CANCEL3] Theorem
⊢ ∀y z. 3 / y * (z / 3) = z / y
[REAL_DIV_PROD] Theorem
⊢ ∀a b c d. a / b * (c / d) = a * c / (b * d)
[REAL_DIV_REFL] Theorem
⊢ ∀x. x ≠ 0 ⇒ x / x = 1
[REAL_DIV_REFL2] Theorem
⊢ 2 / 2 = 1
[REAL_DIV_REFL3] Theorem
⊢ 3 / 3 = 1
[REAL_DIV_RMUL] Theorem
⊢ ∀x y. y ≠ 0 ⇒ x / y * y = x
[REAL_DIV_RMUL_CANCEL] Theorem
⊢ ∀c a b. c ≠ 0 ⇒ a * c / (b * c) = a / b
[REAL_DIV_SUB] Theorem
⊢ ∀x y z. y / x − z / x = (y − z) / x
[REAL_DIV_ZERO] Theorem
⊢ ∀a b. a / b = 0 ⇔ a = 0 ∨ b = 0
[REAL_DOUBLE] Theorem
⊢ ∀x. x + x = 2 * x
[REAL_DOWN] Theorem
⊢ ∀x. 0 < x ⇒ ∃y. 0 < y ∧ y < x
[REAL_DOWN2] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ ∃z. 0 < z ∧ z < x ∧ z < y
[REAL_ENTIRE] Theorem
⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
[REAL_EQ_IMP_LE] Theorem
⊢ ∀x y. x = y ⇒ x ≤ y
[REAL_EQ_LADD] Theorem
⊢ ∀x y z. x + y = x + z ⇔ y = z
[REAL_EQ_LDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / z = y ⇔ x = y * z)
[REAL_EQ_LMUL] Theorem
⊢ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z
[REAL_EQ_LMUL2] Theorem
⊢ ∀x y z. x ≠ 0 ⇒ (y = z ⇔ x * y = x * z)
[REAL_EQ_LMUL_IMP] Theorem
⊢ ∀x y z. x ≠ 0 ∧ x * y = x * z ⇒ y = z
[REAL_EQ_MUL_LCANCEL] Theorem
⊢ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z
[REAL_EQ_NEG] Theorem
⊢ ∀x y. -x = -y ⇔ x = y
[REAL_EQ_RADD] Theorem
⊢ ∀x y z. x + z = y + z ⇔ x = y
[REAL_EQ_RDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x = y / z ⇔ x * z = y)
[REAL_EQ_RMUL] Theorem
⊢ ∀x y z. x * z = y * z ⇔ z = 0 ∨ x = y
[REAL_EQ_RMUL_IMP] Theorem
⊢ ∀x y z. z ≠ 0 ∧ x * z = y * z ⇒ x = y
[REAL_EQ_SGN_ABS] Theorem
⊢ ∀x y. x = y ⇔ sgn x = sgn y ∧ abs x = abs y
[REAL_EQ_SUB_LADD] Theorem
⊢ ∀x y z. x = y − z ⇔ x + z = y
[REAL_EQ_SUB_RADD] Theorem
⊢ ∀x y z. x − y = z ⇔ x = z + y
[REAL_FACT_NZ] Theorem
⊢ ∀n. &FACT n ≠ 0
[REAL_HALF_BETWEEN] Theorem
⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
[REAL_HALF_DOUBLE] Theorem
⊢ ∀x. x / 2 + x / 2 = x
[REAL_IMP_INF_LE] Theorem
⊢ ∀p r. (∃z. ∀x. p x ⇒ z ≤ x) ∧ (∃x. p x ∧ x ≤ r) ⇒ inf p ≤ r
[REAL_IMP_LE_INF] Theorem
⊢ ∀p r. (∃x. p x) ∧ (∀x. p x ⇒ r ≤ x) ⇒ r ≤ inf p
[REAL_IMP_LE_SUP] Theorem
⊢ ∀p x. (∃z. ∀r. p r ⇒ r ≤ z) ∧ (∃r. p r ∧ x ≤ r) ⇒ x ≤ sup p
[REAL_IMP_LT_SUP] Theorem
⊢ ∀p x. (∃z. ∀r. p r ⇒ r ≤ z) ∧ ¬p (sup p) ∧ p x ⇒ x < sup p
[REAL_IMP_MAX_LE2] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
[REAL_IMP_MIN_LE2] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
[REAL_IMP_SUP_LE] Theorem
⊢ ∀p x. (∃r. p r) ∧ (∀r. p r ⇒ r ≤ x) ⇒ sup p ≤ x
[REAL_INF] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ z < x) ⇒
∀y. (∃x. P x ∧ x < y) ⇔ inf P < y
[REAL_INF_CLOSE] Theorem
⊢ ∀p e. (∃x. p x) ∧ 0 < e ⇒ ∃x. p x ∧ x < inf p + e
[REAL_INF_LE] Theorem
⊢ ∀p x.
(∃y. p y) ∧ (∃y. ∀z. p z ⇒ y ≤ z) ⇒
(inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x)
[REAL_INF_LT] Theorem
⊢ ∀p z. (∃x. p x) ∧ inf p < z ⇒ ∃x. p x ∧ x < z
[REAL_INF_MIN] Theorem
⊢ ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ inf p = z
[REAL_INJ] Theorem
⊢ ∀m n. &m = &n ⇔ m = n
[REAL_INV1] Theorem
⊢ 1⁻¹ = 1
[REAL_INVINV] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ⁻¹ = x
[REAL_INV_0] Theorem
⊢ 0⁻¹ = 0
[REAL_INV_1] Theorem
⊢ 1⁻¹ = 1
[REAL_INV_1OVER] Theorem
⊢ ∀x. x⁻¹ = 1 / x
[REAL_INV_1_LE] Theorem
⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ 1 ≤ x⁻¹
[REAL_INV_DIV] Theorem
⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x / y)⁻¹ = y * x⁻¹
[REAL_INV_DIV'] Theorem
⊢ ∀x y. (x / y)⁻¹ = y * x⁻¹
[REAL_INV_EQ_0] Theorem
⊢ ∀x. x⁻¹ = 0 ⇔ x = 0
[REAL_INV_EQ_0'] Theorem
⊢ ∀x. 0 = x⁻¹ ⇔ x = 0
[REAL_INV_INJ] Theorem
⊢ ∀x y. x⁻¹ = y⁻¹ ⇔ x = y
[REAL_INV_INV] Theorem
⊢ ∀x. x⁻¹ ⁻¹ = x
[REAL_INV_LE_1] Theorem
⊢ ∀x. 1 ≤ x ⇒ x⁻¹ ≤ 1
[REAL_INV_LE_ANTIMONO] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)
[REAL_INV_LE_ANTIMONO_IMPL] Theorem
⊢ ∀x y. x < 0 ∧ y < 0 ∧ y ≤ x ⇒ x⁻¹ ≤ y⁻¹
[REAL_INV_LE_ANTIMONO_IMPR] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ∧ y ≤ x ⇒ x⁻¹ ≤ y⁻¹
[REAL_INV_LT0] Theorem
⊢ x⁻¹ < 0 ⇔ x < 0
[REAL_INV_LT1] Theorem
⊢ ∀x. 0 < x ∧ x < 1 ⇒ 1 < x⁻¹
[REAL_INV_LT_ANTIMONO] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)
[REAL_INV_MUL] Theorem
⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x * y)⁻¹ = x⁻¹ * y⁻¹
[REAL_INV_MUL'] Theorem
⊢ ∀x y. (x * y)⁻¹ = x⁻¹ * y⁻¹
[REAL_INV_NEG] Theorem
⊢ ∀x. (-x)⁻¹ = -x⁻¹
[REAL_INV_NZ] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ≠ 0
[REAL_INV_POS] Theorem
⊢ ∀x. 0 < x ⇒ 0 < x⁻¹
[REAL_INV_SGN] Theorem
⊢ ∀x. (sgn x)⁻¹ = sgn x
[REAL_INV_nonzerop] Theorem
⊢ x * x⁻¹ = NZ x ∧ x⁻¹ * x = NZ x
[REAL_LDISTRIB] Theorem
⊢ ∀x y z. x * (y + z) = x * y + x * z
[REAL_LE] Theorem
⊢ ∀m n. &m ≤ &n ⇔ m ≤ n
[REAL_LE1_POW2] Theorem
⊢ ∀x. 1 ≤ x ⇒ 1 ≤ x²
[REAL_LET_ADD] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
[REAL_LET_ADD2] Theorem
⊢ ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z
[REAL_LET_ANTISYM] Theorem
⊢ ∀x y. ¬(x < y ∧ y ≤ x)
[REAL_LET_TOTAL] Theorem
⊢ ∀x y. x ≤ y ∨ y < x
[REAL_LET_TRANS] Theorem
⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
[REAL_LE_01] Theorem
⊢ 0 ≤ 1
[REAL_LE_ADD] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
[REAL_LE_ADD2] Theorem
⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
[REAL_LE_ADDL] Theorem
⊢ ∀x y. y ≤ x + y ⇔ 0 ≤ x
[REAL_LE_ADDR] Theorem
⊢ ∀x y. x ≤ x + y ⇔ 0 ≤ y
[REAL_LE_ANTISYM] Theorem
⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
[REAL_LE_DIV] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x / y
[REAL_LE_DOUBLE] Theorem
⊢ ∀x. 0 ≤ x + x ⇔ 0 ≤ x
[REAL_LE_EPSILON] Theorem
⊢ ∀x y. (∀e. 0 < e ⇒ x ≤ y + e) ⇒ x ≤ y
[REAL_LE_INV] Theorem
⊢ ∀x. 0 ≤ x ⇒ 0 ≤ x⁻¹
[REAL_LE_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x ≤ y ⇒ y⁻¹ ≤ x⁻¹
[REAL_LE_INV_EQ] Theorem
⊢ ∀x. 0 ≤ x⁻¹ ⇔ 0 ≤ x
[REAL_LE_LADD] Theorem
⊢ ∀x y z. x + y ≤ x + z ⇔ y ≤ z
[REAL_LE_LADD_IMP] Theorem
⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
[REAL_LE_LCANCEL_IMP] Theorem
⊢ ∀x y z. 0 < x ∧ x * y ≤ x * z ⇒ y ≤ z
[REAL_LE_LDIV] Theorem
⊢ ∀x y z. 0 < x ∧ y ≤ z * x ⇒ y / x ≤ z
[REAL_LE_LDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / z ≤ y ⇔ x ≤ y * z)
[REAL_LE_LMUL] Theorem
⊢ ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)
[REAL_LE_LMUL1] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
[REAL_LE_LMUL_IMP] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
[REAL_LE_LMUL_NEG] Theorem
⊢ ∀x y z. x < 0 ⇒ (x * y ≤ x * z ⇔ z ≤ y)
[REAL_LE_LMUL_NEG_IMP] Theorem
⊢ ∀a b c. a ≤ 0 ∧ b ≤ c ⇒ a * c ≤ a * b
[REAL_LE_LNEG] Theorem
⊢ ∀x y. -x ≤ y ⇔ 0 ≤ x + y
[REAL_LE_LT] Theorem
⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y
[REAL_LE_MAX] Theorem
⊢ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
[REAL_LE_MAX1] Theorem
⊢ ∀x y. x ≤ max x y
[REAL_LE_MAX2] Theorem
⊢ ∀x y. y ≤ max x y
[REAL_LE_MIN] Theorem
⊢ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
[REAL_LE_MUL] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[REAL_LE_MUL2] Theorem
⊢ ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2
[REAL_LE_NEG] Theorem
⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
[REAL_LE_NEG2] Theorem
⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
[REAL_LE_NEGL] Theorem
⊢ ∀x. -x ≤ x ⇔ 0 ≤ x
[REAL_LE_NEGR] Theorem
⊢ ∀x. x ≤ -x ⇔ x ≤ 0
[REAL_LE_NEGTOTAL] Theorem
⊢ ∀x. 0 ≤ x ∨ 0 ≤ -x
[REAL_LE_POW2] Theorem
⊢ ∀x. 0 ≤ x²
[REAL_LE_RADD] Theorem
⊢ ∀x y z. x + z ≤ y + z ⇔ x ≤ y
[REAL_LE_RCANCEL_IMP] Theorem
⊢ ∀x y z. 0 < z ∧ x * z ≤ y * z ⇒ x ≤ y
[REAL_LE_RDIV] Theorem
⊢ ∀x y z. 0 < x ∧ y * x ≤ z ⇒ y ≤ z / x
[REAL_LE_RDIV_CANCEL] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / z ≤ y / z ⇔ x ≤ y)
[REAL_LE_RDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x ≤ y / z ⇔ x * z ≤ y)
[REAL_LE_REFL] Theorem
⊢ ∀x. x ≤ x
[REAL_LE_RMUL] Theorem
⊢ ∀x y z. 0 < z ⇒ (x * z ≤ y * z ⇔ x ≤ y)
[REAL_LE_RMUL1] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ y * x ≤ z * x
[REAL_LE_RMUL_IMP] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ y * x ≤ z * x
[REAL_LE_RNEG] Theorem
⊢ ∀x y. x ≤ -y ⇔ x + y ≤ 0
[REAL_LE_SQUARE] Theorem
⊢ ∀x. 0 ≤ x * x
[REAL_LE_SUB_CANCEL1] Theorem
⊢ ∀x y z. z − x ≤ z − y ⇔ y ≤ x
[REAL_LE_SUB_CANCEL2] Theorem
⊢ ∀x y z. x − z ≤ y − z ⇔ x ≤ y
[REAL_LE_SUB_LADD] Theorem
⊢ ∀x y z. x ≤ y − z ⇔ x + z ≤ y
[REAL_LE_SUB_RADD] Theorem
⊢ ∀x y z. x − y ≤ z ⇔ x ≤ z + y
[REAL_LE_SUP] Theorem
⊢ ∀p x.
(∃y. p y) ∧ (∃y. ∀z. p z ⇒ z ≤ y) ⇒
(x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y)
[REAL_LE_TOTAL] Theorem
⊢ ∀x y. x ≤ y ∨ y ≤ x
[REAL_LE_TRANS] Theorem
⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
[REAL_LINV_UNIQ] Theorem
⊢ ∀x y. x * y = 1 ⇒ x = y⁻¹
[REAL_LIN_LE_MAX] Theorem
⊢ ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ z * x + (1 − z) * y ≤ max x y
[REAL_LNEG_UNIQ] Theorem
⊢ ∀x y. x + y = 0 ⇔ x = -y
[REAL_LT] Theorem
⊢ ∀m n. &m < &n ⇔ m < n
[REAL_LT1_POW2] Theorem
⊢ ∀x. 1 < x ⇒ 1 < x²
[REAL_LTE_ADD] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
[REAL_LTE_ADD2] Theorem
⊢ ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z
[REAL_LTE_ANTISYM] Theorem
⊢ ∀x y. ¬(x ≤ y ∧ y < x)
[REAL_LTE_ANTSYM] Theorem
⊢ ∀x y. ¬(x ≤ y ∧ y < x)
[REAL_LTE_TOTAL] Theorem
⊢ ∀x y. x < y ∨ y ≤ x
[REAL_LTE_TRANS] Theorem
⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
[REAL_LT_01] Theorem
⊢ 0 < 1
[REAL_LT_1] Theorem
⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ x / y < 1
[REAL_LT_ADD] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
[REAL_LT_ADD1] Theorem
⊢ ∀x y. x ≤ y ⇒ x < y + 1
[REAL_LT_ADD2] Theorem
⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
[REAL_LT_ADDL] Theorem
⊢ ∀x y. y < x + y ⇔ 0 < x
[REAL_LT_ADDNEG] Theorem
⊢ ∀x y z. y < x + -z ⇔ y + z < x
[REAL_LT_ADDNEG2] Theorem
⊢ ∀x y z. x + -y < z ⇔ x < z + y
[REAL_LT_ADDR] Theorem
⊢ ∀x y. x < x + y ⇔ 0 < y
[REAL_LT_ADD_SUB] Theorem
⊢ ∀x y z. x + y < z ⇔ x < z − y
[REAL_LT_ANTISYM] Theorem
⊢ ∀x y. ¬(x < y ∧ y < x)
[REAL_LT_DIV] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x / y
[REAL_LT_FRACTION] Theorem
⊢ ∀n d. 1 < n ⇒ (d / &n < d ⇔ 0 < d)
[REAL_LT_FRACTION_0] Theorem
⊢ ∀n d. n ≠ 0 ⇒ (0 < d / &n ⇔ 0 < d)
[REAL_LT_GT] Theorem
⊢ ∀x y. x < y ⇒ ¬(y < x)
[REAL_LT_HALF1] Theorem
⊢ ∀d. 0 < d / 2 ⇔ 0 < d
[REAL_LT_HALF2] Theorem
⊢ ∀d. d / 2 < d ⇔ 0 < d
[REAL_LT_IADD] Theorem
⊢ ∀x y z. y < z ⇒ x + y < x + z
[REAL_LT_IMP_LE] Theorem
⊢ ∀x y. x < y ⇒ x ≤ y
[REAL_LT_IMP_NE] Theorem
⊢ ∀x y. x < y ⇒ x ≠ y
[REAL_LT_INV] Theorem
⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹
[REAL_LT_INV'] Theorem
⊢ ∀x. 0 < x ⇒ 0 < x⁻¹
[REAL_LT_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹
[REAL_LT_INV_EQ] Theorem
⊢ ∀x. 0 < x⁻¹ ⇔ 0 < x
[REAL_LT_LADD] Theorem
⊢ ∀x y z. x + y < x + z ⇔ y < z
[REAL_LT_LDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / z < y ⇔ x < y * z)
[REAL_LT_LE] Theorem
⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
[REAL_LT_LMUL] Theorem
⊢ ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)
[REAL_LT_LMUL_0] Theorem
⊢ ∀x y. 0 < x ⇒ (0 < x * y ⇔ 0 < y)
[REAL_LT_LMUL_IMP] Theorem
⊢ ∀x y z. y < z ∧ 0 < x ⇒ x * y < x * z
[REAL_LT_LMUL_NEG] Theorem
⊢ ∀x y z. x < 0 ⇒ (x * y < x * z ⇔ z < y)
[REAL_LT_MAX] Theorem
⊢ ∀x y z. z < max x y ⇔ z < x ∨ z < y
[REAL_LT_MIN] Theorem
⊢ ∀x y z. z < min x y ⇔ z < x ∧ z < y
[REAL_LT_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
[REAL_LT_MUL2] Theorem
⊢ ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2
[REAL_LT_MULTIPLE] Theorem
⊢ ∀n d. 1 < n ⇒ (d < &n * d ⇔ 0 < d)
[REAL_LT_NEG] Theorem
⊢ ∀x y. -x < -y ⇔ y < x
[REAL_LT_NEGTOTAL] Theorem
⊢ ∀x. x = 0 ∨ 0 < x ∨ 0 < -x
[REAL_LT_NZ] Theorem
⊢ ∀n. &n ≠ 0 ⇔ 0 < &n
[REAL_LT_RADD] Theorem
⊢ ∀x y z. x + z < y + z ⇔ x < y
[REAL_LT_RDIV] Theorem
⊢ ∀x y z. 0 < z ⇒ (x / z < y / z ⇔ x < y)
[REAL_LT_RDIV_0] Theorem
⊢ ∀y z. 0 < z ⇒ (0 < y / z ⇔ 0 < y)
[REAL_LT_RDIV_EQ] Theorem
⊢ ∀x y z. 0 < z ⇒ (x < y / z ⇔ x * z < y)
[REAL_LT_REFL] Theorem
⊢ ∀x. ¬(x < x)
[REAL_LT_RMUL] Theorem
⊢ ∀x y z. 0 < z ⇒ (x * z < y * z ⇔ x < y)
[REAL_LT_RMUL_0] Theorem
⊢ ∀x y. 0 < y ⇒ (0 < x * y ⇔ 0 < x)
[REAL_LT_RMUL_IMP] Theorem
⊢ ∀x y z. x < y ∧ 0 < z ⇒ x * z < y * z
[REAL_LT_RNEG] Theorem
⊢ ∀x y. x < -y ⇔ x + y < 0
[REAL_LT_SUB_LADD] Theorem
⊢ ∀x y z. x < y − z ⇔ x + z < y
[REAL_LT_SUB_RADD] Theorem
⊢ ∀x y z. x − y < z ⇔ x < z + y
[REAL_LT_TOTAL] Theorem
⊢ ∀x y. x = y ∨ x < y ∨ y < x
[REAL_LT_TRANS] Theorem
⊢ ∀x y z. x < y ∧ y < z ⇒ x < z
[REAL_MAX_ACI] Theorem
⊢ ∀x y z.
max x y = max y x ∧ max (max x y) z = max x (max y z) ∧
max x (max y z) = max y (max x z) ∧ max x x = x ∧
max x (max x y) = max x y
[REAL_MAX_ADD] Theorem
⊢ ∀z x y. max (x + z) (y + z) = max x y + z
[REAL_MAX_ALT] Theorem
⊢ ∀x y. (x ≤ y ⇒ max x y = y) ∧ (y ≤ x ⇒ max x y = x)
[REAL_MAX_LE] Theorem
⊢ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
[REAL_MAX_LT] Theorem
⊢ ∀x y z. max x y < z ⇔ x < z ∧ y < z
[REAL_MAX_MIN] Theorem
⊢ ∀x y. max x y = -min (-x) (-y)
[REAL_MAX_REFL] Theorem
⊢ ∀x. max x x = x
[REAL_MAX_SUB] Theorem
⊢ ∀z x y. max (x − z) (y − z) = max x y − z
[REAL_MAX_SUB_MIN] Theorem
⊢ ∀x y. max x y − min x y = abs (y − x)
[REAL_MEAN] Theorem
⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
[REAL_MIDDLE1] Theorem
⊢ ∀a b. a ≤ b ⇒ a ≤ (a + b) / 2
[REAL_MIDDLE2] Theorem
⊢ ∀a b. a ≤ b ⇒ (a + b) / 2 ≤ b
[REAL_MIN_ACI] Theorem
⊢ ∀x y z.
min x y = min y x ∧ min (min x y) z = min x (min y z) ∧
min x (min y z) = min y (min x z) ∧ min x x = x ∧
min x (min x y) = min x y
[REAL_MIN_ADD] Theorem
⊢ ∀z x y. min (x + z) (y + z) = min x y + z
[REAL_MIN_ALT] Theorem
⊢ ∀x y. (x ≤ y ⇒ min x y = x) ∧ (y ≤ x ⇒ min x y = y)
[REAL_MIN_LE] Theorem
⊢ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
[REAL_MIN_LE1] Theorem
⊢ ∀x y. min x y ≤ x
[REAL_MIN_LE2] Theorem
⊢ ∀x y. min x y ≤ y
[REAL_MIN_LE_LIN] Theorem
⊢ ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ min x y ≤ z * x + (1 − z) * y
[REAL_MIN_LE_MAX] Theorem
⊢ ∀x y. min x y ≤ max x y
[REAL_MIN_LT] Theorem
⊢ ∀x y z. min x y < z ⇔ x < z ∨ y < z
[REAL_MIN_MAX] Theorem
⊢ ∀x y. min x y = -max (-x) (-y)
[REAL_MIN_REFL] Theorem
⊢ ∀x. min x x = x
[REAL_MIN_SUB] Theorem
⊢ ∀z x y. min (x − z) (y − z) = min x y − z
[REAL_MUL] Theorem
⊢ ∀m n. &m * &n = &(m * n)
[REAL_MUL_ASSOC] Theorem
⊢ ∀x y z. x * (y * z) = x * y * z
[REAL_MUL_COMM] Theorem
⊢ ∀x y. x * y = y * x
[REAL_MUL_LID] Theorem
⊢ ∀x. 1 * x = x
[REAL_MUL_LINV] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ * x = 1
[REAL_MUL_LNEG] Theorem
⊢ ∀x y. -x * y = -(x * y)
[REAL_MUL_LZERO] Theorem
⊢ ∀x. 0 * x = 0
[REAL_MUL_RID] Theorem
⊢ ∀x. x * 1 = x
[REAL_MUL_RINV] Theorem
⊢ ∀x. x ≠ 0 ⇒ x * x⁻¹ = 1
[REAL_MUL_RNEG] Theorem
⊢ ∀x y. x * -y = -(x * y)
[REAL_MUL_RZERO] Theorem
⊢ ∀x. x * 0 = 0
[REAL_MUL_SIGN] Theorem
⊢ (∀x y. 0 ≤ x * y ⇔ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0) ∧
∀x y. x * y ≤ 0 ⇔ 0 ≤ x ∧ y ≤ 0 ∨ x ≤ 0 ∧ 0 ≤ y
[REAL_MUL_SUB1_CANCEL] Theorem
⊢ ∀z x y. y * x + y * (z − x) = y * z
[REAL_MUL_SUB2_CANCEL] Theorem
⊢ ∀z x y. x * y + (z − x) * y = z * y
[REAL_MUL_SYM] Theorem
⊢ ∀x y. x * y = y * x
[REAL_NEGNEG] Theorem
⊢ ∀x. --x = x
[REAL_NEG_0] Theorem
⊢ -0 = 0
[REAL_NEG_ADD] Theorem
⊢ ∀x y. -(x + y) = -x + -y
[REAL_NEG_EQ] Theorem
⊢ ∀x y. -x = y ⇔ x = -y
[REAL_NEG_EQ0] Theorem
⊢ ∀x. -x = 0 ⇔ x = 0
[REAL_NEG_GE0] Theorem
⊢ ∀x. 0 ≤ -x ⇔ x ≤ 0
[REAL_NEG_GT0] Theorem
⊢ ∀x. 0 < -x ⇔ x < 0
[REAL_NEG_HALF] Theorem
⊢ ∀x. x − x / 2 = x / 2
[REAL_NEG_INV] Theorem
⊢ ∀x. x ≠ 0 ⇒ -x⁻¹ = (-x)⁻¹
[REAL_NEG_INV'] Theorem
⊢ -x⁻¹ = (-x)⁻¹
[REAL_NEG_LE0] Theorem
⊢ ∀x. -x ≤ 0 ⇔ 0 ≤ x
[REAL_NEG_LMUL] Theorem
⊢ ∀x y. -(x * y) = -x * y
[REAL_NEG_LT0] Theorem
⊢ ∀x. -x < 0 ⇔ 0 < x
[REAL_NEG_MINUS1] Theorem
⊢ ∀x. -x = -1 * x
[REAL_NEG_MUL2] Theorem
⊢ ∀x y. -x * -y = x * y
[REAL_NEG_NEG] Theorem
⊢ ∀x. --x = x
[REAL_NEG_RMUL] Theorem
⊢ ∀x y. -(x * y) = x * -y
[REAL_NEG_SUB] Theorem
⊢ ∀x y. -(x − y) = y − x
[REAL_NEG_THIRD] Theorem
⊢ ∀x. x − x / 3 = 2 * x / 3
[REAL_NOT_LE] Theorem
⊢ ∀x y. ¬(x ≤ y) ⇔ y < x
[REAL_NOT_LT] Theorem
⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
[REAL_NZ_IMP_LT] Theorem
⊢ ∀n. n ≠ 0 ⇒ 0 < &n
[REAL_OF_NUM_ADD] Theorem
⊢ ∀m n. &m + &n = &(m + n)
[REAL_OF_NUM_EQ] Theorem
⊢ ∀m n. &m = &n ⇔ m = n
[REAL_OF_NUM_LE] Theorem
⊢ ∀m n. &m ≤ &n ⇔ m ≤ n
[REAL_OF_NUM_LT] Theorem
⊢ ∀m n. &m < &n ⇔ m < n
[REAL_OF_NUM_MUL] Theorem
⊢ ∀m n. &m * &n = &(m * n)
[REAL_OF_NUM_POW] Theorem
⊢ ∀x n. &x pow n = &(x ** n)
[REAL_OF_NUM_SUC] Theorem
⊢ ∀n. &n + 1 = &SUC n
[REAL_OVER1] Theorem
⊢ ∀x. x / 1 = x
[REAL_POS] Theorem
⊢ ∀n. 0 ≤ &n
[REAL_POSSQ] Theorem
⊢ ∀x. 0 < x * x ⇔ x ≠ 0
[REAL_POS_EQ_ZERO] Theorem
⊢ ∀x. pos x = 0 ⇔ x ≤ 0
[REAL_POS_ID] Theorem
⊢ ∀x. 0 ≤ x ⇒ pos x = x
[REAL_POS_INFLATE] Theorem
⊢ ∀x. x ≤ pos x
[REAL_POS_LE_ZERO] Theorem
⊢ ∀x. pos x ≤ 0 ⇔ x ≤ 0
[REAL_POS_LT] Theorem
⊢ ∀n. 0 < &SUC n
[REAL_POS_MONO] Theorem
⊢ ∀x y. x ≤ y ⇒ pos x ≤ pos y
[REAL_POS_NZ] Theorem
⊢ ∀x. 0 < x ⇒ x ≠ 0
[REAL_POS_POS] Theorem
⊢ ∀x. 0 ≤ pos x
[REAL_POW] Theorem
⊢ ∀m n. &m pow n = &(m ** n)
[REAL_POW2_ABS] Theorem
⊢ ∀x. (abs x)² = x²
[REAL_POW_1_LE] Theorem
⊢ ∀n x. 0 ≤ x ∧ x ≤ 1 ⇒ x pow n ≤ 1
[REAL_POW_ADD] Theorem
⊢ ∀x m n. x pow (m + n) = x pow m * x pow n
[REAL_POW_ANTIMONO] Theorem
⊢ ∀m n x. 0 < x ∧ x ≤ 1 ∧ m ≤ n ⇒ x pow n ≤ x pow m
[REAL_POW_ANTIMONO_LT] Theorem
⊢ ∀m n x. 0 < x ∧ x < 1 ∧ m < n ⇒ x pow n < x pow m
[REAL_POW_DIV] Theorem
⊢ ∀x y n. (x / y) pow n = x pow n / y pow n
[REAL_POW_EQ_0] Theorem
⊢ ∀x n. x pow n = 0 ⇔ x = 0 ∧ n ≠ 0
[REAL_POW_GE0] Theorem
⊢ 0 ≤ x pow n ⇔ 0 ≤ x ∨ EVEN n
[REAL_POW_INV] Theorem
⊢ ∀x n. x⁻¹ pow n = (x pow n)⁻¹
[REAL_POW_LBOUND] Theorem
⊢ ∀x n. 0 ≤ x ⇒ 1 + &n * x ≤ (1 + x) pow n
[REAL_POW_LE] Theorem
⊢ ∀x n. 0 ≤ x ⇒ 0 ≤ x pow n
[REAL_POW_LE0] Theorem
⊢ x pow n ≤ 0 ⇔ 0 < n ∧ x = 0 ∨ x < 0 ∧ ODD n
[REAL_POW_LE_1] Theorem
⊢ ∀n x. 1 ≤ x ⇒ 1 ≤ x pow n
[REAL_POW_LT] Theorem
⊢ ∀x n. 0 < x ⇒ 0 < x pow n
[REAL_POW_LT2] Theorem
⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n
[REAL_POW_MONO] Theorem
⊢ ∀m n x. 1 ≤ x ∧ m ≤ n ⇒ x pow m ≤ x pow n
[REAL_POW_MONO_LT] Theorem
⊢ ∀m n x. 1 < x ∧ m < n ⇒ x pow m < x pow n
[REAL_POW_NEG] Theorem
⊢ x pow n < 0 ⇔ ODD n ∧ x < 0
[REAL_POW_NEG2] Theorem
⊢ ∀x n. -x pow n = if EVEN n then x pow n else -(x pow n)
[REAL_POW_POS] Theorem
⊢ 0 < x pow n ⇔ n = 0 ∨ 0 < x ∨ x < 0 ∧ EVEN n
[REAL_POW_POW] Theorem
⊢ ∀x m n. (x pow m) pow n = x pow (m * n)
[REAL_RDISTRIB] Theorem
⊢ ∀x y z. (x + y) * z = x * z + y * z
[REAL_RINV_UNIQ] Theorem
⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹
[REAL_RNEG_UNIQ] Theorem
⊢ ∀x y. x + y = 0 ⇔ y = -x
[REAL_SGN] Theorem
⊢ ∀x. sgn x = x / abs x
[REAL_SGNS_EQ] Theorem
⊢ ∀x y.
sgn x = sgn y ⇔
(x = 0 ⇔ y = 0) ∧ (x > 0 ⇔ y > 0) ∧ (x < 0 ⇔ y < 0)
[REAL_SGNS_EQ_ALT] Theorem
⊢ ∀x y.
sgn x = sgn y ⇔
(x = 0 ⇒ y = 0) ∧ (x > 0 ⇒ y > 0) ∧ (x < 0 ⇒ y < 0)
[REAL_SGN_0] Theorem
⊢ sgn 0 = 0
[REAL_SGN_ABS] Theorem
⊢ ∀x. sgn x * abs x = x
[REAL_SGN_ABS_ALT] Theorem
⊢ ∀x. sgn x * x = abs x
[REAL_SGN_CASES] Theorem
⊢ ∀x. sgn x = 0 ∨ sgn x = 1 ∨ sgn x = -1
[REAL_SGN_DIV] Theorem
⊢ ∀x y. sgn (x / y) = sgn x / sgn y
[REAL_SGN_EQ] Theorem
⊢ (∀x. sgn x = 0 ⇔ x = 0) ∧ (∀x. sgn x = 1 ⇔ x > 0) ∧
∀x. sgn x = -1 ⇔ x < 0
[REAL_SGN_EQ_INEQ] Theorem
⊢ ∀x y. sgn x = sgn y ⇔ x = y ∨ abs (x − y) < max (abs x) (abs y)
[REAL_SGN_INEQS] Theorem
⊢ (∀x. 0 ≤ sgn x ⇔ 0 ≤ x) ∧ (∀x. 0 < sgn x ⇔ 0 < x) ∧
(∀x. 0 ≥ sgn x ⇔ 0 ≥ x) ∧ (∀x. 0 > sgn x ⇔ 0 > x) ∧
(∀x. 0 = sgn x ⇔ 0 = x) ∧ (∀x. sgn x ≤ 0 ⇔ x ≤ 0) ∧
(∀x. sgn x < 0 ⇔ x < 0) ∧ (∀x. sgn x ≥ 0 ⇔ x ≥ 0) ∧
(∀x. sgn x > 0 ⇔ x > 0) ∧ ∀x. sgn x = 0 ⇔ x = 0
[REAL_SGN_INV] Theorem
⊢ ∀x. sgn x⁻¹ = sgn x
[REAL_SGN_MUL] Theorem
⊢ ∀x y. sgn (x * y) = sgn x * sgn y
[REAL_SGN_NEG] Theorem
⊢ ∀x. sgn (-x) = -sgn x
[REAL_SGN_POW] Theorem
⊢ ∀x n. sgn (x pow n) = sgn x pow n
[REAL_SGN_POW_2] Theorem
⊢ ∀x. sgn x² = sgn (abs x)
[REAL_SGN_REAL_SGN] Theorem
⊢ ∀x. sgn (sgn x) = sgn x
[REAL_SUB] Theorem
⊢ ∀m n. &m − &n = if m − n = 0 then -&(n − m) else &(m − n)
[REAL_SUB_0] Theorem
⊢ ∀x y. x − y = 0 ⇔ x = y
[REAL_SUB_ABS] Theorem
⊢ ∀x y. abs x − abs y ≤ abs (x − y)
[REAL_SUB_ADD] Theorem
⊢ ∀x y. x − y + y = x
[REAL_SUB_ADD2] Theorem
⊢ ∀x y. y + (x − y) = x
[REAL_SUB_INV2] Theorem
⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ x⁻¹ − y⁻¹ = (y − x) / (x * y)
[REAL_SUB_LDISTRIB] Theorem
⊢ ∀x y z. x * (y − z) = x * y − x * z
[REAL_SUB_LE] Theorem
⊢ ∀x y. 0 ≤ x − y ⇔ y ≤ x
[REAL_SUB_LNEG] Theorem
⊢ ∀x y. -x − y = -(x + y)
[REAL_SUB_LT] Theorem
⊢ ∀x y. 0 < x − y ⇔ y < x
[REAL_SUB_LZERO] Theorem
⊢ ∀x. 0 − x = -x
[REAL_SUB_NEG2] Theorem
⊢ ∀x y. -x − -y = y − x
[REAL_SUB_RAT] Theorem
⊢ ∀a b c d. b ≠ 0 ∧ d ≠ 0 ⇒ a / b − c / d = (a * d − b * c) / (b * d)
[REAL_SUB_RDISTRIB] Theorem
⊢ ∀x y z. (x − y) * z = x * z − y * z
[REAL_SUB_REFL] Theorem
⊢ ∀x. x − x = 0
[REAL_SUB_RNEG] Theorem
⊢ ∀x y. x − -y = x + y
[REAL_SUB_RZERO] Theorem
⊢ ∀x. x − 0 = x
[REAL_SUB_SUB] Theorem
⊢ ∀x y. x − y − x = -y
[REAL_SUB_SUB2] Theorem
⊢ ∀x y. x − (x − y) = y
[REAL_SUB_TRIANGLE] Theorem
⊢ ∀a b c. a − b + (b − c) = a − c
[REAL_SUMSQ] Theorem
⊢ ∀x y. x * x + y * y = 0 ⇔ x = 0 ∧ y = 0
[REAL_SUP] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < sup P
[REAL_SUP_ALLPOS] Theorem
⊢ ∀P. (∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
[REAL_SUP_CONST] Theorem
⊢ ∀x. sup (λr. r = x) = x
[REAL_SUP_EXISTS] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
[REAL_SUP_EXISTS_UNIQUE] Theorem
⊢ ∀p. (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒
∃!s. ∀y. (∃x. p x ∧ y < x) ⇔ y < s
[REAL_SUP_LE] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < sup P
[REAL_SUP_MAX] Theorem
⊢ ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ sup p = z
[REAL_SUP_SOMEPOS] Theorem
⊢ ∀P. (∃x. P x ∧ 0 < x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
[REAL_SUP_UBOUND] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. P y ⇒ y ≤ sup P
[REAL_SUP_UBOUND_LE] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. P y ⇒ y ≤ sup P
[REAL_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
[SETOK_LE_LT] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇔
(∃x. P x) ∧ ∃z. ∀x. P x ⇒ x < z
[SIMP_REAL_ARCH] Theorem
⊢ ∀x. ∃n. x ≤ &n
[SIMP_REAL_ARCH_NEG] Theorem
⊢ ∀x. ∃n. -&n ≤ x
[SQRT_0] Theorem
⊢ sqrt 0 = 0
[SQRT_1] Theorem
⊢ sqrt 1 = 1
[SQRT_DIV] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (x / y) = sqrt x / sqrt y
[SQRT_EQ] Theorem
⊢ ∀x y. x² = y ∧ 0 ≤ x ⇒ x = sqrt y
[SQRT_INV] Theorem
⊢ ∀x. 0 ≤ x ⇒ sqrt x⁻¹ = (sqrt x)⁻¹
[SQRT_MONO_LE] Theorem
⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
[SQRT_MONO_LT] 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_POS_UNIQ] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ∧ y² = x ⇒ sqrt x = y
[SQRT_POW2] Theorem
⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x
[SQRT_POW_2] Theorem
⊢ ∀x. 0 ≤ x ⇒ (sqrt x)² = x
[SUB_POW_2] Theorem
⊢ ∀x y. (x − y)² = x² + y² − 2 * x * y
[SUM_0] Theorem
⊢ ∀m n. sum (m,n) (λr. 0) = 0
[SUM_1] Theorem
⊢ ∀f n. sum (n,1) f = f n
[SUM_2] Theorem
⊢ ∀f n. sum (n,2) f = f n + f (n + 1)
[SUM_ABS] Theorem
⊢ ∀f m n. abs (sum (m,n) (λm. abs (f m))) = sum (m,n) (λm. abs (f m))
[SUM_ABS_LE] Theorem
⊢ ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))
[SUM_ADD] Theorem
⊢ ∀f g m n. sum (m,n) (λn. f n + g n) = sum (m,n) f + sum (m,n) g
[SUM_BOUND] Theorem
⊢ ∀f k m n. (∀p. m ≤ p ∧ p < m + n ⇒ f p ≤ k) ⇒ sum (m,n) f ≤ &n * k
[SUM_CANCEL] Theorem
⊢ ∀f n d. sum (n,d) (λn. f (SUC n) − f n) = f (n + d) − f n
[SUM_CMUL] Theorem
⊢ ∀f c m n. sum (m,n) (λn. c * f n) = c * sum (m,n) f
[SUM_DIFF] Theorem
⊢ ∀f m n. sum (m,n) f = sum (0,m + n) f − sum (0,m) f
[SUM_DIFFS] Theorem
⊢ ∀d m n. sum (m,n) (λi. d (SUC i) − d i) = d (m + n) − d m
[SUM_EQ] Theorem
⊢ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r = g r) ⇒ sum (m,n) f = sum (m,n) g
[SUM_EQ_0] Theorem
⊢ (∀r. m ≤ r ∧ r < m + n ⇒ f r = 0) ⇒ sum (m,n) f = 0
[SUM_GROUP] Theorem
⊢ ∀n k f. sum (0,n) (λm. sum (m * k,k) f) = sum (0,n * k) f
[SUM_LE] Theorem
⊢ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r ≤ g r) ⇒ sum (m,n) f ≤ sum (m,n) g
[SUM_LT] Theorem
⊢ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r < g r) ∧ 0 < n ⇒
sum (m,n) f < sum (m,n) g
[SUM_NEG] Theorem
⊢ ∀f n d. sum (n,d) (λn. -f n) = -sum (n,d) f
[SUM_NSUB] Theorem
⊢ ∀n f c. sum (0,n) f − &n * c = sum (0,n) (λp. f p − c)
[SUM_OFFSET] Theorem
⊢ ∀f n k. sum (0,n) (λm. f (m + k)) = sum (0,n + k) f − sum (0,k) f
[SUM_PERMUTE_0] Theorem
⊢ ∀n p.
(∀y. y < n ⇒ ∃!x. x < n ∧ p x = y) ⇒
∀f. sum (0,n) (λn. f (p n)) = sum (0,n) f
[SUM_PICK] Theorem
⊢ ∀n k x.
sum (0,n) (λm. if m = k then x else 0) = if k < n then x else 0
[SUM_POS] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ⇒ ∀m n. 0 ≤ sum (m,n) f
[SUM_POS_GEN] Theorem
⊢ ∀f m. (∀n. m ≤ n ⇒ 0 ≤ f n) ⇒ ∀n. 0 ≤ sum (m,n) f
[SUM_REINDEX] Theorem
⊢ ∀f m k n. sum (m + k,n) f = sum (m,n) (λr. f (r + k))
[SUM_SPLIT] Theorem
⊢ ∀f m n p. sum (m,n) f + sum (m + n,p) f = sum (m,n + p) f
[SUM_SUB] Theorem
⊢ ∀f g m n. sum (m,n) (λn. f n − g n) = sum (m,n) f − sum (m,n) g
[SUM_SUBST] Theorem
⊢ ∀f g m n.
(∀p. m ≤ p ∧ p < m + n ⇒ f p = g p) ⇒ sum (m,n) f = sum (m,n) g
[SUM_TWO] Theorem
⊢ ∀f n p. sum (0,n) f + sum (n,p) f = sum (0,n + p) f
[SUM_ZERO] Theorem
⊢ ∀f N. (∀n. n ≥ N ⇒ f n = 0) ⇒ ∀m n. m ≥ N ⇒ sum (m,n) f = 0
[SUP_EPSILON] Theorem
⊢ ∀p e.
0 < e ∧ (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒
∃x. p x ∧ sup p ≤ x + e
[SUP_LEMMA1] Theorem
⊢ ∀P s d.
(∀y. (∃x. (λx. P (x + d)) x ∧ y < x) ⇔ y < s) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < s + d
[SUP_LEMMA2] Theorem
⊢ ∀P. (∃x. P x) ⇒ ∃d x. (λx. P (x + d)) x ∧ 0 < x
[SUP_LEMMA3] Theorem
⊢ ∀d. (∃z. ∀x. P x ⇒ x < z) ⇒ ∃z. ∀x. (λx. P (x + d)) x ⇒ x < z
[SUP_LT_EPSILON] Theorem
⊢ ∀p e.
0 < e ∧ (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒
∃x. p x ∧ sup p < x + e
[X_HALF_HALF] Theorem
⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x
[ZERO_LT_POW] Theorem
⊢ (0 < x pow NUMERAL (BIT2 n) ⇔ x ≠ 0) ∧
(0 < x pow NUMERAL (BIT1 n) ⇔ 0 < x)
[ZERO_LT_invx] Theorem
⊢ 0 < x⁻¹ pow n ⇔ 0 < x pow n
[abs] Theorem
⊢ ∀x. abs x = if 0 ≤ x then x else -x
[add_ints] Theorem
⊢ &n + &m = &(n + m) ∧
-&n + &m = (if n ≤ m then &(m − n) else -&(n − m)) ∧
&n + -&m = (if n < m then -&(m − n) else &(n − m)) ∧
-&n + -&m = -&(n + m)
[add_rat] Theorem
⊢ x / y + u / v =
if y = 0 then unint (x / y) + u / v
else if v = 0 then x / y + unint (u / v)
else if y = v then (x + u) / v
else (x * v + u * y) / (y * v)
[add_ratl] Theorem
⊢ x / y + z = if y = 0 then unint (x / y) + z else (x + z * y) / y
[add_ratr] Theorem
⊢ x + y / z = if z = 0 then x + unint (y / z) else (x * z + y) / z
[div_rat] Theorem
⊢ x / y / (u / v) =
if u = 0 ∨ v = 0 then x / y / unint (u / v)
else if y = 0 then unint (x / y) / (u / v)
else x * v / (y * u)
[div_ratl] Theorem
⊢ x / y / z =
if y = 0 then unint (x / y) / z
else if z = 0 then unint (x / y / z)
else x / (y * z)
[div_ratr] Theorem
⊢ x / (y / z) = x * z / y
[eq_ints] Theorem
⊢ (&n = &m ⇔ n = m) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0) ∧
(&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = -&m ⇔ n = m)
[eq_rat] Theorem
⊢ x / y = u / v ⇔
if y = 0 then u = 0 ∨ v = 0
else if v = 0 then x = 0
else if y = v then x = u
else x * v = y * u
[eq_ratl] Theorem
⊢ x / y = z ⇔ if y = 0 then unint (x / y) = z else x = y * z
[eq_ratr] Theorem
⊢ z = x / y ⇔ if y = 0 then z = unint (x / y) else y * z = x
[le_int] Theorem
⊢ (&n ≤ &m ⇔ n ≤ m) ∧ (-&n ≤ &m ⇔ T) ∧ (&n ≤ -&m ⇔ n = 0 ∧ m = 0) ∧
(-&n ≤ -&m ⇔ m ≤ n)
[le_rat] Theorem
⊢ x / &n ≤ u / &m ⇔
if n = 0 then unint (x / 0) ≤ u / &m
else if m = 0 then x / &n ≤ unint (u / 0)
else &m * x ≤ &n * u
[le_ratl] Theorem
⊢ x / &n ≤ u ⇔ if n = 0 then unint (x / 0) ≤ u else x ≤ &n * u
[le_ratr] Theorem
⊢ x ≤ u / &m ⇔ if m = 0 then x ≤ unint (u / 0) else &m * x ≤ u
[lt_int] Theorem
⊢ (&n < &m ⇔ n < m) ∧ (-&n < &m ⇔ n ≠ 0 ∨ m ≠ 0) ∧ (&n < -&m ⇔ F) ∧
(-&n < -&m ⇔ m < n)
[lt_rat] Theorem
⊢ x / &n < u / &m ⇔
if n = 0 then unint (x / 0) < u / &m
else if m = 0 then x / &n < unint (u / 0)
else &m * x < &n * u
[lt_ratl] Theorem
⊢ x / &n < u ⇔ if n = 0 then unint (x / 0) < u else x < &n * u
[lt_ratr] Theorem
⊢ x < u / &m ⇔ if m = 0 then x < unint (u / 0) else &m * x < u
[max_def] Theorem
⊢ ∀x y. max x y = if x ≤ y then y else x
[min_def] Theorem
⊢ ∀x y. min x y = if x ≤ y then x else y
[mult_ints] Theorem
⊢ &a * &b = &(a * b) ∧ -&a * &b = -&(a * b) ∧ &a * -&b = -&(a * b) ∧
-&a * -&b = &(a * b)
[mult_rat] Theorem
⊢ x / y * (u / v) =
if y = 0 then unint (x / y) * (u / v)
else if v = 0 then x / y * unint (u / v)
else x * u / (y * v)
[mult_ratl] Theorem
⊢ x / y * z = if y = 0 then unint (x / y) * z else x * z / y
[mult_ratr] Theorem
⊢ x * (y / z) = if z = 0 then x * unint (y / z) else x * y / z
[neg_rat] Theorem
⊢ -(x / y) = -x / y ∧ x / -y = -x / y
[nonzerop_0] Theorem
⊢ NZ 0 = 0
[nonzerop_EQ0] Theorem
⊢ NZ r = 0 ⇔ r = 0
[nonzerop_EQ1_I] Theorem
⊢ r ≠ 0 ⇒ NZ r = 1
[nonzerop_NUMERAL] Theorem
⊢ NZ (&NUMERAL (BIT1 n)) = 1 ∧ NZ (&NUMERAL (BIT2 n)) = 1
[nonzerop_inv] Theorem
⊢ NZ x⁻¹ = NZ x
[nonzerop_mulXX] Theorem
⊢ NZ r * NZ r = NZ r
[nonzerop_mult] Theorem
⊢ NZ (x * y) = NZ x * NZ y
[nonzerop_nonzero_pow] Theorem
⊢ 0 < n ⇒ NZ x pow n = NZ x
[nonzerop_nonzerop] Theorem
⊢ NZ (NZ x) = NZ x
[nonzerop_pow] Theorem
⊢ NZ (x pow n) = NZ x pow n
[pow] Theorem
⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n
[pow0] Theorem
⊢ ∀x. x pow 0 = 1
[pow_eq0] Theorem
⊢ x pow y = 0 ⇔ x = 0 ∧ 0 < y
[pow_inv_eq] Theorem
⊢ x pow m * x⁻¹ pow m = NZ x pow m
[pow_inv_mul] Theorem
⊢ 0 < n ⇒ x pow n * x⁻¹ = x pow (n − 1) * NZ x
[pow_inv_mul_invlt] Theorem
⊢ ∀x m n. n < m ⇒ x pow m * x⁻¹ pow n = x pow (m − n)
[pow_inv_mul_powlt] Theorem
⊢ ∀x m n. m < n ⇒ x pow m * x⁻¹ pow n = x⁻¹ pow (n − m)
[pow_rat] Theorem
⊢ x pow 0 = 1 ∧ 0 pow NUMERAL (BIT1 n) = 0 ∧
0 pow NUMERAL (BIT2 n) = 0 ∧
&NUMERAL a pow NUMERAL n = &(NUMERAL a ** NUMERAL n) ∧
-&NUMERAL a pow NUMERAL n =
(if ODD (NUMERAL n) then numeric_negate else (λx. x))
(&(NUMERAL a ** NUMERAL n)) ∧ (x / y) pow n = x pow n / y pow n
[real_div] Theorem
⊢ ∀x y. x / y = x * y⁻¹
[real_ge] Theorem
⊢ ∀x y. x ≥ y ⇔ y ≤ x
[real_gt] Theorem
⊢ ∀x y. x > y ⇔ y < x
[real_lt] Theorem
⊢ ∀y x. x < y ⇔ ¬(y ≤ x)
[real_lte] Theorem
⊢ ∀x y. x ≤ y ⇔ ¬(y < x)
[real_of_num] Theorem
⊢ 0 = real_0 ∧ ∀n. &SUC n = &n + real_1
[real_sub] Theorem
⊢ ∀x y. x − y = x + -y
[sum] Theorem
⊢ (∀n f. sum (n,0) f = 0) ∧
∀n m f. sum (n,SUC m) f = sum (n,m) f + f (n + m)
[sum_compute] Theorem
⊢ (∀n f. sum (n,0) f = 0) ∧
(∀n m f.
sum (n,NUMERAL (BIT1 m)) f =
sum (n,NUMERAL (BIT1 m) − 1) f + f (n + (NUMERAL (BIT1 m) − 1))) ∧
∀n m f.
sum (n,NUMERAL (BIT2 m)) f =
sum (n,NUMERAL (BIT1 m)) f + f (n + NUMERAL (BIT1 m))
[sum_ind] Theorem
⊢ ∀P. (∀n f. P (n,0) f) ∧ (∀n m f. P (n,m) f ⇒ P (n,SUC m) f) ⇒
∀v v1 v2. P (v,v1) v2
*)
end
HOL 4, Trindemossen-1