let j, k, l, m be Nat; :: thesis: ( (j |^ (m + 1)) + (k |^ (m + 1)) = l |^ (m + 1) & j,k are_coprime implies j,l are_coprime )
set n = m + 1;
assume A1: ( (j |^ (m + 1)) + (k |^ (m + 1)) = l |^ (m + 1) & j,k are_coprime ) ; :: thesis: j,l are_coprime
then (j |^ (m + 1)) gcd (k |^ (m + 1)) = 1 by WSIERP_1:11, INT_2:def 3;
then l |^ (m + 1),j |^ (m + 1) are_coprime by A1, EULER_1:7;
hence j,l are_coprime by Lm53; :: thesis: verum