let n be Nat; :: thesis: for f being natural-valued increasing FinSequence st n > 1 holds
((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))
defpred S1[ Nat] means for f being natural-valued increasing FinSequence st n > 1 & f . (len f) <= $1 & f <> {} holds
Sum (n |^ f) < 2 * (n |^ (f . (len f)));
A1: for f being natural-valued FinSequence st n > 1 & len f = 1 holds
Sum (n |^ f) < 2 * (n |^ (f . (len f)))
proof
let f be natural-valued FinSequence; :: thesis: ( n > 1 & len f = 1 implies Sum (n |^ f) < 2 * (n |^ (f . (len f))) )
assume A2: ( n > 1 & len f = 1 ) ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
then A3: 1 in dom f by FINSEQ_3:25;
n to_power (f . 1) > 0 by A2, NEWTON:83;
then 1 * (n to_power (f . 1)) < 2 * (n to_power (f . 1)) by XREAL_1:68;
then A4: (n |^ f) . 1 < 2 * (n |^ (f . (len f))) by A3, Def4, A2;
n |^ f = <*((n |^ f) . 1)*> by CARD_1:def 7, A2, FINSEQ_1:40;
hence Sum (n |^ f) < 2 * (n |^ (f . (len f))) by RVSUM_1:73, A4; :: thesis: verum
end;
A5: S1[ 0 ]
proof
let f be natural-valued increasing FinSequence; :: thesis: ( n > 1 & f . (len f) <= 0 & f <> {} implies Sum (n |^ f) < 2 * (n |^ (f . (len f))) )
assume A6: ( n > 1 & f . (len f) <= 0 & f <> {} ) ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
len f <= 1
proof
assume A7: len f > 1 ; :: thesis: contradiction
then ( 1 in dom f & len f in dom f ) by FINSEQ_3:25;
then f . 1 < 0 by A7, VALUED_0:def 13, A6;
hence contradiction ; :: thesis: verum
end;
then len f = 1 by NAT_1:25, A6;
hence Sum (n |^ f) < 2 * (n |^ (f . (len f))) by A6, A1; :: thesis: verum
end;
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
let f be natural-valued increasing FinSequence; :: thesis: ( n > 1 & f . (len f) <= i + 1 & f <> {} implies Sum (n |^ f) < 2 * (n |^ (f . (len f))) )
assume A10: ( n > 1 & f . (len f) <= i + 1 & f <> {} ) ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
per cases ( f . (len f) <= i or f . (len f) = i + 1 ) by A10, NAT_1:8;
suppose f . (len f) <= i ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
hence Sum (n |^ f) < 2 * (n |^ (f . (len f))) by A10, A9; :: thesis: verum
end;
suppose f . (len f) = i + 1 ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
per cases ( len f = 1 or len f > 1 ) by A10, NAT_1:25;
suppose len f = 1 ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
hence Sum (n |^ f) < 2 * (n |^ (f . (len f))) by A10, A1; :: thesis: verum
end;
suppose A11: len f > 1 ; :: thesis: Sum (n |^ f) < 2 * (n |^ (f . (len f)))
then reconsider l1 = (len f) - 1 as Nat ;
reconsider f1 = f | l1 as natural-valued FinSequence ;
l1 + 1 > 1 by A11;
then A12: ( l1 >= 1 & l1 + 1 > l1 ) by NAT_1:13;
then A13: ( l1 in dom f & len f in dom f ) by A11, FINSEQ_3:25;
then f . l1 < f . (len f) by A12, VALUED_0:def 13;
then f . l1 < i + 1 by A10, XXREAL_0:2;
then A14: f . l1 <= i by NAT_1:13;
len f = l1 + 1 ;
then A15: Sum (n |^ f) = (Sum (n |^ f1)) + (n |^ (f . (len f))) by Lm5;
A16: len f1 = l1 by A12, FINSEQ_1:59;
A17: f1 <> {} by A12, FINSEQ_1:59;
l1 in Seg l1 by A12;
then A18: f . l1 = f1 . l1 by FUNCT_1:49;
f1 is increasing by Lm4;
then A19: Sum (n |^ f1) < 2 * (n |^ (f . l1)) by A17, A18, A16, A10, A9, A14;
1 + (f . l1) <= f . (len f) by A13, A12, VALUED_0:def 13, NAT_1:13;
then A20: n |^ (1 + (f . l1)) <= n |^ (f . (len f)) by PREPOWER:93, A10;
n >= 1 + 1 by A10, NAT_1:13;
then A21: 2 * (n |^ (f . l1)) <= n * (n |^ (f . l1)) by XREAL_1:64;
n |^ (1 + (f . l1)) = n * (n |^ (f . l1)) by NEWTON:6;
then Sum (n |^ f1) < n |^ (1 + (f . l1)) by XXREAL_0:2, A19, A21;
then Sum (n |^ f1) < n |^ (f . (len f)) by XXREAL_0:2, A20;
then Sum (n |^ f) < (n |^ (f . (len f))) + (n |^ (f . (len f))) by A15, XREAL_1:8;
hence Sum (n |^ f) < 2 * (n |^ (f . (len f))) ; :: thesis: verum
end;
end;
end;
end;
end;
A22: for i being Nat holds S1[i] from NAT_1:sch 2(A5, A8);
 let f be natural-valued increasing FinSequence; :: thesis: ( n > 1 implies ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f))) )
assume A23: n > 1 ; :: thesis: ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))
A24: Sum (n |^ f) = ((n |^ f) . 1) + (((n |^ f),2) +...) by Th22;
per cases ( f = {} or f <> {} ) ;
suppose f = {} ; :: thesis: ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))
then A25: Sum (n |^ f) = 0 by RVSUM_1:72;
n |^ (f . (len f)) > 0 by A23, NEWTON:83;
hence ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f))) by A24, A25; :: thesis: verum
end;
suppose f <> {} ; :: thesis: ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))
hence ((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f))) by A22, A23, A24; :: thesis: verum
end;
end;