let a, b, c be Nat; :: thesis: ( a <> 1 & b <> 0 & c <> 0 & b > a |-count c implies not a |^ b divides c )
assume ( a <> 1 & b <> 0 & c <> 0 ) ; :: thesis: ( not b > a |-count c or not a |^ b divides c )
then A2: ( a |^ (a |-count c) divides c & not a |^ ((a |-count c) + 1) divides c ) by NAT_3:def 7;
assume b > a |-count c ; :: thesis: not a |^ b divides c
then b >= (a |-count c) + 1 by NAT_1:13;
then consider k being Nat such that
A3: b = ((a |-count c) + 1) + k by NAT_1:10;
a |^ b = (a |^ ((a |-count c) + 1)) * (a |^ k) by A3, NEWTON:8;
hence not a |^ b divides c by A2, INT29; :: thesis: verum