let p be prime Nat; 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; ( 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
; ( 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)) )
( 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
;
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;
verum
end;
assume
p divides (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)) + (f * ((digits (n,b)) . 0))
; 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; verum