let a, b, c be Nat; :: thesis: for q being Integer st q < 0 & b < c & (a |^ 2) + (b |^ 2) = c |^ 2 holds
(a |^ 2) + ((b + q) |^ 2) > (c + q) |^ 2
let q be Integer; :: thesis: ( q < 0 & b < c & (a |^ 2) + (b |^ 2) = c |^ 2 implies (a |^ 2) + ((b + q) |^ 2) > (c + q) |^ 2 )
assume A1: ( q < 0 & b < c & (a |^ 2) + (b |^ 2) = c |^ 2 ) ; :: thesis: (a |^ 2) + ((b + q) |^ 2) > (c + q) |^ 2
then A1a: b - c < c - c by XREAL_1:9;
((a |^ 2) + ((b + q) |^ 2)) - ((c + q) |^ 2) = (2 * q) * (b - c) by A1, Lm61;
then (((a |^ 2) + ((b + q) |^ 2)) - ((c + q) |^ 2)) + ((c + q) |^ 2) > 0 + ((c + q) |^ 2) by A1, A1a, XREAL_1:6;
hence (a |^ 2) + ((b + q) |^ 2) > (c + q) |^ 2 ; :: thesis: verum