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

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