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
consider t being Integer such that
A2: l = k * t by A1;
per cases ( 0 < l or l = 0 ) ;
suppose 0 < l ; :: thesis: ex t being Nat st l = k * t
then 0 <= t by A2;
then reconsider t = t as Element of NAT by INT_1:3;
take t ; :: thesis: l = k * t
thus l = k * t by A2; :: thesis: verum
end;
suppose A3: l = 0 ; :: thesis: ex t being Nat st l = k * t
take 0 ; :: thesis: l = k * 0
thus l = k * 0 by A3; :: thesis: verum
end;
end;
end;
end;
assume ex t being Nat st l = k * t ; :: thesis: k divides l
hence k divides l ; :: thesis: verum