let a, b be Real; :: thesis: ( 0 <= a & 0 <= b implies sqrt (a + b) <= (sqrt a) + (sqrt b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; :: thesis: sqrt (a + b) <= (sqrt a) + (sqrt b)
A3: 0 <= sqrt a by A1, Def2;
0 <= sqrt (a * b) by A1, A2, Def2;
then 0 <= (sqrt a) * (sqrt b) by A1, A2, Th29;
then 0 <= 2 * ((sqrt a) * (sqrt b)) ;
then a + 0 <= a + ((2 * (sqrt a)) * (sqrt b)) by XREAL_1:6;
then A4: a + b <= (a + ((2 * (sqrt a)) * (sqrt b))) + b by XREAL_1:6;
A5: 0 <= sqrt b by A2, Def2;
sqrt ((a + ((2 * (sqrt a)) * (sqrt b))) + b) = sqrt ((((sqrt a) ^2) + ((2 * (sqrt a)) * (sqrt b))) + b) by A1, Def2
.= sqrt ((((sqrt a) ^2) + ((2 * (sqrt a)) * (sqrt b))) + ((sqrt b) ^2)) by A2, Def2
.= sqrt (((sqrt a) + (sqrt b)) ^2)
.= (sqrt a) + (sqrt b) by A3, A5, Def2 ;
hence sqrt (a + b) <= (sqrt a) + (sqrt b) by A1, A2, A4, Th26; :: thesis: verum