let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 )
take n div 3 ; :: thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 )
set w = n mod 3;
A1: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

proof

n mod 3 < 2 + 1 by NAT_D:1;
then A2: n mod 3 <= 1 + 1 by NAT_1:13;

now :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

per cases ( n mod 3 <= 1 or n mod 3 = 1 + 1 ) by A2, NAT_1:8;

suppose A3: n mod 3 <= 1 ; :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

now :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

per cases ( n mod 3 <= 0 or n mod 3 = 0 + 1 ) by A3, NAT_1:8;

suppose n mod 3 <= 0 ; :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) by NAT_1:2; :: thesis: verum

end;

suppose n mod 3 = 0 + 1 ; :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; :: thesis: verum

end;

suppose n mod 3 = 1 + 1 ; :: thesis: ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 )

hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) ; :: thesis: verum

end;

A4: n = (3 * (n div 3)) + (n mod 3) by NAT_D:2;

now :: thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 )

per cases ( n mod 3 = 0 or n mod 3 = 1 or n mod 3 = 2 ) by A1;

suppose n mod 3 = 0 ; :: thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 )

hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by A4; :: thesis: verum

end;

suppose n mod 3 = 1 ; :: thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 )

hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by NAT_D:2; :: thesis: verum

end;

suppose n mod 3 = 2 ; :: thesis: ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 )

hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) by NAT_D:2; :: thesis: verum

end;

end;

end;

hence ( n = 3 * (n div 3) or n = (3 * (n div 3)) + 1 or n = (3 * (n div 3)) + 2 ) ; :: thesis: verum