let r be Nat; :: thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )

per cases ( l = 0 or l > 0 ) ;

suppose l = 0 ; :: thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )

hence ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) ) by INT_1:def 10; :: thesis: verum

end;

suppose A1: l > 0 ; :: thesis: ( r = k mod l iff ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) )

then A2: k = (l * (k div l)) + (k mod l) by INT_1:59;
hence ( not r = k mod l or ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) by A1, INT_1:58; :: thesis: ( ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) implies r = k mod l )
assume A3: ( ex t being Nat st
( k = (l * t) + r & r < l ) or ( r = 0 & l = 0 ) ) ; :: thesis: r = k mod l
A4: k mod l < l by A1, INT_1:58;
k mod l is Nat by Lm2;
hence r = k mod l by A2, A3, A4, NAT_1:18; :: thesis: verum

end;

end;