let a be Nat; :: thesis: for t being Integer holds
( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )
let t be Integer; :: thesis: ( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )
assume |.t.| < a ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )
then A2: ( t < a & t > - a ) by SEQ_2:1;
per cases ( t >= 0 or t < 0 ) ;
suppose B1: t >= 0 ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )
then t mod a = t by A2, NAT_D:63;
hence ( t mod a = |.t.| or t mod a = a - |.t.| ) by B1, ABSVALUE:def 1; :: thesis: verum
end;
suppose B1: t < 0 ; :: thesis: ( t mod a = |.t.| or t mod a = a - |.t.| )
then t mod a = a + t by A2, NAT_D:63
.= a - (- t)
.= a - |.t.| by B1, ABSVALUE:def 1 ;
hence ( t mod a = |.t.| or t mod a = a - |.t.| ) ; :: thesis: verum
end;
end;