let n be Nat; 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; ( 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) )
; 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)
; 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; verum