let r1, r2 be non negative Real; :: thesis: ( sqrt (r1 * r2) = (r1 + r2) / 2 iff r1 = r2 )

hereby :: thesis: ( r1 = r2 implies sqrt (r1 * r2) = (r1 + r2) / 2 )

assume A1: sqrt (r1 * r2) = (r1 + r2) / 2 ; :: thesis: r1 = r2
A2: ((sqrt (r1 * r2)) * 2) ^2 = ((sqrt (r1 * r2)) ^2) * (2 ^2)
.= (r1 * r2) * 4 by SQUARE_1:def 2
.= (4 * r1) * r2 ;
0 = ((r1 + r2) ^2) - (((sqrt (r1 * r2)) * 2) ^2) by A1
.= (r1 - r2) ^2 by A2 ;
then r1 - r2 = 0 ;
hence r1 = r2 ; :: thesis: verum

end;

assume A3: r1 = r2 ; :: thesis: sqrt (r1 * r2) = (r1 + r2) / 2
then sqrt (r1 * r2) = (sqrt r1) ^2 by SQUARE_1:29
.= (r1 + r2) / 2 by A3, SQUARE_1:def 2 ;
hence sqrt (r1 * r2) = (r1 + r2) / 2 ; :: thesis: verum