let m, x, z, y be real number ; (m * x) + (z * y) <= (sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 )))
A1:
z ^2 >= 0
by XREAL_1:65;
A2:
m ^2 >= 0
by XREAL_1:65;
then A3:
sqrt ((m ^2 ) + (z ^2 )) >= 0
by A1, SQUARE_1:def 4;
A4:
((m * x) + (z * y)) ^2 >= 0
by XREAL_1:65;
((m * y) ^2 ) + ((z * x) ^2 ) >= (2 * (m * y)) * (z * x)
by SERIES_3:6;
then A5:
(((m * y) ^2 ) + ((z * x) ^2 )) + (((m ^2 ) * (x ^2 )) + ((z ^2 ) * (y ^2 ))) >= ((((2 * m) * x) * y) * z) + (((m ^2 ) * (x ^2 )) + ((z ^2 ) * (y ^2 )))
by XREAL_1:8;
A6:
y ^2 >= 0
by XREAL_1:65;
A7:
x ^2 >= 0
by XREAL_1:65;
then A8:
sqrt ((x ^2 ) + (y ^2 )) >= 0
by A6, SQUARE_1:def 4;
((sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 )))) ^2 =
((sqrt ((m ^2 ) + (z ^2 ))) ^2 ) * ((sqrt ((x ^2 ) + (y ^2 ))) ^2 )
.=
((m ^2 ) + (z ^2 )) * ((sqrt ((x ^2 ) + (y ^2 ))) ^2 )
by A2, A1, SQUARE_1:def 4
.=
((m ^2 ) + (z ^2 )) * ((x ^2 ) + (y ^2 ))
by A7, A6, SQUARE_1:def 4
.=
((((m ^2 ) * (x ^2 )) + ((m * y) ^2 )) + ((z * x) ^2 )) + ((z ^2 ) * (y ^2 ))
;
then
sqrt (((sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 )))) ^2 ) >= sqrt (((m * x) + (z * y)) ^2 )
by A5, A4, SQUARE_1:94;
then A9:
(sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 ))) >= sqrt (((m * x) + (z * y)) ^2 )
by A3, A8, SQUARE_1:89;