let a be Nat; :: thesis: ( a >= 3 iff (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 )
( a >= 3 implies (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 )

proof

assume a >= 3 ; :: thesis: (a |^ 2) + (a |^ 2) > (a + 1) |^ 2
then consider b being Nat such that
A2: a = 3 + b by NAT_1:10;
defpred S₁[ Nat] means ((3 + $1) |^ 2) + ((3 + $1) |^ 2) > ((3 + $1) + 1) |^ 2;
A3: S₁[ 0 ]

proof

( 3 |^ 2 = 3 * 3 & 4 |^ 2 = 4 * 4 ) by NEWTON:81;
hence S₁[ 0 ] ; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then ( 1 + (2 + k) >= 1 + 0 & ((3 + k) |^ 2) + (((3 + k) + 0) |^ 2) > (((3 + k) + 0) + 1) |^ 2 ) by XREAL_1:6;
then (((3 + k) + 1) |^ 2) + ((((3 + k) + 0) + 1) |^ 2) > ((((3 + k) + 1) + 0) + 1) |^ 2 by Th47;
hence S₁[k + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A4);
hence (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 by A2; :: thesis: verum

end;

hence ( a >= 3 iff (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 ) by Lm120; :: thesis: verum