let a, b, n, k be Nat; :: thesis: ( b > 0 & k > 0 & a + b > k & a + b divides k * (a |^ n) implies not a,b are_coprime )
assume A1: ( b > 0 & k > 0 & a + b > k & a + b divides k * (a |^ n) ) ; :: thesis: not a,b are_coprime
defpred S1[ Nat] means ( a + b divides k * (a |^ $1) implies not a,b are_coprime );
L1: S1[ 0 ]
proof
k * (a |^ 0) = k * 1 by NEWTON:4;
hence S1[ 0 ] by A1, INT_2:27; :: thesis: verum
end;
L2: for x being Nat st S1[x] holds
S1[x + 1]
proof
let x be Nat; :: thesis: ( S1[x] implies S1[x + 1] )
assume B1: S1[x] ; :: thesis: S1[x + 1]
B2: a |^ (x + 1) = (a |^ x) * a by NEWTON:6;
( a,b are_coprime & not a + b divides k * (a |^ x) implies not a + b divides k * (a |^ (x + 1)) )
proof
assume C1: ( a,b are_coprime & not a + b divides k * (a |^ x) ) ; :: thesis: not a + b divides k * (a |^ (x + 1))
then 1 = (b + (1 * a)) gcd a by A1, EULER_1:16;
then a + b,a are_coprime ;
then not a + b divides (k * (a |^ x)) * a by C1, INT_2:25;
hence not a + b divides k * (a |^ (x + 1)) by B2; :: thesis: verum
end;
hence S1[x + 1] by B1; :: thesis: verum
end;
for c being Nat holds S1[c] from NAT_1:sch 2(L1, L2);
 hence not a,b are_coprime by A1; :: thesis: verum