let p be Prime; :: thesis: 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)) )
let n, f, b be Nat; :: thesis: ( ex k being Nat st (b * f) + 1 = p * k & b > 1 & p,b are_coprime implies ( p divides n iff p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) ) )
assume that
A1: ex k being Nat st (b * f) + 1 = p * k and
A2: b > 1 and
A3: p,b are_coprime ; :: thesis: ( p divides n iff p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) )
consider k being Nat such that
A4: (b * f) + 1 = p * k by A1;
thus ( p divides n implies p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) ) :: thesis: ( p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) implies p divides n )

proof

assume p divides n ; :: thesis: p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0))
then consider i being Nat such that
A5: n = p * i by NAT_D:def 3;
A6: (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0) = p * i by A2, A5, Th19;
(p * k) * ((digits (n,b)) . 0) = ((b * f) + 1) * ((digits (n,b)) . 0) by A4;
then A7: (b * ((value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)))) / b = (p * (i - (k * ((digits (n,b)) . 0)))) / b by A6;
then (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) = (p * (i - (k * ((digits (n,b)) . 0)))) / b by A2, XCMPLX_1:89;
then b divides p * (i - (k * ((digits (n,b)) . 0))) by A2, WSIERP_1:17;
then consider j being Integer such that
A8: i - (k * ((digits (n,b)) . 0)) = b * j by A3, INT_2:25, INT_1:def 3;
(value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) = (p * (b * j)) / b by A8, A7, A2, XCMPLX_1:89
.= (p * j) * (b / b)
.= (p * j) * 1 by A2, XCMPLX_1:60 ;
hence p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) by INT_1:def 3; :: thesis: verum

end;

assume p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) ; :: thesis: p divides n
then consider i being Integer such that
A9: (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) - (f * ((digits (n,b)) . 0)) = p * i by INT_1:def 3;
n = (b * ((p * i) + (f * ((digits (n,b)) . 0)))) + ((digits (n,b)) . 0) by A2, A9, Th19
.= ((b * p) * i) + (((b * f) + 1) * ((digits (n,b)) . 0))
.= ((b * p) * i) + ((p * k) * ((digits (n,b)) . 0)) by A4
.= p * ((b * i) + (k * ((digits (n,b)) . 0))) ;
hence p divides n by INT_1:def 3; :: thesis: verum