let a be non trivial Nat; :: thesis: for b, c being non zero Integer st a |-count b > a |-count c holds
( a |^ (a |-count c) divides b & not a |^ (a |-count b) divides c )
let b, c be non zero Integer; :: thesis: ( a |-count b > a |-count c implies ( a |^ (a |-count c) divides b & not a |^ (a |-count b) divides c ) )
A1: a > 1 by Def0;
reconsider n = a |-count b, m = a |-count c as Nat ;
assume A2: a |-count b > a |-count c ; :: thesis: ( a |^ (a |-count c) divides b & not a |^ (a |-count b) divides c )
then n >= m + 1 by NAT_1:13;
then consider k being Nat such that
A3: n = (m + 1) + k by NAT_1:10;
( not a |^ (m + 1) divides c & a |^ (m + 1) divides (a |^ (m + 1)) * (a |^ k) ) by A1, Def6;
then not (a |^ (m + 1)) * (a |^ k) divides c by INT_2:9;
then ( not a |^ n divides c & a |^ n divides b & a |^ m divides a |^ n ) by NEWTON:8, A3, A1, Def6, A2, NEWTON:89;
hence ( a |^ (a |-count c) divides b & not a |^ (a |-count b) divides c ) by INT_2:9; :: thesis: verum