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

end;

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

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

end;

end;