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