let a be non zero Integer; :: thesis: for b being non trivial Nat
for c being Integer st a = (b |^ (b |-count a)) * c holds
not b divides c
let b be non trivial Nat; :: thesis: for c being Integer st a = (b |^ (b |-count a)) * c holds
not b divides c
let c be Integer; :: thesis: ( a = (b |^ (b |-count a)) * c implies not b divides c )
A0: b > 1 by Def0;
assume A1: a = (b |^ (b |-count a)) * c ; :: thesis: not b divides c
assume b divides c ; :: thesis: contradiction
then consider d being Integer such that
A2: c = b * d ;
a = ((b |^ (b |-count a)) * b) * d by A1, A2;
then b * (b |^ (b |-count a)) divides a ;
then b |^ ((b |-count a) + 1) divides a by NEWTON:6;
hence contradiction by Def6, A0; :: thesis: verum