let n be Nat; :: thesis: for f1, f2 being natural-valued increasing FinSequence st n > 1 & Sum (n |^ f1) > 0 & Sum (n |^ f1) = Sum (n |^ f2) holds
f1 . (len f1) <= f2 . (len f2)
let f1, f2 be natural-valued increasing FinSequence; :: thesis: ( n > 1 & Sum (n |^ f1) > 0 & Sum (n |^ f1) = Sum (n |^ f2) implies f1 . (len f1) <= f2 . (len f2) )
assume A1: ( n > 1 & Sum (n |^ f1) > 0 & Sum (n |^ f1) = Sum (n |^ f2) ) ; :: thesis: f1 . (len f1) <= f2 . (len f2)
A2: ( ((n |^ f1),1) +... = Sum (n |^ f1) & Sum (n |^ f2) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) & ((n |^ f2),1) +... = Sum (n |^ f2) ) by Th21, Th22;
set l1 = len f1;
set l2 = len f2;
A3: f1 <> {} by A1, RVSUM_1:72;
assume f1 . (len f1) > f2 . (len f2) ; :: thesis: contradiction
then f1 . (len f1) >= 1 + (f2 . (len f2)) by NAT_1:13;
then A4: n |^ (f1 . (len f1)) >= n |^ (1 + (f2 . (len f2))) by PREPOWER:93, A1;
A5: Sum (n |^ f1) < 2 * (n |^ (f2 . (len f2))) by A1, Th26, A2;
reconsider L1 = (len f1) - 1 as Nat by A3;
reconsider F1 = f1 | L1 as natural-valued FinSequence ;
A6: ((n |^ F1),1) +... = Sum (n |^ F1) by Th21;
L1 + 1 = len f1 ;
then Sum (n |^ f1) = (Sum (n |^ F1)) + (n |^ (f1 . (len f1))) by Lm5;
then Sum (n |^ f1) >= 0 + (n |^ (f1 . (len f1))) by A6, XREAL_1:6;
then A7: n |^ (f1 . (len f1)) < 2 * (n |^ (f2 . (len f2))) by A5, XXREAL_0:2;
n >= 1 + 1 by A1, NAT_1:13;
then 2 * (n |^ (f2 . (len f2))) <= n * (n |^ (f2 . (len f2))) by XREAL_1:64;
then 2 * (n |^ (f2 . (len f2))) <= n |^ (1 + (f2 . (len f2))) by NEWTON:6;
hence contradiction by A7, XXREAL_0:2, A4; :: thesis: verum