let c, k be Nat; :: thesis: for a, b being non zero Nat st c >= a + b holds
(c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2))
let a, b be non zero Nat; :: thesis: ( c >= a + b implies (c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2)) )
A1: ( (a |^ 1) + (b |^ 1) <= (a + b) |^ 1 implies (a |^ ((k + 1) + 1)) + (b |^ ((k + 1) + 1)) < (a + b) |^ ((k + 1) + 1) ) by NEWTON01:18;
assume c >= a + b ; :: thesis: (c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2))
then c |^ (k + 1) >= (a + b) |^ (k + 1) by NEWTON02:40;
then (c |^ (k + 1)) * (a + b) >= ((a + b) |^ (k + 1)) * (a + b) by XREAL_1:64;
then (c |^ (k + 1)) * (a + b) >= (a + b) |^ ((k + 1) + 1) by NEWTON:6;
hence (c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2)) by A1, XXREAL_0:2; :: thesis: verum