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

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

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

hence i mod i = 0 by Def8; :: thesis: verum

end;

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

hence i mod i = i - ((i div i) * i) by Def8
.= i - (1 * i) by A1, Th74
.= 0 ;
:: thesis: verum

end;

end;