let a, b be Nat; :: thesis: for k being Integer st b <> 0 & a * k = b holds
k is Element of NAT
let k be Integer; :: thesis: ( b <> 0 & a * k = b implies k is Element of NAT )
assume that
A1: b <> 0 and
A2: a * k = b ; :: thesis: k is Element of NAT
A3: a divides b by A2;
A4: a <> 0 by A1, A2;
then k = b / a by A2, XCMPLX_1:89;
hence k is Element of NAT by A3, A4, Lm5; :: thesis: verum