let a, b, c be Nat; :: thesis: ( (a |^ 2) + (b |^ 2) = c |^ 2 implies ex t being Integer st b |^ 2 = ((2 * a) + t) * t )
assume (a |^ 2) + (b |^ 2) = c |^ 2 ; :: thesis: ex t being Integer st b |^ 2 = ((2 * a) + t) * t
then b |^ 2 = (c |^ 2) - (a |^ 2)
.= (c - a) * (c + a) by NEWTON01:1
.= (c - a) * ((c - a) + (2 * a)) ;
hence ex t being Integer st b |^ 2 = ((2 * a) + t) * t ; :: thesis: verum