let a, b be real positive number ; :: thesis: ( a < b implies a / b < sqrt (a / b) )
assume A1: a < b ; :: thesis: a / b < sqrt (a / b)
b ^2 > 0 ;
then b |^ 2 > 0 by NEWTON:100;
then (b |^ 2) * b > 0 ;
then A2: b |^ (2 + 1) > 0 by NEWTON:11;
a - b < 0 by A1, XREAL_1:51;
then (a * b) * (a - b) < 0 ;
then (((a ^2 ) * b) - (a * (b ^2 ))) + (a * (b ^2 )) < 0 + (a * (b ^2 )) by XREAL_1:10;
then ((a ^2 ) * b) / (b |^ (2 + 1)) < (a * (b ^2 )) / (b |^ (2 + 1)) by A2, XREAL_1:76;
then ((a ^2 ) * b) / ((b |^ 2) * b) < (a * (b ^2 )) / (b |^ (2 + 1)) by NEWTON:11;
then ((a ^2 ) * b) / ((b |^ 2) * b) < (a * (b ^2 )) / ((b |^ 2) * b) by NEWTON:11;
then ((a ^2 ) * b) / ((b ^2 ) * b) < (a * (b ^2 )) / ((b |^ 2) * b) by NEWTON:100;
then ((a ^2 ) * b) / ((b ^2 ) * b) < (a * (b ^2 )) / ((b ^2 ) * b) by NEWTON:100;
then (a ^2 ) / (b ^2 ) < (a * (b ^2 )) / (b * (b ^2 )) by XCMPLX_1:92;
then (a ^2 ) / (b ^2 ) < a / b by XCMPLX_1:92;
then (a / b) ^2 < a / b by XCMPLX_1:77;
then sqrt ((a / b) ^2 ) < sqrt (a / b) by SQUARE_1:95;
hence a / b < sqrt (a / b) by SQUARE_1:89; :: thesis: verum