theorem :: INT_8:30

for k being Nat st k >= 3 holds
for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k