let k, l be Nat; :: thesis: ( k divides l iff ex t being Nat st l = k * t )

hereby :: thesis: ( ex t being Nat st l = k * t implies k divides l )

assume A1: k divides l ; :: thesis: ex t being Nat st l = k * t
thus ex t being Nat st l = k * t :: thesis: verum

proof

A2: k >= 0 by NAT_1:2;
consider t being Integer such that
A3: l = k * t by A1, INT_1:def 3;

per cases ( 0 < l or l = 0 ) by NAT_1:3;

suppose 0 < l ; :: thesis: ex t being Nat st l = k * t

then 0 <= t by A3, A2, XREAL_1:131;
then reconsider t = t as Element of NAT by INT_1:3;
take t ; :: thesis: l = k * t
thus l = k * t by A3; :: thesis: verum

end;

suppose A4: l = 0 ; :: thesis: ex t being Nat st l = k * t

take 0 ; :: thesis: l = k * 0
thus l = k * 0 by A4; :: thesis: verum

end;

end;

end;

end;

assume ex t being Nat st l = k * t ; :: thesis: k divides l
hence k divides l by INT_1:def 3; :: thesis: verum