let a, b, c, d, e, f be real number ; ( 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:129;
then A5:
0 + 0 <= (b * d) + (e * f)
by XREAL_1:9;
( 0 <= c ^2 & 0 <= d ^2 )
by XREAL_1:65;
then A6:
0 + 0 <= (c ^2 ) + (d ^2 )
by XREAL_1:9;
0 <= f ^2
by XREAL_1:65;
then A7:
0 + 0 <= ((c ^2 ) + (d ^2 )) + (f ^2 )
by A6, XREAL_1:9;
then A8:
0 <= sqrt (((c ^2 ) + (d ^2 )) + (f ^2 ))
by SQUARE_1:def 4;
0 <= (((a * c) + (b * d)) + (e * f)) ^2
by XREAL_1:65;
then A9:
sqrt ((((a * c) + (b * d)) + (e * f)) ^2 ) <= sqrt ((((a ^2 ) + (b ^2 )) + (e ^2 )) * (((c ^2 ) + (d ^2 )) + (f ^2 )))
by Th15, SQUARE_1:94;
( 0 <= a ^2 & 0 <= b ^2 )
by XREAL_1:65;
then A10:
0 + 0 <= (a ^2 ) + (b ^2 )
by XREAL_1:9;
0 <= e ^2
by XREAL_1:65;
then A11:
0 + 0 <= ((a ^2 ) + (b ^2 )) + (e ^2 )
by A10, XREAL_1:9;
0 <= a * c
by A1, A3, XREAL_1:129;
then
0 + 0 <= (a * c) + ((b * d) + (e * f))
by A5, XREAL_1:9;
then
((a * c) + (b * d)) + (e * f) <= sqrt ((((a ^2 ) + (b ^2 )) + (e ^2 )) * (((c ^2 ) + (d ^2 )) + (f ^2 )))
by A9, SQUARE_1:89;
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:97;
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:66;
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:8;
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:8;
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:8;
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:8;
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:8;
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:8;
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 4;
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 4;
( 0 <= (a + c) ^2 & 0 <= (b + d) ^2 )
by XREAL_1:65;
then A13:
0 + 0 <= ((a + c) ^2 ) + ((b + d) ^2 )
by XREAL_1:9;
0 <= (e + f) ^2
by XREAL_1:65;
then
0 + 0 <= (((a + c) ^2 ) + ((b + d) ^2 )) + ((e + f) ^2 )
by A13, XREAL_1:9;
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:94;
0 <= sqrt (((a ^2 ) + (b ^2 )) + (e ^2 ))
by A11, SQUARE_1:def 4;
then
0 + 0 <= (sqrt (((a ^2 ) + (b ^2 )) + (e ^2 ))) + (sqrt (((c ^2 ) + (d ^2 )) + (f ^2 )))
by A8, XREAL_1:9;
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:89; verum