let p be Prime; :: thesis: for n being non zero Nat holds
( p divides n iff p |-count n > 0 )
let n be non zero Nat; :: thesis: ( p divides n iff p |-count n > 0 )
A1: p <> 1 by INT_2:def 4;
thus ( p divides n implies p |-count n > 0 ) :: thesis: ( p |-count n > 0 implies p divides n )
proof
assume A2: p divides n ; :: thesis: p |-count n > 0
p |-count n >= 1
proof
assume p |-count n < 1 ; :: thesis: contradiction
then p |-count n = 0 by NAT_1:25;
then not p |^ (0 + 1) divides n by A1, NAT_3:def 7;
hence contradiction by A2; :: thesis: verum
end;
hence p |-count n > 0 ; :: thesis: verum
end;
assume p |-count n > 0 ; :: thesis: p divides n
then reconsider d = p |-count n as non zero Nat ;
p <> 1 by INT_2:def 4;
then p |^ d divides n by NAT_3:def 7;
then p |^ (0 + 1) divides n by NAT_3:4;
hence p divides n ; :: thesis: verum