let n be Nat; :: thesis: for i being Integer st 2 |^ 2 <= n & 2 |^ n divides i |^ 3 holds
2 |^ 2 divides i
let i be Integer; :: thesis: ( 2 |^ 2 <= n & 2 |^ n divides i |^ 3 implies 2 |^ 2 divides i )

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: ( 2 |^ 2 <= n & 2 |^ n divides i |^ 3 implies 2 |^ 2 divides i )

hence ( 2 |^ 2 <= n & 2 |^ n divides i |^ 3 implies 2 |^ 2 divides i ) by INT_2:12; :: thesis: verum

end;

suppose A1: i <> 0 ; :: thesis: ( 2 |^ 2 <= n & 2 |^ n divides i |^ 3 implies 2 |^ 2 divides i )

assume A2: 2 |^ 2 <= n ; :: thesis: ( not 2 |^ n divides i |^ 3 or 2 |^ 2 divides i )
assume 2 |^ n divides i |^ 3 ; :: thesis: 2 |^ 2 divides i
then 2 |^ n divides |.(i |^ 3).| by Th4;
then A3: 2 |^ n divides |.i.| |^ 3 by TAYLOR_2:1;
consider a being Nat, b being odd Nat such that
A4: |.i.| = b * (2 |^ a) by A1, NAT_6:3;
A5: |.i.| |^ 3 = (b |^ 3) * ((2 |^ a) |^ 3) by A4, NEWTON:7;
A6: b |^ 3,2 |^ n are_coprime by NAT_5:3;
(2 |^ a) |^ 3 = 2 |^ (3 * a) by NEWTON:9;
then n <= 3 * a by A3, A5, A6, INT_2:25, PEPIN:31;
then A7: 2 |^ 2 <= 3 * a by A2, XXREAL_0:2;

now :: thesis: not a < 1 + 1

assume a < 1 + 1 ; :: thesis: contradiction
then a <= 1 by NAT_1:13;
then 3 * a <= 3 * 1 by XREAL_1:64;
hence contradiction by A7, Lm1, XXREAL_0:2; :: thesis: verum

end;

then 2 |^ 2 divides |.i.| by A4, INT_2:2, PEPIN:31;
hence 2 |^ 2 divides i by Th4; :: thesis: verum

end;

end;