let a, b be non zero Nat; :: thesis: ( (a |^ 2) - (b |^ 2) in NAT implies ((a |^ 2) - (b |^ 2)) mod (2 * b) = ((a |^ 2) + (b |^ 2)) mod (2 * b) )
assume A1: (a |^ 2) - (b |^ 2) in NAT ; :: thesis: ((a |^ 2) - (b |^ 2)) mod (2 * b) = ((a |^ 2) + (b |^ 2)) mod (2 * b)
A2: b |^ 2 = b * b by NEWTON:81;
((a |^ 2) - (b |^ 2)) mod (2 * (b |^ 2)) = ((a |^ 2) + (b |^ 2)) mod (2 * (b |^ 2)) by MRS;
then ((a |^ 2) - (b |^ 2)) mod ((2 * b) * b) = ((a |^ 2) + (b |^ 2)) mod ((2 * b) * b) by A2;
hence ((a |^ 2) - (b |^ 2)) mod (2 * b) = ((a |^ 2) + (b |^ 2)) mod (2 * b) by A1, RMI; :: thesis: verum