let a be even Integer; :: thesis: for b being Integer
for n being non zero Nat st a,b are_coprime holds
(b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime
let b be Integer; :: thesis: for n being non zero Nat st a,b are_coprime holds
(b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime
let n be non zero Nat; :: thesis: ( a,b are_coprime implies (b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime )
assume A1: a,b are_coprime ; :: thesis: (b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime
A2: a |^ n,b |^ n are_coprime by A1, WSIERP_1:11;
(a |^ n) + (b |^ n),(a |^ n) - (b |^ n) are_coprime by A2, SCP;
then 1 = ((a |^ n) + (b |^ n)) gcd (- ((b |^ n) - (a |^ n)))
.= ((a |^ n) + (b |^ n)) gcd ((b |^ n) - (a |^ n)) by NEWTON02:1 ;
hence (b |^ n) + (a |^ n),(b |^ n) - (a |^ n) are_coprime ; :: thesis: verum