let x, y be positive Nat; :: thesis: ( ((x * y) + x) + y = 2 |^ 32 iff ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) )
A1: ( x + 1 <> 0 + 1 & y + 1 <> 0 + 1 ) ;
thus ( not ((x * y) + x) + y = 2 |^ 32 or ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) :: thesis: ( ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) implies ((x * y) + x) + y = 2 |^ 32 )

proof

assume ((x * y) + x) + y = 2 |^ 32 ; :: thesis: ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) )
then Fermat 5 = (x + 1) * (y + 1) by Lm4;
then ( ( x + 1 = 641 & y + 1 = 6700417 ) or ( x + 1 = 6700417 & y + 1 = 641 ) ) by A1, Th84, NUMBER07:59, XPRIMES1:641, XPRIMES3:4;
hence ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) ; :: thesis: verum

end;

thus ( ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) implies ((x * y) + x) + y = 2 |^ 32 ) by Lm11, Lm6, Lm12; :: thesis: verum