let a, b, n be Nat; :: thesis: ( a > 1 & b > 0 & a gcd b = 1 implies not a divides (a + b) |^ n )
assume A0: ( a > 1 & b > 0 & a gcd b = 1 ) ; :: thesis: not a divides (a + b) |^ n
then a gcd (b |^ n) = 1 by WSIERP_1:12;
then not a divides a gcd (b |^ n) by WSIERP_1:15, A0;
then not a divides b |^ n by INT_2:def 2;
hence not a divides (a + b) |^ n by Th11; :: thesis: verum