let b be non trivial Nat; :: thesis: for a being non zero Nat holds
( b |-count a = 0 iff a mod b <> 0 )
let a be non zero Nat; :: thesis: ( b |-count a = 0 iff a mod b <> 0 )
per cases ( b |-count a <> 0 or b |-count a = 0 ) ;
suppose A1: b |-count a <> 0 ; :: thesis: ( b |-count a = 0 iff a mod b <> 0 )
then b divides a by MOB16;
hence ( b |-count a = 0 iff a mod b <> 0 ) by A1, PEPIN:6; :: thesis: verum
end;
suppose A1: b |-count a = 0 ; :: thesis: ( b |-count a = 0 iff a mod b <> 0 )
then not b divides a by MOB16;
hence ( b |-count a = 0 iff a mod b <> 0 ) by A1, PEPIN:6; :: thesis: verum
end;
end;