let a, b, c, d, e, f be Real; ( 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f implies sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2))) )
assume that
A1:
0 <= a
and
A2:
0 <= b
and
A3:
0 <= c
and
A4:
( 0 <= d & 0 <= e & 0 <= f )
; sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))
( 0 <= b * d & 0 <= e * f )
by A2, A4, XREAL_1:127;
then A5:
0 + 0 <= (b * d) + (e * f)
by XREAL_1:7;
( 0 <= c ^2 & 0 <= d ^2 )
by XREAL_1:63;
then A6:
0 + 0 <= (c ^2) + (d ^2)
by XREAL_1:7;
0 <= f ^2
by XREAL_1:63;
then A7:
0 + 0 <= ((c ^2) + (d ^2)) + (f ^2)
by A6, XREAL_1:7;
then A8:
0 <= sqrt (((c ^2) + (d ^2)) + (f ^2))
by SQUARE_1:def 2;
0 <= (((a * c) + (b * d)) + (e * f)) ^2
by XREAL_1:63;
then A9:
sqrt ((((a * c) + (b * d)) + (e * f)) ^2) <= sqrt ((((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2)))
by Th17, SQUARE_1:26;
( 0 <= a ^2 & 0 <= b ^2 )
by XREAL_1:63;
then A10:
0 + 0 <= (a ^2) + (b ^2)
by XREAL_1:7;
0 <= e ^2
by XREAL_1:63;
then A11:
0 + 0 <= ((a ^2) + (b ^2)) + (e ^2)
by A10, XREAL_1:7;
0 <= a * c
by A1, A3, XREAL_1:127;
then
0 + 0 <= (a * c) + ((b * d) + (e * f))
by A5, XREAL_1:7;
then
((a * c) + (b * d)) + (e * f) <= sqrt ((((a ^2) + (b ^2)) + (e ^2)) * (((c ^2) + (d ^2)) + (f ^2)))
by A9, SQUARE_1:22;
then
((a * c) + (b * d)) + (e * f) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))
by A11, A7, SQUARE_1:29;
then
2 * (((a * c) + (b * d)) + (e * f)) <= 2 * ((sqrt (((a ^2) + (b ^2)) + (e ^2))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))
by XREAL_1:64;
then
((2 * ((a * c) + (b * d))) + (2 * (e * f))) + (e ^2) <= ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))) + (e ^2)
by XREAL_1:6;
then
((2 * ((a * c) + (b * d))) + ((e ^2) + (2 * (e * f)))) + (f ^2) <= (((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2)))) + (e ^2)) + (f ^2)
by XREAL_1:6;
then
(((2 * (a * c)) + (2 * (b * d))) + ((e + f) ^2)) + (b ^2) <= (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (f ^2)) + (b ^2)
by XREAL_1:6;
then
(((2 * (a * c)) + ((b ^2) + (2 * (b * d)))) + ((e + f) ^2)) + (d ^2) <= ((b ^2) + (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (f ^2))) + (d ^2)
by XREAL_1:6;
then
(a ^2) + ((2 * (a * c)) + (((b + d) ^2) + ((e + f) ^2))) <= ((b ^2) + (((e ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((d ^2) + (f ^2)))) + (a ^2)
by XREAL_1:6;
then
(((a ^2) + (2 * (a * c))) + (((b + d) ^2) + ((e + f) ^2))) + (c ^2) <= (((((a ^2) + (b ^2)) + (e ^2)) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((d ^2) + (f ^2))) + (c ^2)
by XREAL_1:6;
then
(((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= ((((a ^2) + (b ^2)) + (e ^2)) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((c ^2) + ((d ^2) + (f ^2)))
;
then
(((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= (((sqrt (((a ^2) + (b ^2)) + (e ^2))) ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + (((c ^2) + (d ^2)) + (f ^2))
by A11, SQUARE_1:def 2;
then A12:
(((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2) <= (((sqrt (((a ^2) + (b ^2)) + (e ^2))) ^2) + ((2 * (sqrt (((a ^2) + (b ^2)) + (e ^2)))) * (sqrt (((c ^2) + (d ^2)) + (f ^2))))) + ((sqrt (((c ^2) + (d ^2)) + (f ^2))) ^2)
by A7, SQUARE_1:def 2;
( 0 <= (a + c) ^2 & 0 <= (b + d) ^2 )
by XREAL_1:63;
then A13:
0 + 0 <= ((a + c) ^2) + ((b + d) ^2)
by XREAL_1:7;
0 <= (e + f) ^2
by XREAL_1:63;
then
0 + 0 <= (((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)
by A13, XREAL_1:7;
then A14:
sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= sqrt (((sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))) ^2)
by A12, SQUARE_1:26;
0 <= sqrt (((a ^2) + (b ^2)) + (e ^2))
by A11, SQUARE_1:def 2;
then
0 + 0 <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))
by A8, XREAL_1:7;
hence
sqrt ((((a + c) ^2) + ((b + d) ^2)) + ((e + f) ^2)) <= (sqrt (((a ^2) + (b ^2)) + (e ^2))) + (sqrt (((c ^2) + (d ^2)) + (f ^2)))
by A14, SQUARE_1:22; verum