let a, b be non trivial Nat; :: thesis: for c being non zero Nat holds (a |-count b) * (b |-count c) <= a |-count c
let c be non zero Nat; :: thesis: (a |-count b) * (b |-count c) <= a |-count c
( a <> 1 & b <> 1 ) by Def0;
then A2: ( a |^ (a |-count b) divides b & b |^ (b |-count c) divides c & a |^ (a |-count c) divides c & not a |^ ((a |-count c) + 1) divides c ) by NAT_3:def 7;
then (a |^ (a |-count b)) |^ (b |-count c) divides c by LmY;
then a |^ ((a |-count b) * (b |-count c)) divides c by NEWTON:9;
then (a |-count b) * (b |-count c) < (a |-count c) + 1 by A2, LmX;
hence (a |-count b) * (b |-count c) <= a |-count c by NAT_1:13; :: thesis: verum