let a, b be Nat; :: thesis: ( a <> 0 implies ( a divides b iff b / a is Element of NAT ) )
assume A1: a <> 0 ; :: thesis: ( a divides b iff b / a is Element of NAT )
A2: now :: thesis: ( a divides b implies b / a is Element of NAT )
assume a divides b ; :: thesis: b / a is Element of NAT
then consider d being Nat such that
A3: b = a * d by NAT_D:def 3;
reconsider d = d as Element of NAT by ORDINAL1:def 12;
b = a * d by A3;
hence b / a is Element of NAT by A1, XCMPLX_1:89; :: thesis: verum
end;
now :: thesis: ( b / a is Element of NAT implies a divides b )
assume b / a is Element of NAT ; :: thesis: a divides b
then reconsider d = b / a as Element of NAT ;
b = a * d by A1, XCMPLX_1:87;
hence a divides b ; :: thesis: verum
end;
hence ( a divides b iff b / a is Element of NAT ) by A2; :: thesis: verum