let a, b, c, d be positive Real; :: thesis: ( ((a * b) * c) * d >= ((((a + b) + c) + d) / 4) |^ 4 implies ( a = b & b = c & c = d ) )
set f = <*a,b,c,d*>;
A1: len <*a,b,c,d*> = 4 by FINSEQ_4:76;
A2: Sum <*a,b,c,d*> = ((a + b) + c) + d by RVSUM_1:142;
(GMean <*a,b,c,d*>) |^ 4 <= (Mean <*a,b,c,d*>) |^ 4 by PREPOWER:9, RVSUM_3:47;
then A3: ((a * b) * c) * d <= ((((a + b) + c) + d) / 4) |^ 4 by A1, A2, Th88;
A4: (GMean <*a,b,c,d*>) |^ 4 = ((a * b) * c) * d by Th93;
A5: Mean <*a,b,c,d*> = (((a + b) + c) + d) / 4 by Th97;
assume ((a * b) * c) * d >= ((((a + b) + c) + d) / 4) |^ 4 ; :: thesis: ( a = b & b = c & c = d )
then ((a * b) * c) * d = ((((a + b) + c) + d) / 4) |^ 4 by A3, XXREAL_0:1;
then (Mean <*a,b,c,d*>) |^ 4 = (GMean <*a,b,c,d*>) |^ 4 by A4, A5;
then <*a,b,c,d*> is constant by Lm19, WSIERP_1:3;
hence ( a = b & b = c & c = d ) by Th98; :: thesis: verum