:: Partial Sum and Partial Product of Some Series
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005 Association of Mizar Users
Lm1:
for a, b being real number holds
( 4 = 2 |^ 2 & (a + b) |^ 2 = ((a |^ 2) + ((2 * a) * b)) + (b |^ 2) )
Lm2:
for n being Element of NAT holds (((1 / 2) |^ (n + 1)) + (2 |^ (n + 1))) |^ 2 = (((1 / 4) |^ (n + 1)) + (4 |^ (n + 1))) + 2
Lm3:
for n being Element of NAT holds (((1 / 3) |^ (n + 1)) + (3 |^ (n + 1))) |^ 2 = (((1 / 9) |^ (n + 1)) + (9 |^ (n + 1))) + 2
Lm4:
for a, b being real number holds (a - b) * (a + b) = (a |^ 2) - (b |^ 2)
Lm5:
for a, b being real number holds (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
Lm6:
for n being Element of NAT
for a being real number 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 Element of NAT holds 1 / ((2 -Root (n + 2)) + (2 -Root (n + 1))) = (2 -Root (n + 2)) - (2 -Root (n + 1))
theorem Th1: :: SERIES_4:1
theorem Th2: :: SERIES_4:2
theorem :: SERIES_4:3
theorem :: SERIES_4:4
theorem :: SERIES_4:5
theorem :: SERIES_4:6
theorem :: SERIES_4:7
theorem :: SERIES_4:8
theorem :: SERIES_4:9
theorem :: SERIES_4:10
theorem :: SERIES_4:11
theorem :: SERIES_4:12
theorem :: SERIES_4:13
theorem :: SERIES_4:14
theorem :: SERIES_4:15
theorem :: SERIES_4:16
theorem :: SERIES_4:17
theorem :: SERIES_4:18
theorem :: SERIES_4:19
theorem :: SERIES_4:20
theorem :: SERIES_4:21
theorem :: SERIES_4:22
theorem :: SERIES_4:23
theorem :: SERIES_4:24
theorem :: SERIES_4:25
theorem :: SERIES_4:26
theorem :: SERIES_4:27
theorem :: SERIES_4:28
theorem :: SERIES_4:29
theorem :: SERIES_4:30