let a, b be real positive number ; :: thesis: for n being Element of NAT holds ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n
let n be Element of NAT ; :: thesis: ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n
defpred S₁[ Element of NAT ] means ((a |^ $1) + (b |^ $1)) / 2 >= ((a + b) / 2) |^ $1;
((a |^ 0 ) + (b |^ 0 )) / 2 = (1 + (b |^ 0 )) / 2 by NEWTON:9
.= (1 + 1) / 2 by NEWTON:9
.= ((a + b) / 2) |^ 0 by NEWTON:9 ;
then A1: S₁[ 0 ] ;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A3: (((a |^ n) + (b |^ n)) / 2) * (a + b) >= (((a + b) / 2) |^ n) * (a + b) by XREAL_1:66;

per cases ( a - b >= 0 or a - b < 0 ) ;

suppose A4: a - b >= 0 ; :: thesis: S₁[n + 1]

then (a - b) + b >= 0 + b by XREAL_1:8;
then a |^ n >= b |^ n by PREPOWER:17;
then (a |^ n) - (b |^ n) >= 0 by XREAL_1:50;
then (a - b) * ((a |^ n) - (b |^ n)) >= 0 by A4;
then (((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 ;
then ((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 by NEWTON:11;
then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b) >= 0 ;
then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1)) >= 0 by NEWTON:11;
then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a)) >= 0 + (((a |^ n) * b) + ((b |^ n) * a)) by XREAL_1:8;
then ((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1))) by XREAL_1:8;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= (((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) ;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) by NEWTON:11;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:11;
then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:74;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A3, XXREAL_0:2;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:15;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) * (a + b)) / (2 |^ n) ;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a + b) |^ (n + 1)) / (2 |^ n) by NEWTON:11;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:74;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:79;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:11;
hence S₁[n + 1] by PREPOWER:15; :: thesis: verum

end;

suppose A5: a - b < 0 ; :: thesis: S₁[n + 1]

then (a - b) + b < 0 + b by XREAL_1:8;
then a |^ n <= b |^ n by PREPOWER:17;
then (a |^ n) - (b |^ n) <= 0 by XREAL_1:49;
then (a - b) * ((a |^ n) - (b |^ n)) >= 0 by A5;
then (((a |^ n) * a) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 ;
then ((a |^ (n + 1)) - ((a |^ n) * b)) - (((b |^ n) * a) - ((b |^ n) * b)) >= 0 by NEWTON:11;
then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + ((b |^ n) * b) >= 0 ;
then (((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1)) >= 0 by NEWTON:11;
then ((((a |^ (n + 1)) - ((a |^ n) * b)) - ((b |^ n) * a)) + (b |^ (n + 1))) + (((a |^ n) * b) + ((b |^ n) * a)) >= 0 + (((a |^ n) * b) + ((b |^ n) * a)) by XREAL_1:8;
then ((a |^ (n + 1)) + (b |^ (n + 1))) + ((a |^ (n + 1)) + (b |^ (n + 1))) >= (((a |^ n) * b) + ((b |^ n) * a)) + ((a |^ (n + 1)) + (b |^ (n + 1))) by XREAL_1:8;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= (((a |^ (n + 1)) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) ;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + (b |^ (n + 1)) by NEWTON:11;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:11;
then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:74;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A3, XXREAL_0:2;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:15;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) * (a + b)) / (2 |^ n) ;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= ((a + b) |^ (n + 1)) / (2 |^ n) by NEWTON:11;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:74;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:79;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:11;
hence S₁[n + 1] by PREPOWER:15; :: thesis: verum

end;

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n ; :: thesis: verum