defpred S1[ Nat] means for f being Real_Sequence
for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds
f . $1 >= ($1 to_power (k + 1)) / (k + 1);
A1:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A2:
for
f being
Real_Sequence for
k being
Element of
NAT st ( for
n being
Element of
NAT holds
f . n = Sum (
(seq_n^ k),
n) ) holds
f . n >= (n to_power (k + 1)) / (k + 1)
;
S1[n + 1]
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
let f be
Real_Sequence;
for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds
f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1)let k be
Element of
NAT ;
( ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) implies f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1) )
assume A3:
for
n being
Element of
NAT holds
f . n = Sum (
(seq_n^ k),
n)
;
f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1)
set R3 = (
n,1)
In_Power (k + 1);
len ((n,1) In_Power (k + 1)) =
(k + 1) + 1
by NEWTON:def 4
.=
k + 2
;
then reconsider R3 = (
n,1)
In_Power (k + 1) as
Element of
(k + 2) -tuples_on REAL by FINSEQ_2:92;
set R2 =
((k + 1) ") * ((n,1) In_Power (k + 1));
len (((k + 1) ") * ((n,1) In_Power (k + 1))) =
len ((n,1) In_Power (k + 1))
by NEWTON:2
.=
(k + 1) + 1
by NEWTON:def 4
.=
k + 2
;
then reconsider R2 =
((k + 1) ") * ((n,1) In_Power (k + 1)) as
Element of
(k + 2) -tuples_on REAL by FINSEQ_2:92;
reconsider nk =
(n to_power (k + 1)) / (k + 1) as
Element of
REAL by XREAL_0:def 1;
set R1 =
<*nk*> ^ ((n,1) In_Power k);
A4:
len <*((n to_power (k + 1)) / (k + 1))*> = 1
by FINSEQ_1:40;
set g =
seq_n^ k;
f . n >= (n to_power (k + 1)) / (k + 1)
by A2, A3;
then
Sum (
(seq_n^ k),
n)
>= (n to_power (k + 1)) / (k + 1)
by A3;
then A5:
(Partial_Sums (seq_n^ k)) . n >= (n to_power (k + 1)) / (k + 1)
by SERIES_1:def 5;
reconsider nk =
(n to_power (k + 1)) / (k + 1) as
Element of
REAL by XREAL_0:def 1;
(seq_n^ k) . (n + 1) =
(n + 1) to_power k
by Def3
.=
Sum ((n,1) In_Power k)
by NEWTON:30
;
then A6:
((n to_power (k + 1)) / (k + 1)) + ((seq_n^ k) . (n + 1)) = Sum (<*nk*> ^ ((n,1) In_Power k))
by RVSUM_1:76;
len ((n,1) In_Power k) = k + 1
by NEWTON:def 4;
then A7:
len (<*nk*> ^ ((n,1) In_Power k)) =
(k + 1) + 1
by A4, FINSEQ_1:22
.=
k + 2
;
then reconsider R1 =
<*nk*> ^ ((n,1) In_Power k) as
Element of
(k + 2) -tuples_on REAL by FINSEQ_2:92;
A8:
for
i being
Nat st
i in Seg (k + 2) holds
R2 . i <= R1 . i
proof
set k1 =
(k + 1) " ;
let i be
Nat;
( i in Seg (k + 2) implies R2 . i <= R1 . i )
assume A9:
i in Seg (k + 2)
;
R2 . i <= R1 . i
A10:
1
<= i
by A9, FINSEQ_1:1;
set r2 =
R2 . i;
set r1 =
R1 . i;
A11:
i <= k + 2
by A9, FINSEQ_1:1;
per cases
( i = 1 or i > 1 )
by A10, XXREAL_0:1;
suppose A13:
i > 1
;
R2 . i <= R1 . iset i0 =
i - 1;
set m =
(i - 1) - 1;
A14:
i - 1
> 1
- 1
by A13, XREAL_1:9;
then reconsider i0 =
i - 1 as
Element of
NAT by INT_1:3;
set l =
k - ((i - 1) - 1);
A15:
i0 >= 0 + 1
by A14, INT_1:7;
then reconsider m =
(i - 1) - 1 as
Element of
NAT by INT_1:3;
set i3 =
(k + 1) - i0;
len ((n,1) In_Power k) = k + 1
by NEWTON:def 4;
then A16:
dom ((n,1) In_Power k) = Seg (k + 1)
by FINSEQ_1:def 3;
i - 1
<= (k + 2) - 1
by A11, XREAL_1:9;
then A17:
i0 in dom ((n,1) In_Power k)
by A15, A16, FINSEQ_1:1;
m = i - 2
;
then A18:
k >= m + 0
by A11, XREAL_1:20;
then
k - ((i - 1) - 1) >= 0
by XREAL_1:19;
then reconsider l =
k - ((i - 1) - 1) as
Element of
NAT by INT_1:3;
A19:
(k + 1) - i0 = l
;
then A20:
i0 + 0 <= k + 1
by XREAL_1:19;
reconsider i3 =
(k + 1) - i0 as
Element of
NAT by A19;
len ((n,1) In_Power (k + 1)) = (k + 1) + 1
by NEWTON:def 4;
then
dom ((n,1) In_Power (k + 1)) = Seg (k + 2)
by FINSEQ_1:def 3;
then
R3 . i = (((k + 1) choose i0) * (n |^ i3)) * (1 |^ i0)
by A9, NEWTON:def 4;
then A21:
R2 . i =
((k + 1) ") * ((((k + 1) choose i0) * (n |^ i3)) * (1 |^ i0))
by RVSUM_1:45
.=
((k + 1) ") * ((((k + 1) choose l) * (n |^ l)) * (1 |^ i0))
by A20, NEWTON:20
.=
((k + 1) ") * ((((k + 1) choose l) * (n |^ l)) * 1)
by NEWTON:10
.=
(((k + 1) ") * ((k + 1) choose l)) * (n to_power l)
;
k - m <= k - 0
by XREAL_1:13;
then A22:
((k + 1) choose l) / (k + 1) <= k choose l
by Lm43;
R1 . i =
((n,1) In_Power k) . i0
by A4, A7, A11, A13, FINSEQ_1:24
.=
((k choose m) * (n |^ l)) * (1 |^ m)
by A17, NEWTON:def 4
.=
((k choose l) * (n |^ l)) * (1 |^ m)
by A18, NEWTON:20
.=
((k choose l) * (n |^ l)) * 1
by NEWTON:10
.=
(k choose l) * (n to_power l)
;
hence
R2 . i <= R1 . i
by A21, A22, XREAL_1:64;
verum end;
end;
((n + 1) to_power (k + 1)) / (k + 1) =
((n + 1) |^ (k + 1)) * ((k + 1) ")
.=
(Sum ((n,1) In_Power (k + 1))) * ((k + 1) ")
by NEWTON:30
.=
Sum (((k + 1) ") * ((n,1) In_Power (k + 1)))
by RVSUM_1:87
;
then A23:
((n + 1) to_power (k + 1)) / (k + 1) <= Sum R1
by A8, RVSUM_1:82;
f . (n + 1) =
Sum (
(seq_n^ k),
(n + 1))
by A3
.=
(Partial_Sums (seq_n^ k)) . (n + 1)
by SERIES_1:def 5
.=
((Partial_Sums (seq_n^ k)) . n) + ((seq_n^ k) . (n + 1))
by SERIES_1:def 1
;
then
f . (n + 1) >= ((n to_power (k + 1)) / (k + 1)) + ((seq_n^ k) . (n + 1))
by A5, XREAL_1:6;
hence
f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1)
by A6, A23, XXREAL_0:2;
verum
end;
A24:
S1[1]
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A24, A1);
hence
for n being Element of NAT st n >= 1 holds
for f being Real_Sequence
for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds
f . n >= (n to_power (k + 1)) / (k + 1)
; verum