let a, b be non negative Real; :: thesis: for n being non zero Nat holds (a |^ n) + (b |^ n) <= Sum ((a,b) Subnomial n)
let n be non zero Nat; :: thesis: (a |^ n) + (b |^ n) <= Sum ((a,b) Subnomial n)
reconsider f = (a,b) Subnomial n as nonnegative-yielding FinSequence of REAL ;
len f = n + 1 by Def2;
then A1: Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1)) by NEWTON02:115;
A2: ((a,b) Subnomial n) . 1 = ((a,b) In_Power n) . 1 by NS
.= a |^ n by NEWTON:28 ;
A3: ((a,b) Subnomial n) . (n + 1) = ((a,b) In_Power n) . (n + 1) by NS
.= b |^ n by NEWTON:29 ;
(Sum ((f | n) /^ 1)) + ((a |^ n) + (b |^ n)) >= 0 + ((a |^ n) + (b |^ n)) by XREAL_1:6;
hence (a |^ n) + (b |^ n) <= Sum ((a,b) Subnomial n) by A1, A2, A3; :: thesis: verum