let n be Nat; :: thesis: for t, u, z being Integer st (t |^ n) + (u |^ n) = z |^ n holds
2 |^ n divides ((t * u) * z) |^ n
let t, u, z be Integer; :: thesis: ( (t |^ n) + (u |^ n) = z |^ n implies 2 |^ n divides ((t * u) * z) |^ n )
assume (t |^ n) + (u |^ n) = z |^ n ; :: thesis: 2 |^ n divides ((t * u) * z) |^ n
then ((t |^ n) + (u |^ n)) + (- (z |^ n)) = 0 ;
then ((t |^ n) + (u |^ n)) + (- (z |^ n)) is even ;
then ((t |^ n) * (u |^ n)) * (- (z |^ n)) is even by Th100;
then - (((t |^ n) * (u |^ n)) * (z |^ n)) is even ;
then ((t |^ n) * (u |^ n)) * (z |^ n) is even by INT_2:10;
then ( t is even or u is even or z is even ) ;
then (t * u) * z is even ;
hence 2 |^ n divides ((t * u) * z) |^ n by Th15; :: thesis: verum