let a, b be Nat; :: thesis: ( a <> b implies (2 * a) * b < (a |^ 2) + (b |^ 2) )

A0: ( a * a = a |^ 2 & b * b = b |^ 2 ) by NEWTON:81;

assume a <> b ; :: thesis: (2 * a) * b < (a |^ 2) + (b |^ 2)

then ( not a - b is zero & a - b is real & 2 is even ) ;

then A1: (a - b) |^ 2 > 0 ;

assume not (2 * a) * b < (a |^ 2) + (b |^ 2) ; :: thesis: contradiction

then ((2 * a) * b) - ((2 * a) * b) >= ((a |^ 2) + (b |^ 2)) - ((2 * a) * b) by XREAL_1:9;

then 0 >= (a - b) * (a - b) by A0;

hence contradiction by A1, NEWTON:81; :: thesis: verum

A0: ( a * a = a |^ 2 & b * b = b |^ 2 ) by NEWTON:81;

assume a <> b ; :: thesis: (2 * a) * b < (a |^ 2) + (b |^ 2)

then ( not a - b is zero & a - b is real & 2 is even ) ;

then A1: (a - b) |^ 2 > 0 ;

assume not (2 * a) * b < (a |^ 2) + (b |^ 2) ; :: thesis: contradiction

then ((2 * a) * b) - ((2 * a) * b) >= ((a |^ 2) + (b |^ 2)) - ((2 * a) * b) by XREAL_1:9;

then 0 >= (a - b) * (a - b) by A0;

hence contradiction by A1, NEWTON:81; :: thesis: verum