let a, b be Real; :: thesis: sqrt ((a ^2) + (b ^2)) <= |.a.| + |.b.|
A1: (sqrt ((a ^2) + (b ^2))) ^2 >= 0 by XREAL_1:63;
( a ^2 >= 0 & b ^2 >= 0 ) by XREAL_1:63;
then A2: (sqrt ((a ^2) + (b ^2))) ^2 = (a ^2) + (b ^2) by SQUARE_1:def 2;
( (|.a.| + |.b.|) ^2 = ((|.a.| ^2) + ((2 * |.a.|) * |.b.|)) + (|.b.| ^2) & |.a.| ^2 = a ^2 ) by Th75;
then ((|.a.| + |.b.|) ^2) - ((sqrt ((a ^2) + (b ^2))) ^2) = (((a ^2) + ((2 * |.a.|) * |.b.|)) + (b ^2)) - ((a ^2) + (b ^2)) by A2, Th75
.= (2 * |.a.|) * |.b.| ;
then (|.a.| + |.b.|) ^2 >= (sqrt ((a ^2) + (b ^2))) ^2 by XREAL_1:49;
then sqrt ((|.a.| + |.b.|) ^2) >= sqrt ((sqrt ((a ^2) + (b ^2))) ^2) by A1, SQUARE_1:26;
hence sqrt ((a ^2) + (b ^2)) <= |.a.| + |.b.| by A2, SQUARE_1:22; :: thesis: verum