let a, b 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 k,l are_coprime by INT_2:def 3;
then ( k,l |^ b are_coprime & k |^ a,l |^ b are_coprime ) by Th10, Th11;
hence ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) by INT_2:def 3; :: thesis: verum