let p, r be real number ; :: thesis: ( p >= 0 & r >= 0 implies p + r >= 2 * (sqrt (p * r)) )
assume A1: ( p >= 0 & r >= 0 ) ; :: thesis: p + r >= 2 * (sqrt (p * r))
A2: ((sqrt p) - (sqrt r)) ^2 >= 0 by XREAL_1:65;
((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 4
.= (p - ((2 * (sqrt p)) * (sqrt r))) + r by A1, SQUARE_1:def 4
.= (p + r) - ((2 * (sqrt p)) * (sqrt r)) ;
then 0 + ((2 * (sqrt p)) * (sqrt r)) <= p + r by A2, XREAL_1:21;
then 2 * ((sqrt p) * (sqrt r)) <= p + r ;
hence p + r >= 2 * (sqrt (p * r)) by A1, SQUARE_1:97; :: thesis: verum