let j, z be Integer; :: thesis: ( 0 <= j & j ^2 < z & z < (j + 1) ^2 implies for i being Integer holds not z = i ^2 )
assume that
A1: j >= 0 and
A2: j ^2 < z and
A3: z < (j + 1) ^2 ; :: thesis: for i being Integer holds not z = i ^2
given i being Integer such that A4: i ^2 = z ; :: thesis: contradiction
sqrt (j ^2) = j by A1, SQUARE_1:22;
then A5: j < sqrt z by A2, SQUARE_1:27;
sqrt ((j + 1) ^2) = j + 1 by A1, SQUARE_1:22;
then sqrt (i ^2) < j + 1 by A3, A4, SQUARE_1:27;
hence contradiction by A4, A5, INT_1:7; :: thesis: verum