let a, b be non trivial Nat; :: thesis: for c being non zero Nat holds a |^ ((a |-count b) * (b |-count c)) <= c
let c be non zero Nat; :: thesis: a |^ ((a |-count b) * (b |-count c)) <= c
A1: a |^ ((a |-count b) * (b |-count c)) = (a |^ (a |-count b)) |^ (b |-count c) by NEWTON:9;
A2: (a |^ (a |-count b)) |^ (b |-count c) <= b |^ (b |-count c) by Count0, NEWTON02:41;
b |^ (b |-count c) <= c by Count0;
hence a |^ ((a |-count b) * (b |-count c)) <= c by A1, A2, XXREAL_0:2; :: thesis: verum