let p be Prime; :: thesis: for a, b being non empty natural number st b divides a holds
p |-count b <= p |-count a
let a, b be non empty natural number ; :: thesis: ( b divides a implies p |-count b <= p |-count a )
set x = p |-count a;
set y = p |-count b;
set z = p |-count (a div b);
assume b divides a ; :: thesis: p |-count b <= p |-count a
then A1: a = b * (a div b) by NAT_D:3;
A2: p > 1 by INT_2:def 5;
A3: a div b <> 0 by A1;
0 + 1 <= p |^ (p |-count (a div b)) by NAT_1:13;
then 1 * (p |^ (p |-count b)) <= (p |^ (p |-count (a div b))) * (p |^ (p |-count b)) by XREAL_1:68;
then p |^ (p |-count b) <= p |^ (p |-count a) by A1, A3, Th29;
hence p |-count b <= p |-count a by A2, PEPIN:71; :: thesis: verum