environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_1, SEQ_1, FINSEQ_1, RAT_1, ORDINAL4, POWER, INT_2, SQUARE_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, NAT_1, FUNCT_1, ARYTM_1, REALSET1, SEQ_2, ORDINAL2, COMPLEX1, VALUED_1, SERIES_1, CARD_3, XBOOLE_0, RFINSEQ, PARTFUN1, FINSEQ_2, NEWTON, SIN_COS, IRRAT_1, REAL_1, ASYMPT_1;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, INT_1, COMPLEX1, SQUARE_1, NAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, POWER, FINSEQ_1, RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, SIN_COS, RAT_1, INT_2, PEPIN, NEWTON;
definitions SEQ_2;
theorems SEQ_1, POWER, NEWTON, NAT_1, SEQ_2, SEQ_4, ABSVALUE, RVSUM_1, FINSEQ_2, SERIES_1, RFINSEQ, FINSEQ_3, FINSEQ_5, SIN_COS, SQUARE_1, INT_1, RAT_1, INT_2, FUNCT_2, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, NAT_D, PARTFUN1, CARD_1, VALUED_0, ORDINAL1, XREAL_0, TARSKI;
schemes SEQ_1, NAT_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, FINSEQ_1, SQUARE_1, RVSUM_1, SEQ_1, SEQ_2;
constructors HIDDEN, ARYTM_0, REAL_1, NAT_1, NAT_D, SEQ_2, PARTFUN1, RVSUM_1, LIMFUNC1, COMSEQ_3, RFINSEQ, BINARITH, SIN_COS, PEPIN, SERIES_1, POWER, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS, FUNCOP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SQUARE_1, XCMPLX_0;
expansions SEQ_2;
theorem Th4:
for
k,
n being
Nat st
n > 0 holds
n ^ (- (k + 1)) = (n ^ (- k)) / n
theorem Th11:
for
k being
Nat holds
(1 / (k + 1)) * (1 / (k !)) = 1
/ ((k + 1) !)
theorem Th38:
for
k,
n being
Nat for
x being
Real st
x = 1
/ (n + 1) holds
(n !) / (((n + k) + 1) !) <= x ^ (k + 1)
theorem Th40:
for
x,
n being
Real st
n >= 2 &
x = 1
/ (n + 1) holds
x / (1 - x) < 1