environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, NAT_1, XXREAL_0, POWER, ARYTM_3, RELAT_1, CARD_1, SQUARE_1, SEQ_1, FUNCT_1, ARYTM_1, ASYMPT_0, FUNCT_2, INT_1, VALUED_1, TARSKI, SEQ_2, ORDINAL2, COMPLEX1, CARD_3, SERIES_1, REALSET1, VALUED_0, NEWTON, FINSEQ_1, FINSEQ_2, ORDINAL4, XBOOLE_0, ASYMPT_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, FUNCT_2, FUNCT_7, SQUARE_1, INT_1, NAT_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, NEWTON, POWER, SERIES_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RVSUM_1, ASYMPT_0;
definitions ASYMPT_0;
theorems TARSKI, FUNCT_2, INT_1, NAT_1, SEQ_1, SQUARE_1, SEQ_2, ABSVALUE, FUNCOP_1, POWER, NEWTON, EULER_2, SERIES_1, FINSEQ_1, PRE_FF, RVSUM_1, FINSEQ_2, ASYMPT_0, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, VALUED_1;
schemes FUNCT_2, SEQ_1, NAT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, ASYMPT_0, SQUARE_1, VALUED_0, VALUED_1, FUNCT_2, POWER, FINSEQ_1;
constructors HIDDEN, PARTFUN1, DOMAIN_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3, RVSUM_1, NEWTON, PREPOWER, SERIES_1, ASYMPT_0, RELSET_1, FUNCOP_1, BINOP_2, COMSEQ_2, FUNCT_7, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ASYMPT_0, SQUARE_1, VALUED_1, XCMPLX_0, SEQ_1;
expansions ASYMPT_0, VALUED_1;
Lm1:
for n being Nat st n >= 2 holds
2 to_power n > n + 1
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;
Lm2:
for a being logbase Real
for f being Real_Sequence st a > 1 & ( for n being Element of NAT st n > 0 holds
f . n = log (a,n) ) holds
f is eventually-positive
Lm3:
for a, b, c being Real st a > 0 & c > 0 & c <> 1 holds
a to_power b = c to_power (b * (log (c,a)))
Lm4:
for f, g being Real_Sequence
for n being Nat holds (f /" g) . n = (f . n) / (g . n)
Lm5:
for f, g being eventually-nonnegative Real_Sequence holds
( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g )
Lm6:
for a, b, c being Real st 0 < a & a <= b & c >= 0 holds
a to_power c <= b to_power c
Lm7:
for n being Nat st n >= 4 holds
(2 * n) + 3 < 2 to_power n
Lm8:
for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n
Lm9:
for c being Real st c > 6 holds
c ^2 < 2 to_power c
Lm10:
for e being positive Real
for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) holds
( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
Lm11:
for e being Real st e > 0 holds
( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 )
Lm12:
for f being Real_Sequence
for N being Element of NAT st ( for n being Element of NAT st n <= N holds
f . n >= 0 ) holds
Sum (f,N) >= 0
Lm13:
for f, g being Real_Sequence
for N being Element of NAT st ( for n being Element of NAT st n <= N holds
f . n <= g . n ) holds
Sum (f,N) <= Sum (g,N)
Lm14:
for f being Real_Sequence
for b being Real st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for N being Element of NAT holds Sum (f,N) = b * N
Lm15:
for f being Real_Sequence
for N, M being Nat holds (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M)
Lm16:
for f, g being Real_Sequence
for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds
f . n <= g . n ) holds
Sum (f,N,M) <= Sum (g,N,M)
Lm17:
for n being Element of NAT holds [/(n / 2)\] <= n
Lm18:
for f being Real_Sequence
for b being Real
for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for M being Element of NAT holds Sum (f,N,M) = b * (N - M)
Lm19:
for a, b, c being Real st a > 1 & b >= a & c >= 1 holds
log (a,c) >= log (b,c)
Lm21:
for n being Element of NAT holds ((n ^2) - n) + 1 > 0
Lm22:
for f, g being Real_Sequence
for N being Element of NAT
for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds
f . n = g . n ) holds
( g is convergent & lim g = c )
Lm23:
for n being Element of NAT st n >= 1 holds
((n ^2) - n) + 1 <= n ^2
Lm24:
for n being Element of NAT st n >= 1 holds
n ^2 <= 2 * (((n ^2) - n) + 1)
Lm25:
for e being Real st 0 < e & e < 1 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))
Lm26:
2 to_power 12 = 4096
Lm27:
for n being Nat st n >= 3 holds
n ^2 > (2 * n) + 1
Lm28:
for n being Element of NAT st n >= 10 holds
2 to_power (n - 1) > (2 * n) ^2
Lm29:
for n being Nat st n >= 9 holds
(n + 1) to_power 6 < 2 * (n to_power 6)
Lm30:
for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6
Lm31:
for x being Real st x > 9 holds
2 to_power x > (2 * x) ^2
Lm32:
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(sqrt n) - (log (2,n)) > 1
Lm33:
5 ! = 120
Lm34:
for n being Element of NAT st n >= 10 holds
(2 to_power (2 * n)) / (n !) < 1 / (2 to_power (n - 9))
Lm35:
for n being Element of NAT st n >= 3 holds
2 * (n - 2) >= n - 1
Lm36:
5 to_power 5 = 3125
Lm37:
4 to_power 4 = 256
Lm38:
for a, b, d, e being Real holds (a / b) / (d / e) = (a / d) * (e / b)
Lm39:
for x being Real st x >= 0 holds
sqrt x = x to_power (1 / 2)
Lm40:
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log (2,n))) > n / 2
Lm41:
for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
s is V48()
Lm42:
for n being Element of NAT st n >= 1 holds
((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)
Lm43:
for k, n being Element of NAT st k <= n holds
n choose k >= ((n + 1) choose k) / (n + 1)
Lm44:
for f being Real_Sequence st ( for n being Nat holds f . n = log (2,(n !)) ) holds
for n being Element of NAT holds f . n = Sum (seq_logn,n)
Lm45:
for n being Element of NAT st n >= 4 holds
n * (log (2,n)) >= 2 * n
Lm46:
for n being Element of NAT st n >= 2 holds
[/(n / 2)\] < n
Lm47:
for n being Element of NAT st n >= 2 holds
n ^2 > n + 1
Lm48:
for n being Element of NAT st n >= 1 holds
(2 to_power (n + 1)) - (2 to_power n) > 1
Lm49:
for n being Element of NAT st n >= 2 holds
not (2 to_power n) - 1 in POWEROF2SET
Lm50:
for n being Element of NAT st n >= 2 holds
n ! > 1
Lm51:
for n1, n being Element of NAT st n <= n1 holds
n ! <= n1 !
Lm52:
for k being Element of NAT st k >= 1 holds
ex n being Element of NAT st
( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds
m = n ) )
Lm53:
for n being Element of NAT st n >= 3 holds
n ! > n
Lm54:
(seq_n^ 1) - (seq_const 1) is eventually-positive