let b be non zero Integer; :: thesis: for a being Integer st |.a.| <> 1 holds
( a |^ (|.a.| |-count |.b.|) divides b & not a |^ ((|.a.| |-count |.b.|) + 1) divides b )
let a be Integer; :: thesis: ( |.a.| <> 1 implies ( a |^ (|.a.| |-count |.b.|) divides b & not a |^ ((|.a.| |-count |.b.|) + 1) divides b ) )
assume A0: |.a.| <> 1 ; :: thesis: ( a |^ (|.a.| |-count |.b.|) divides b & not a |^ ((|.a.| |-count |.b.|) + 1) divides b )
reconsider k = |.a.|, l = |.b.| as Nat ;
A1: ( |.a.| |^ (k |-count l) = |.(a |^ (k |-count l)).| & |.a.| |^ ((k |-count l) + 1) = |.(a |^ ((k |-count l) + 1)).| ) by TAYLOR_2:1;
( k |^ (k |-count l) divides l & not k |^ ((k |-count l) + 1) divides l ) by A0, NAT_3:def 7;
hence ( a |^ (|.a.| |-count |.b.|) divides b & not a |^ ((|.a.| |-count |.b.|) + 1) divides b ) by A1, INT_2:16; :: thesis: verum