let n, x, y, z be positive Nat; :: thesis: ( (n |^ x) + (n |^ y) = n |^ z iff ( n = 2 & y = x & z = x + 1 ) )
thus ( (n |^ x) + (n |^ y) = n |^ z implies ( n = 2 & y = x & z = x + 1 ) ) :: thesis: ( n = 2 & y = x & z = x + 1 implies (n |^ x) + (n |^ y) = n |^ z )

proof

assume A1: (n |^ x) + (n |^ y) = n |^ z ; :: thesis: ( n = 2 & y = x & z = x + 1 )

per cases ( x <= y or y <= x ) ;

suppose x <= y ; :: thesis: ( n = 2 & y = x & z = x + 1 )

hence ( n = 2 & y = x & z = x + 1 ) by A1, Lm18; :: thesis: verum

end;

suppose y <= x ; :: thesis: ( n = 2 & y = x & z = x + 1 )

then ( n = 2 & y = x & z = y + 1 ) by A1, Lm18;
hence ( n = 2 & y = x & z = x + 1 ) ; :: thesis: verum

end;

end;

end;

(2 |^ x) + (2 |^ x) = 2 * (2 |^ x)
.= 2 |^ (x + 1) by NEWTON:6 ;
hence ( n = 2 & y = x & z = x + 1 implies (n |^ x) + (n |^ y) = n |^ z ) ; :: thesis: verum