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 ;
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 ;
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