theorem Th38: :: NUMERAL2:38

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)) )