let m, x, z, y be real number ; :: thesis: (m * x) + (z * y) <= (sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 )))
( m ^2 >= 0 & z ^2 >= 0 & x ^2 >= 0 & y ^2 >= 0 )
by XREAL_1:65;
then A1:
( (m ^2 ) + (z ^2 ) >= 0 & (x ^2 ) + (y ^2 ) >= 0 )
;
A2: ((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 A1, SQUARE_1:def 4
.=
((m ^2 ) + (z ^2 )) * ((x ^2 ) + (y ^2 ))
by A1, SQUARE_1:def 4
.=
((((m ^2 ) * (x ^2 )) + ((m * y) ^2 )) + ((z * x) ^2 )) + ((z ^2 ) * (y ^2 ))
;
((m * y) ^2 ) + ((z * x) ^2 ) >= (2 * (m * y)) * (z * x)
by SERIES_3:6;
then A3:
(((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;
((m * x) + (z * y)) ^2 >= 0
by XREAL_1:65;
then A4:
sqrt (((sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 )))) ^2 ) >= sqrt (((m * x) + (z * y)) ^2 )
by A2, A3, SQUARE_1:94;
A5:
( sqrt ((m ^2 ) + (z ^2 )) >= 0 & sqrt ((x ^2 ) + (y ^2 )) >= 0 )
by A1, SQUARE_1:def 4;
then A6:
(sqrt ((m ^2 ) + (z ^2 ))) * (sqrt ((x ^2 ) + (y ^2 ))) >= sqrt (((m * x) + (z * y)) ^2 )
by A4, SQUARE_1:89;