let n, x, y, z be positive Nat; :: thesis: ( x <= y & (n |^ x) + (n |^ y) = n |^ z implies ( n = 2 & y = x & z = x + 1 ) )
assume that
A1: x <= y and
A2: (n |^ x) + (n |^ y) = n |^ z ; :: thesis: ( n = 2 & y = x & z = x + 1 )
n >= 0 + 1 by NAT_1:13;

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

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

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

end;

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

(n |^ z) - (n |^ x) <= (n |^ z) - 0 by XREAL_1:10;
then A4: z >= y by A2, A3, PEPIN:66;
then reconsider zx = z - x as Element of NAT by A1, INT_1:5, XXREAL_0:2;
reconsider yx = y - x as Element of NAT by A1, INT_1:5;
A5: ( (n |^ x) * (n |^ zx) = n |^ (x + zx) & (n |^ x) * (n |^ yx) = n |^ (x + yx) ) by NEWTON:8;
n |^ x = (n |^ z) - (n |^ y) by A2
.= (n |^ x) * ((n |^ zx) - (n |^ yx)) by A5 ;
then A6: (n |^ zx) - (n |^ yx) = 1 by XCMPLX_1:7;

A7: now :: thesis: not y > x

assume A8: y > x ; :: thesis: contradiction
then yx > x - x by XREAL_1:9;
then A9: n divides n |^ yx by NAT_3:3;
z > x by A4, A8, XXREAL_0:2;
then zx > x - x by XREAL_1:9;
then n divides n |^ zx by NAT_3:3;
hence contradiction by A3, A6, A9, INT_5:1, NAT_D:7; :: thesis: verum

end;

then x = y by A1, XXREAL_0:1;
then A10: n |^ yx = 1 by NEWTON:4;
then zx = 1 by A6, NUMBER03:34, XPRIMES1:2;
hence ( n = 2 & y = x & z = x + 1 ) by A1, A6, A7, A10, XXREAL_0:1; :: thesis: verum

end;

end;