let a, b be real number ; :: thesis: ( 0 <= a & 0 <= b implies sqrt (a + b) <= (sqrt a) + (sqrt b) )
assume A1: ( 0 <= a & 0 <= b ) ; :: thesis: sqrt (a + b) <= (sqrt a) + (sqrt b)
then A2: 0 + 0 <= a + b ;
( 0 <= sqrt a & 0 <= sqrt b ) by A1, SQUARE_1:def 4;
then A3: 0 + 0 <= (sqrt a) + (sqrt b) ;
A4: sqrt ((a + ((2 * (sqrt a)) * (sqrt b))) + b) = sqrt ((((sqrt a) ^2 ) + ((2 * (sqrt a)) * (sqrt b))) + b) by A1, SQUARE_1:def 4
.= sqrt ((((sqrt a) ^2 ) + ((2 * (sqrt a)) * (sqrt b))) + ((sqrt b) ^2 )) by A1, SQUARE_1:def 4
.= sqrt (((sqrt a) + (sqrt b)) ^2 )
.= (sqrt a) + (sqrt b) by A3, SQUARE_1:89 ;
0 <= a * b by A1;
then 0 <= sqrt (a * b) by SQUARE_1:def 4;
then 0 <= (sqrt a) * (sqrt b) by A1, SQUARE_1:97;
then 0 <= 2 * ((sqrt a) * (sqrt b)) ;
then a + 0 <= a + ((2 * (sqrt a)) * (sqrt b)) by XREAL_1:8;
then a + b <= (a + ((2 * (sqrt a)) * (sqrt b))) + b by XREAL_1:8;
hence sqrt (a + b) <= (sqrt a) + (sqrt b) by A2, A4, SQUARE_1:94; :: thesis: verum