theorem Th37: :: NUMERAL2:37

for p being Prime
for n, f, b being Nat st ex k being Nat st (b * f) + 1 = p * k & b > 1 & p,b are_coprime holds
( p divides n iff p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) )