let a, b, n be Nat; :: thesis: ( a > 0 implies (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2) )
assume A1: a > 0 ; :: thesis: (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2)
assume not (a |^ (n + 2)) + (a |^ (n + 2)) <> b |^ (n + 2) ; :: thesis: contradiction
then consider j, k, l being Nat such that
A3: ( (j |^ (n + 2)) + (k |^ (n + 2)) = l |^ (n + 2) & j,k are_coprime & j,l are_coprime & k,l are_coprime & a = (a gcd a) * j & a = (a gcd a) * k & b = (a gcd a) * l ) by A1, Th41;
( k * a = 1 * a & j * a = 1 * a ) by NAT_D:32, A3;
then ( k = 1 & j = 1 ) by A1, XCMPLX_1:5;
hence contradiction by A3, Lm60; :: thesis: verum