let m, n, k be Element of NAT ; :: thesis: ( ( m divides n or k = 0 ) iff k * m divides k * n )

hereby :: thesis: ( not k * m divides k * n or m divides n or k = 0 )

assume A1: ( m divides n or k = 0 ) ; :: thesis: k * m divides k * n

per cases ( m divides n or k = 0 ) by A1;

suppose m divides n ; :: thesis: k * m divides k * n

then consider k' being Nat such that
A2: n = m * k' by NAT_D:def 3;
k * n = (k * m) * k' by A2;
hence k * m divides k * n by NAT_D:def 3; :: thesis: verum

end;

suppose k = 0 ; :: thesis: k * m divides k * n

hence k * m divides k * n ; :: thesis: verum

end;

end;

end;

assume A3: k * m divides k * n ; :: thesis: ( m divides n or k = 0 )

now

assume A4: k <> 0 ; :: thesis: m divides n
consider k' being Nat such that
A5: k * n = (k * m) * k' by A3, NAT_D:def 3;
k * n = k * (m * k') by A5;
then n = m * k' by A4, XCMPLX_1:5;
hence m divides n by NAT_D:def 3; :: thesis: verum

end;

hence ( m divides n or k = 0 ) ; :: thesis: verum