let k, m, n 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 A3:
k * m divides k * n
; :: thesis: ( m divides n or k = 0 )assume A1:
( m divides n or k = 0 )
; :: thesis: k * m divides k * n

end;now :: thesis: ( k <> 0 implies m divides n )

hence
( m divides n or k = 0 )
; :: thesis: verumconsider k9 being Nat such that

A4: k * n = (k * m) * k9 by A3, NAT_D:def 3;

assume A5: k <> 0 ; :: thesis: m divides n

k * n = k * (m * k9) by A4;

then n = m * k9 by A5, XCMPLX_1:5;

hence m divides n ; :: thesis: verum

end;A4: k * n = (k * m) * k9 by A3, NAT_D:def 3;

assume A5: k <> 0 ; :: thesis: m divides n

k * n = k * (m * k9) by A4;

then n = m * k9 by A5, XCMPLX_1:5;

hence m divides n ; :: thesis: verum