There is this simple number theory problem which says "how many 4 digit numbers that are divisible by 3 and whose digits exclude 2, 4, 6 and 9 exist?"
the solution is quite intuitive:
each digit can be either 0, 1, 3, 5, 7 or 8, except the first digit, which can't be 0.
now, say our number is $n=10x+y$. if $x\equiv0\mod{3}$, then $y$ can be either 0 or 3. if $x\equiv1\mod{3}$, then $y$ can be either 5 or 8. if $x\equiv2\mod{3}$, then $y$ can be either 1 or 4.
there are always 2 values $y$ can take, so there are $5\times6\times6\times2=360$ values of $n$.
My question is how can you formalize this solution. More precisely, write a proof with formal sybolism about: $$|\{n\in\mathbb{N}:1000\le n\le 9999\land\exists k\in\mathbb{N}(n=3k)\land\exists a,b,c,d\in\{0,1,3,5,7,8\}(n=1000a+100b+10c+d)\}|=360$$ that uses the aforementioned reasoning.
I've tried several things but still can't figure it out. Any help is appreciated :)