let n, i be Nat; :: thesis: ( n >= 2 |^ ((2 * i) + 2) implies n / 2 >= (2 |^ i) * (sqrt n) )
assume A1: n >= 2 |^ ((2 * i) + 2) ; :: thesis: n / 2 >= (2 |^ i) * (sqrt n)
assume n / 2 < (2 |^ i) * (sqrt n) ; :: thesis: contradiction
then (n / 2) * 2 < ((2 |^ i) * (sqrt n)) * 2 by XREAL_1:68;
then n < (2 * (2 |^ i)) * (sqrt n) ;
then n < (2 |^ (i + 1)) * (sqrt n) by NEWTON:6;
then n ^2 < ((2 |^ (i + 1)) * (sqrt n)) ^2 by SQUARE_1:16;
then n ^2 < ((2 |^ (i + 1)) ^2) * ((sqrt n) ^2) ;
then n ^2 < ((2 |^ (i + 1)) ^2) * n by SQUARE_1:def 2;
then n ^2 < ((2 |^ (i + 1)) |^ 2) * n by NEWTON:81;
then n ^2 < (2 |^ (2 * (i + 1))) * n by NEWTON:9;
then (n ^2) / n < ((2 |^ ((2 * i) + 2)) * n) / n by A1, XREAL_1:74;
then n < ((2 |^ ((2 * i) + 2)) * n) / n by A1, XCMPLX_1:89;
hence contradiction by A1, XCMPLX_1:89; :: thesis: verum