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