let m, x, y, z be Real; (m * x) + (z * y) <= (sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2)))
A1:
z ^2 >= 0
by XREAL_1:63;
A2:
m ^2 >= 0
by XREAL_1:63;
then A3:
sqrt ((m ^2) + (z ^2)) >= 0
by A1, SQUARE_1:def 2;
A4:
((m * x) + (z * y)) ^2 >= 0
by XREAL_1:63;
((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:6;
A6:
y ^2 >= 0
by XREAL_1:63;
A7:
x ^2 >= 0
by XREAL_1:63;
then A8:
sqrt ((x ^2) + (y ^2)) >= 0
by A6, SQUARE_1:def 2;
((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 2
.=
((m ^2) + (z ^2)) * ((x ^2) + (y ^2))
by A7, A6, SQUARE_1:def 2
.=
((((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:26;
then A9:
(sqrt ((m ^2) + (z ^2))) * (sqrt ((x ^2) + (y ^2))) >= sqrt (((m * x) + (z * y)) ^2)
by A3, A8, SQUARE_1:22;