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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A2: (((a |^ n) + (b |^ n)) / 2) * (a + b) >= (((a + b) / 2) |^ n) * (a + b) by XREAL_1:64;

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

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

then (a - b) + b >= 0 + b by XREAL_1:6;
then a |^ n >= b |^ n by PREPOWER:9;
then (a |^ n) - (b |^ n) >= 0 by XREAL_1:48;
then (a - b) * ((a |^ n) - (b |^ n)) >= 0 by A3;
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:6;
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:6;
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:6;
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:6;
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:6;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:6;
then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:72;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A2, XXREAL_0:2;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:8;
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:6;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:72;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:78;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:6;
hence S₁[n + 1] by PREPOWER:8; :: thesis: verum

end;

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

then (a - b) + b < 0 + b by XREAL_1:6;
then a |^ n <= b |^ n by PREPOWER:9;
then (a |^ n) - (b |^ n) <= 0 by XREAL_1:47;
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:6;
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:6;
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:6;
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:6;
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:6;
then (2 * (a |^ (n + 1))) + (2 * (b |^ (n + 1))) >= ((((a |^ n) * a) + ((a |^ n) * b)) + ((b |^ n) * a)) + ((b |^ n) * b) by NEWTON:6;
then (2 * ((a |^ (n + 1)) + (b |^ (n + 1)))) / 2 >= (((a |^ n) + (b |^ n)) * (a + b)) / 2 by XREAL_1:72;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) / 2) |^ n) * (a + b) by A2, XXREAL_0:2;
then (a |^ (n + 1)) + (b |^ (n + 1)) >= (((a + b) |^ n) / (2 |^ n)) * (a + b) by PREPOWER:8;
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:6;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= (((a + b) |^ (n + 1)) / (2 |^ n)) / 2 by XREAL_1:72;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / ((2 |^ n) * 2) by XCMPLX_1:78;
then ((a |^ (n + 1)) + (b |^ (n + 1))) / 2 >= ((a + b) |^ (n + 1)) / (2 |^ (n + 1)) by NEWTON:6;
hence S₁[n + 1] by PREPOWER:8; :: thesis: verum

end;

end;

end;

((a |^ 0) + (b |^ 0)) / 2 = (1 + (b |^ 0)) / 2 by NEWTON:4
.= (1 + 1) / 2 by NEWTON:4
.= ((a + b) / 2) |^ 0 by NEWTON:4 ;
then A5: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A1);
hence ((a |^ n) + (b |^ n)) / 2 >= ((a + b) / 2) |^ n ; :: thesis: verum