environ
vocabularies HIDDEN, NUMBERS, XXREAL_0, SUBSET_1, SEQ_1, COMPLEX1, SQUARE_1, NEWTON, RELAT_1, ARYTM_3, ARYTM_1, CARD_1, POWER, PREPOWER, FUNCT_1, SERIES_1, VALUED_1, NAT_1, REAL_1, SERIES_3, ABIAN, FUNCT_7;
notations HIDDEN, SUBSET_1, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NEWTON, REAL_1, NAT_1, PREPOWER, COMPLEX1, VALUED_1, SEQ_1, ABIAN, POWER, SERIES_1, FUNCT_2;
definitions ;
theorems XCMPLX_1, SQUARE_1, SIN_COS2, POLYEQ_2, ABSVALUE, NEWTON, POWER, ASYMPT_1, XREAL_1, PREPOWER, FUNCT_2, SERIES_1, SEQ_1, COMPLEX1, POLYEQ_1, XXREAL_0, ABIAN;
schemes NAT_1;
registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, COMPLEX1, NEWTON, VALUED_1, FUNCT_2, VALUED_0, RELSET_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, NEWTON, PREPOWER, SERIES_1, VALUED_1, PARTFUN1, RELSET_1, BINOP_2, ABIAN;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, XCMPLX_0;
expansions ;
Lm1:
for x being Real holds x ^2 = x |^ 2
Lm2:
2 |^ 3 = 8
Lm3:
3 |^ 3 = 27
Lm4:
for x being Real holds (- x) |^ 3 = - (x |^ 3)
Lm5:
for x, y being Real holds (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3)
Lm6:
for x, y being Real holds (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2))
Lm7:
for x, y, z being Real st x ^2 <= y * z holds
|.x.| <= sqrt (y * z)
theorem
for
x,
y,
z being
Real holds
((x + y) + z) ^2 >= 3
* (((x * y) + (y * z)) + (x * z))
theorem
for
x,
y,
z being
Real st
(x + y) + z = 1 holds
((x * y) + (y * z)) + (x * z) <= 1
/ 3
theorem Th18:
for
x,
y being
Real st
x + y = 1 holds
x * y <= 1
/ 4
Lm8:
for s being Real_Sequence st ( for n being Nat holds
( s . n > - 1 & s . n < 0 ) ) holds
for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
Lm9:
for s being Real_Sequence st ( for n being Nat holds s . n >= 0 ) holds
for n being Nat holds ((Partial_Sums s) . n) * (s . (n + 1)) >= 0
Lm10:
for n being Nat
for s, s1, s2 being Real_Sequence st ( for n being Nat holds s . n = ((s1 . n) + (s2 . n)) ^2 ) holds
(Partial_Sums s) . n >= 0
Lm11:
for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
(n + 1) -root ((Partial_Product s) . n) > 0
Lm12:
for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0