let x be real number ; :: thesis: ( x ^2 < 1 implies ((2 * x) / (1 + (x ^2 ))) ^2 < 1 )
assume A1: x ^2 < 1 ; :: thesis: ((2 * x) / (1 + (x ^2 ))) ^2 < 1
x ^2 >= 0 by XREAL_1:65;
then A2: 4 * (x ^2 ) >= 4 * 0 ;
(x ^2 ) + (- 1) < 1 + (- 1) by A1, XREAL_1:10;
then ((x ^2 ) - 1) * ((x ^2 ) - 1) > 0 * ((x ^2 ) - 1) by XREAL_1:71;
then A3: ((((x ^2 ) ^2 ) - (2 * (x ^2 ))) + 1) + (4 * (x ^2 )) > 0 + (4 * (x ^2 )) by XREAL_1:10;
((2 * x) / (1 + (x ^2 ))) ^2 = ((2 * x) ^2 ) / ((1 + (x ^2 )) ^2 ) by XCMPLX_1:77
.= (4 * (x ^2 )) / ((((x ^2 ) ^2 ) + (2 * (x ^2 ))) + 1) ;
hence ((2 * x) / (1 + (x ^2 ))) ^2 < 1 by A2, A3, XREAL_1:191; :: thesis: verum