let a, b be non negative Real; :: thesis: for n being non zero Nat holds
( a * (((a + b) + b) |^ n) >= ((a + b) |^ (n + 1)) - (b |^ (n + 1)) & ((a + b) |^ (n + 1)) - (b |^ (n + 1)) >= a * (((a + b) |^ n) + (b |^ n)) )
let n be non zero Nat; :: thesis: ( a * (((a + b) + b) |^ n) >= ((a + b) |^ (n + 1)) - (b |^ (n + 1)) & ((a + b) |^ (n + 1)) - (b |^ (n + 1)) >= a * (((a + b) |^ n) + (b |^ n)) )
((a + b) - b) * (Sum (((a + b),b) Subnomial n)) = ((a + b) |^ (n + 1)) - (b |^ (n + 1)) by SumS;
hence ( a * (((a + b) + b) |^ n) >= ((a + b) |^ (n + 1)) - (b |^ (n + 1)) & ((a + b) |^ (n + 1)) - (b |^ (n + 1)) >= a * (((a + b) |^ n) + (b |^ n)) ) by SST, SLT, XREAL_1:64; :: thesis: verum