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 Def10; :: thesis: verum

end;

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

0 div i = 0 ;
then 0 mod i = 0 - (i * 0) by A1, Def10;
hence 0 = 0 mod i ; :: thesis: verum

end;

end;