let a, b be Nat; :: thesis: for t being Integer st b |^ 2 = ((2 * a) + t) * t holds
ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2
let t be Integer; :: thesis: ( b |^ 2 = ((2 * a) + t) * t implies ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 )
assume b |^ 2 = ((2 * a) + t) * t ; :: thesis: ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2
then A1: b |^ 2 = ((a + t) + a) * ((a + t) - a)
.= ((a + t) |^ 2) - (a |^ 2) by NEWTON01:1 ;
|.(a + t).| in NAT by INT_1:3;
then consider c being Nat such that
A2: c = |.(a + t).| ;
( c |^ 2 = (a + t) |^ 2 or c |^ 2 = (- (a + t)) |^ 2 ) by A2, ABSVALUE:1;
then c |^ 2 = (a + t) |^ 2 by WSIERP_1:1;
hence ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 by A1; :: thesis: verum