environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, NAT_1, RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, REALSET1, XXREAL_0, CARD_3, COMPLEX1, SEQ_2, ORDINAL2, RSSPACE, ASYMPT_1, FUNCSDOM, FINSET_1, POWER, ORDINAL4, FUNCOP_1, VECTSP_1, PARTFUN3, PRE_TOPC, FINSEQ_1, MESFUNC1, ASYMPT_2, ASYMPT_3, ASYMPT_0, ORDINAL1, INT_1, AFINSQ_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, INT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, POWER, SERIES_1, ASYMPT_0, ASYMPT_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_1, RLVECT_1, VECTSP_1, FUNCSDOM, RSSPACE, ASYMPT_2;
definitions TARSKI, XBOOLE_0, FUNCT_2, ALGSTR_0, RLVECT_1, VECTSP_1;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQ_2, ABSVALUE, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XREAL_0, AFINSQ_1, AFINSQ_2, INT_1, ASYMPT_0, ASYMPT_1, POWER, FUNCSDOM, PRE_FF, TAYLOR_1, RLVECT_1, VECTSP_1, REALSET1, ZFMISC_1, ASYMPT_2, PARTFUN3, GROUP_1;
schemes NAT_1, SEQ_1, XBOOLE_0;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0, FUNCSDOM, RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_1, FUNCT_2, AFINSQ_1, AFINSQ_2, XBOOLE_0, SUBSET_1, RELAT_1, INT_1, ASYMPT_0, POWER, ASYMPT_1, RSSPACE, PARTFUN3, REALSET1, NEWTON, COMPLEX1;
constructors HIDDEN, REAL_1, SEQ_2, SERIES_1, REALSET1, RLSUB_1, RELSET_1, COMSEQ_2, SEQ_1, FUNCSDOM, INTEGRA2, XXREAL_2, RECDEF_1, FCONT_1, PREPOWER, ASYMPT_0, ASYMPT_1, PARTFUN3, AFINSQ_2, FUNCT_4, PARTFUN2, RSSPACE4, PROB_1, NEWTON, VALUED_2, ASYMPT_2, GROUP_1, RVSUM_1, RFINSEQ2, METRIC_1, MATRPROB;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities REALSET1, STRUCT_0, ALGSTR_0, FUNCSDOM, BINOP_1, RLVECT_1, ORDINAL1, ASYMPT_0;
expansions TARSKI, RLVECT_1, FUNCT_1, PARTFUN3, GROUP_1, FUNCSDOM, STRUCT_0, VECTSP_1, ASYMPT_2;
theorem LMC31:
for
r being
Real ex
N being
Nat st
for
n being
Nat st
N <= n holds
r < n / (log (2,n))
reconsider rr = 0 as Element of REAL by XREAL_0:def 1;