let n be Nat; :: thesis: for a being non trivial Nat
for b, c being non zero Integer st a |-count b = a |-count c & a |^ n divides b holds
a |^ n divides c
let a be non trivial Nat; :: thesis: for b, c being non zero Integer st a |-count b = a |-count c & a |^ n divides b holds
a |^ n divides c
let b, c be non zero Integer; :: thesis: ( a |-count b = a |-count c & a |^ n divides b implies a |^ n divides c )
A0: a > 1 by Def0;
assume A1: ( a |-count b = a |-count c & a |^ n divides b ) ; :: thesis: a |^ n divides c
not a |^ ((a |-count b) + 1) divides b by A0, Def6;
then (a |-count b) + 1 > n by A1, PP;
then a |-count b >= n by NAT_1:13;
then A3: a |^ n divides a |^ (a |-count b) by NEWTON:89;
a |^ (a |-count c) divides c by A0, Def6;
hence a |^ n divides c by A1, A3, INT_2:9; :: thesis: verum