let b, a be Nat; :: thesis: for k, l being Integer st k gcd l = 1 holds
( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
let k, l be Integer; :: thesis: ( k gcd l = 1 implies ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) )
assume k gcd l = 1 ; :: thesis: ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
then A1: k,l are_relative_prime by INT_2:def 4;
then A2: k,l |^ b are_relative_prime by Th15;
k |^ a,l |^ b are_relative_prime by A1, Th16;
hence ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) by A2, INT_2:def 4; :: thesis: verum