let n be Nat; :: thesis: for a, b being non negative Real holds (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)
let a, b be non negative Real; :: thesis: (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)
defpred S₁[ Nat] means (a + b) |^ ($1 + 2) >= (a |^ ($1 + 2)) + ((($1 + 2) * (a |^ ($1 + 1))) * b);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
a |^ (n + 1) >= 0

proof

per cases ( a = 0 or a > 0 ) ;

suppose a = 0 ; :: thesis: a |^ (n + 1) >= 0

hence a |^ (n + 1) >= 0 ; :: thesis: verum

end;

suppose a > 0 ; :: thesis: a |^ (n + 1) >= 0

hence a |^ (n + 1) >= 0 by PREPOWER:6; :: thesis: verum

end;

end;

end;

then A2: (a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b) <= (((n + 2) * (a |^ (n + 1))) * (b ^2)) + ((a |^ (n + 3)) + (((n + 3) * (a |^ (n + 2))) * b)) by XREAL_1:31;
assume (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) ; :: thesis: S₁[n + 1]
then ((a + b) |^ (n + 2)) * (a + b) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b) by XREAL_1:64;
then (a + b) |^ ((n + 2) + 1) >= ((a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b)) * (a + b) by NEWTON:6;
then (a + b) |^ (n + 3) >= (((a |^ (n + 2)) * a) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b) ;
then (a + b) |^ (n + 3) >= ((a |^ ((n + 2) + 1)) + (b * (a |^ (n + 2)))) + ((((n + 2) * (a + b)) * (a |^ (n + 1))) * b) by NEWTON:6;
then (a + b) |^ (n + 3) >= (((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a * (a |^ (n + 1)))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b)) ;
then (a + b) |^ (n + 3) >= (((a |^ (n + 3)) + ((a |^ (n + 2)) * b)) + (((n + 2) * (a |^ ((n + 1) + 1))) * b)) + (((n + 2) * (a |^ (n + 1))) * (b * b)) by NEWTON:6;
hence S₁[n + 1] by A2, XXREAL_0:2; :: thesis: verum

end;

A3: (a |^ (0 + 2)) + (((0 + 2) * (a |^ (0 + 1))) * b) = (a ^2) + ((2 * (a |^ 1)) * b) by Lm1
.= (a ^2) + ((2 * a) * b) ;
(a + b) |^ (0 + 2) = (a + b) ^2 by Lm1
.= ((a ^2) + ((2 * a) * b)) + (b ^2) ;
then A4: S₁[ 0 ] by A3, XREAL_1:31;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence (a + b) |^ (n + 2) >= (a |^ (n + 2)) + (((n + 2) * (a |^ (n + 1))) * b) ; :: thesis: verum