let a be Nat; :: thesis: ( (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 implies a >= 3 )
L1: (a - 1) |^ 2 = (a + (- 1)) |^ 2
.= ((a |^ 2) + ((2 * a) * (- 1))) + ((- 1) |^ 2) by Lm10
.= ((a |^ 2) + ((2 * a) * (- 1))) + ((- 1) * (- 1)) by NEWTON:81 ;
assume A1: (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 ; :: thesis: a >= 3
then a |^ 2 > 0 ;
then a |^ 2 > 0 |^ 2 by NEWTON:11;
then a - 1 >= 1 - 1 by NAT_1:14, XREAL_1:9;
then A2: a - 1 in NAT by INT_1:3;
(a + 1) |^ 2 = ((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2) by Lm10
.= ((a |^ 2) + (2 * a)) + 1 ;
then ((a |^ 2) + (a |^ 2)) - (((a |^ 2) + (2 * a)) - 1) > (((a |^ 2) + (2 * a)) + 1) - (((a |^ 2) + (2 * a)) - 1) by A1, XREAL_1:9;
then (a - 1) |^ 2 > 1 |^ 2 by L1, XXREAL_0:2;
then (a - 1) + 1 > 1 + 1 by A2, Lm3a, XREAL_1:6;
then a >= 2 + 1 by NAT_1:13;
hence a >= 3 ; :: thesis: verum