let a, b, c, n be Nat; :: thesis: ( 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 & j,l are_coprime & k,l are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l ) )
assume A1: ( a > 0 & b > 0 & (a |^ n) + (b |^ n) = c |^ n ) ; :: thesis: ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & j,l are_coprime & k,l are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l )
then n <> 0 by Lm0;
then consider m being Nat such that
A3: n = 1 + m by NAT_1:10, NAT_1:14;
consider j, k, l being Nat such that
A4: ( (j |^ (m + 1)) + (k |^ (m + 1)) = l |^ (m + 1) & j,k are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l ) by A1, A3, Lm58;
( j,l are_coprime & k,l are_coprime ) by A4, Lm59;
hence ex j, k, l being Nat st
( (j |^ n) + (k |^ n) = l |^ n & j,k are_coprime & j,l are_coprime & k,l are_coprime & a = (a gcd b) * j & b = (a gcd b) * k & c = (a gcd b) * l ) by A3, A4; :: thesis: verum