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:
S1[1]
A5:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A7:
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)
;
:: thesis: S1[n + 1]
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
let f be
Real_Sequence;
:: thesis: 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 ;
:: thesis: ( ( 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 A8:
for
n being
Element of
NAT holds
f . n = Sum (seq_n^ k),
n
;
:: thesis: f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1)
set g =
seq_n^ k;
A9:
f . (n + 1) =
Sum (seq_n^ k),
(n + 1)
by A8
.=
(Partial_Sums (seq_n^ k)) . (n + 1)
by SERIES_1:def 6
.=
((Partial_Sums (seq_n^ k)) . n) + ((seq_n^ k) . (n + 1))
by SERIES_1:def 1
;
f . n >= (n to_power (k + 1)) / (k + 1)
by A7, A8;
then
Sum (seq_n^ k),
n >= (n to_power (k + 1)) / (k + 1)
by A8;
then
(Partial_Sums (seq_n^ k)) . n >= (n to_power (k + 1)) / (k + 1)
by SERIES_1:def 6;
then A10:
f . (n + 1) >= ((n to_power (k + 1)) / (k + 1)) + ((seq_n^ k) . (n + 1))
by A9, XREAL_1:8;
(seq_n^ k) . (n + 1) =
(n + 1) to_power k
by Def3
.=
Sum (n,1 In_Power k)
by NEWTON:41
;
then A11:
((n to_power (k + 1)) / (k + 1)) + ((seq_n^ k) . (n + 1)) = Sum (<*((n to_power (k + 1)) / (k + 1))*> ^ (n,1 In_Power k))
by RVSUM_1:106;
A12:
((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:41
.=
Sum (((k + 1) " ) * (n,1 In_Power (k + 1)))
by RVSUM_1:117
;
set R1 =
<*((n to_power (k + 1)) / (k + 1))*> ^ (n,1 In_Power k);
set R2 =
((k + 1) " ) * (n,1 In_Power (k + 1));
A13:
len (n,1 In_Power k) = k + 1
by NEWTON:def 4;
A14:
len <*((n to_power (k + 1)) / (k + 1))*> = 1
by FINSEQ_1:57;
then A15:
len (<*((n to_power (k + 1)) / (k + 1))*> ^ (n,1 In_Power k)) =
(k + 1) + 1
by A13, FINSEQ_1:35
.=
k + 2
;
then reconsider R1 =
<*((n to_power (k + 1)) / (k + 1))*> ^ (n,1 In_Power k) as
Element of
(k + 2) -tuples_on REAL by FINSEQ_2:110;
len (((k + 1) " ) * (n,1 In_Power (k + 1))) =
len (n,1 In_Power (k + 1))
by NEWTON:6
.=
(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:110;
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:110;
for
i being
Nat st
i in Seg (k + 2) holds
R2 . i <= R1 . i
proof
let i be
Nat;
:: thesis: ( i in Seg (k + 2) implies R2 . i <= R1 . i )
assume A16:
i in Seg (k + 2)
;
:: thesis: R2 . i <= R1 . i
set r2 =
R2 . i;
set r1 =
R1 . i;
A17:
( 1
<= i &
i <= k + 2 )
by A16, FINSEQ_1:3;
set k1 =
(k + 1) " ;
per cases
( i = 1 or i > 1 )
by A17, XXREAL_0:1;
suppose A19:
i > 1
;
:: thesis: R2 . i <= R1 . iset i0 =
i - 1;
set m =
(i - 1) - 1;
set l =
k - ((i - 1) - 1);
A20:
i - 1
> 1
- 1
by A19, XREAL_1:11;
then reconsider i0 =
i - 1 as
Element of
NAT by INT_1:16;
A21:
i0 >= 0 + 1
by A20, INT_1:20;
then
(i - 1) - 1
>= 0
by XREAL_1:21;
then reconsider m =
(i - 1) - 1 as
Element of
NAT by INT_1:16;
m = i - 2
;
then A22:
k >= m + 0
by A17, XREAL_1:22;
then
k - ((i - 1) - 1) >= 0
by XREAL_1:21;
then reconsider l =
k - ((i - 1) - 1) as
Element of
NAT by INT_1:16;
A23:
i - 1
<= (k + 2) - 1
by A17, XREAL_1:11;
len (n,1 In_Power k) = k + 1
by NEWTON:def 4;
then
dom (n,1 In_Power k) = Seg (k + 1)
by FINSEQ_1:def 3;
then A24:
i0 in dom (n,1 In_Power k)
by A21, A23, FINSEQ_1:3;
A25:
R1 . i =
(n,1 In_Power k) . i0
by A14, A15, A17, A19, FINSEQ_1:37
.=
((k choose m) * (n |^ l)) * (1 |^ m)
by A24, NEWTON:def 4
.=
((k choose l) * (n |^ l)) * (1 |^ m)
by A22, NEWTON:30
.=
((k choose l) * (n |^ l)) * 1
by NEWTON:15
.=
(k choose l) * (n to_power l)
;
set i3 =
(k + 1) - i0;
A26:
(k + 1) - i0 = l
;
then reconsider i3 =
(k + 1) - i0 as
Element of
NAT ;
A27:
i0 + 0 <= k + 1
by A26, XREAL_1:21;
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 A16, NEWTON:def 4;
then A28:
R2 . i =
((k + 1) " ) * ((((k + 1) choose i0) * (n |^ i3)) * (1 |^ i0))
by RVSUM_1:67
.=
((k + 1) " ) * ((((k + 1) choose l) * (n |^ l)) * (1 |^ i0))
by A27, NEWTON:30
.=
((k + 1) " ) * ((((k + 1) choose l) * (n |^ l)) * 1)
by NEWTON:15
.=
(((k + 1) " ) * ((k + 1) choose l)) * (n to_power l)
;
k - m <= k - 0
by XREAL_1:15;
then
((k + 1) choose l) / (k + 1) <= k choose l
by Lm49;
then
((k + 1) " ) * ((k + 1) choose l) <= k choose l
;
hence
R2 . i <= R1 . i
by A25, A28, XREAL_1:66;
:: thesis: verum end;
end;
then
((n + 1) to_power (k + 1)) / (k + 1) <= Sum R1
by A12, RVSUM_1:112;
hence
f . (n + 1) >= ((n + 1) to_power (k + 1)) / (k + 1)
by A10, A11, XXREAL_0:2;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A1, A5);
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)
; :: thesis: verum