let a, b, n be Nat; :: thesis: ( n > 0 & a > b & a,b are_coprime implies ((a |^ n) + (b |^ n)) gcd ((a |^ n) - (b |^ n)) <= 2 )
assume ( n > 0 & a > b & a,b are_coprime ) ; :: thesis: ((a |^ n) + (b |^ n)) gcd ((a |^ n) - (b |^ n)) <= 2
then ( a |^ n > b |^ n & a |^ n,b |^ n are_coprime ) by Th40, WSIERP_1:11;
hence ((a |^ n) + (b |^ n)) gcd ((a |^ n) - (b |^ n)) <= 2 by Th8; :: thesis: verum