let p be Prime; :: thesis: for a, b being non zero Nat st b divides a holds
p |-count (a div b) = (p |-count a) -' (p |-count b)
let a, b be non zero Nat; :: thesis: ( b divides a implies p |-count (a div b) = (p |-count a) -' (p |-count b) )
set x = p |-count a;
set y = p |-count b;
set z = p |-count (a div b);
assume A1: b divides a ; :: thesis: p |-count (a div b) = (p |-count a) -' (p |-count b)
then a = b * (a div b) by NAT_D:3;
then a div b <> 0 ;
then p |-count (b * (a div b)) = (p |-count b) + (p |-count (a div b)) by Th28;
then A2: (p |-count (a div b)) + (p |-count b) = (p |-count a) + 0 by A1, NAT_D:3;
p |-count b <= p |-count a by A1, Th30;
then (p |-count b) - (p |-count b) <= (p |-count a) - (p |-count b) by XREAL_1:13;
hence p |-count (a div b) = (p |-count a) -' (p |-count b) by A2, XREAL_0:def 2; :: thesis: verum