environ
vocabularies HIDDEN, NUMBERS, SEQ_1, NEWTON, ARYTM_3, RELAT_1, ARYTM_1, CARD_1, PREPOWER, XXREAL_0, FUNCT_1, SERIES_1, REALSET1, NAT_1, SERIES_3, REAL_1;
notations HIDDEN, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, SERIES_3, SEQ_1, NEWTON, PREPOWER, SERIES_1;
definitions ;
theorems SERIES_3, NAT_1, PREPOWER, NEWTON, XCMPLX_1, SERIES_1, XREAL_1, WSIERP_1;
schemes NAT_1;
registrations XCMPLX_0, XREAL_0, NAT_1, NEWTON, NUMBERS, VALUED_0, RELSET_1, FUNCT_2, ORDINAL1;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, BINOP_2, NEWTON, PREPOWER, SERIES_1, SERIES_3, VALUED_1, SUBSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities ;
expansions ;
Lm1:
for a, b being Real holds
( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
Lm2:
for n being Nat holds (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2
Lm3:
for n being Nat holds (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2
Lm4:
for a, b being Real holds (a - b) * (a + b) = (a |^ 2) - (b |^ 2)
Lm5:
for a, b being Real holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
Lm6:
for n being Nat
for a being Real st a <> 1 holds
((((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))) + (n * (a |^ (n + 1)))) + (a |^ (n + 1)) = ((a * (1 - (a |^ (n + 1)))) / ((1 - a) |^ 2)) - (((n + 1) * (a |^ (n + 2))) / (1 - a))
Lm7:
for n being Nat holds 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))
theorem Th1:
for
a,
b,
c being
Real holds
((a + b) + c) |^ 2
= (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + ((2 * a) * b)) + ((2 * a) * c)) + ((2 * b) * c)
theorem
for
a,
b,
c being
Real holds
((a - b) + c) |^ 2
= (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)
theorem
for
a,
b,
c being
Real holds
((a - b) - c) |^ 2
= (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) - ((2 * a) * c)) + ((2 * b) * c)
theorem
for
a,
b,
c,
d being
Real holds
(((a + b) + c) + d) |^ 2
= ((((((a |^ 2) + (b |^ 2)) + (c |^ 2)) + (d |^ 2)) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * a) * d))) + (((2 * b) * c) + ((2 * b) * d))) + ((2 * c) * d)
theorem
for
a,
b,
c being
Real holds
((a + b) + c) |^ 3
= ((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (((3 * (a |^ 2)) * b) + ((3 * (a |^ 2)) * c))) + (((3 * (b |^ 2)) * a) + ((3 * (b |^ 2)) * c))) + (((3 * (c |^ 2)) * a) + ((3 * (c |^ 2)) * b))) + (((6 * a) * b) * c)