let b, n be non zero Nat; :: thesis: for a being non trivial Nat holds
( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a gcd b) |^ n) = 1 )
let a be non trivial Nat; :: thesis: ( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a gcd b) |^ n) = 1 )
( a divides b iff a |^ n divides b |^ n ) by POWD;
then ( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a |^ n) gcd (b |^ n)) = 1 ) by CD;
hence ( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a gcd b) |^ n) = 1 ) by NEWTON027; :: thesis: verum