let a, b, c, n be Nat; ( a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n implies ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l ) )
set x = a gcd b;
assume A1:
( a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n )
; ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )
then A1b:
n <> 0
by Lm0;
a gcd b <> 0
by A1, INT_2:5;
then A1d:
(a gcd b) |^ n > 0
by PREPOWER:6;
consider j, k being Integer such that
A2:
( a = (a gcd b) * j & b = (a gcd b) * k & j,k are_coprime )
by A1, INT_2:23;
( j > 0 & k > 0 )
by A1, A2;
then A2b:
( j in NAT & k in NAT )
by INT_1:3;
A3:
a |^ n = ((a gcd b) |^ n) * (j |^ n)
by A2, NEWTON:7;
A4:
b |^ n = ((a gcd b) |^ n) * (k |^ n)
by A2, NEWTON:7;
then
c |^ n = ((a gcd b) |^ n) * ((j |^ n) + (k |^ n))
by A1, A3;
then
a gcd b divides c
by A1b, INT_1:def 3, WSIERP_1:26;
then consider l being Nat such that
A8:
c = (a gcd b) * l
by NAT_D:def 3;
((j |^ n) + (k |^ n)) * ((a gcd b) |^ n) = (l |^ n) * ((a gcd b) |^ n)
by A1, A3, A4, A8, NEWTON:7;
then
(j |^ n) + (k |^ n) = l |^ n
by A1d, XCMPLX_1:5;
hence
ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )
by A2, A2b, A8; verum