let a, b be Integer; :: thesis: for m, n being non zero Nat holds
( a,b are_coprime iff a |^ m,b |^ n are_coprime )
let m, n be non zero Nat; :: thesis: ( a,b are_coprime iff a |^ m,b |^ n are_coprime )
L1: ( a,b are_coprime implies a |^ m,b |^ n are_coprime )

proof

assume a,b are_coprime ; :: thesis: a |^ m,b |^ n are_coprime
then a,b |^ n are_coprime by WSIERP_1:10;
hence a |^ m,b |^ n are_coprime by WSIERP_1:10; :: thesis: verum

end;

( a |^ m,b |^ n are_coprime implies a,b are_coprime )

proof

assume A1: a |^ m,b |^ n are_coprime ; :: thesis: a,b are_coprime
reconsider k = m - 1 as Nat ;
reconsider l = n - 1 as Nat ;
( a |^ (k + 1) = a * (a |^ k) & b |^ (l + 1) = b * (b |^ l) ) by NEWTON:6;
hence a,b are_coprime by A1, N0141; :: thesis: verum

end;

hence ( a,b are_coprime iff a |^ m,b |^ n are_coprime ) by L1; :: thesis: verum