let p, r be Real; :: thesis: ( p >= 0 & r >= 0 implies p + r >= 2 * (sqrt (p * r)) )
assume that
A1: p >= 0 and
A2: r >= 0 ; :: thesis: p + r >= 2 * (sqrt (p * r))
A3: ((sqrt p) - (sqrt r)) ^2 >= 0 by XREAL_1:63;
((sqrt p) - (sqrt r)) ^2 = (((sqrt p) ^2) - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2)
.= (p - ((2 * (sqrt p)) * (sqrt r))) + ((sqrt r) ^2) by A1, SQUARE_1:def 2
.= (p - ((2 * (sqrt p)) * (sqrt r))) + r by A2, SQUARE_1:def 2
.= (p + r) - ((2 * (sqrt p)) * (sqrt r)) ;
then 0 + ((2 * (sqrt p)) * (sqrt r)) <= p + r by A3, XREAL_1:19;
then 2 * ((sqrt p) * (sqrt r)) <= p + r ;
hence p + r >= 2 * (sqrt (p * r)) by A1, A2, SQUARE_1:29; :: thesis: verum