let n be Nat; :: thesis: for a, b being non zero Nat
for p being prime Nat st (a |^ n) + (b |^ n) = p |^ n holds
a,b are_coprime
let a, b be non zero Nat; :: thesis: for p being prime Nat st (a |^ n) + (b |^ n) = p |^ n holds
a,b are_coprime
let p be prime Nat; :: thesis: ( (a |^ n) + (b |^ n) = p |^ n implies a,b are_coprime )
A1: (a |^ n) + (b |^ n) > (a |^ n) + 0 by XREAL_1:6;
assume A2: (a |^ n) + (b |^ n) = p |^ n ; :: thesis: a,b are_coprime
then reconsider n = n as non zero Nat ;
a |^ n < p |^ n by A1, A2;
then a < p by NEWTON02:40;
then a,p are_coprime by NAT_D:7, NAT_6:6;
then a |^ n,p |^ n are_coprime by WSIERP_1:11;
then a |^ n,b |^ n are_coprime by A2, NEWTON02:45;
then a,b |^ n are_coprime by NEWTON02:73;
hence a,b are_coprime by NEWTON02:73; :: thesis: verum