let a, b be non negative Real; :: thesis: for n being non zero Nat holds (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (a + b) |^ (n + 1)
let n be non zero Nat; :: thesis: (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (a + b) |^ (n + 1)
(a * (((a + b) |^ n) + (b |^ n))) + (b * (b |^ n)) <= (((a + b) |^ (n + 1)) - (b |^ (n + 1))) + (b * (b |^ n)) by PLT, XREAL_1:6;
then (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (((a + b) |^ (n + 1)) - (b |^ (n + 1))) + (b |^ (n + 1)) by NEWTON:6;
hence (a * ((a + b) |^ n)) + ((a + b) * (b |^ n)) <= (a + b) |^ (n + 1) ; :: thesis: verum