let i be Integer; :: thesis: 0 = 0 mod i

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: 0 = 0 mod i

hence 0 = 0 mod i by INT_1:def 8; :: thesis: verum

end;

suppose A1: i <> 0 ; :: thesis: 0 = 0 mod i

0 div i = 0 by INT_1:47;
then 0 mod i = 0 - (i * 0 ) by A1, INT_1:def 8;
hence 0 = 0 mod i ; :: thesis: verum

end;

end;