For a positive integer $x$ expressed in decimals, we can write
$$ x = \sum_{k=0}^n a_k \cdot 10^k \tag{$a_k \in \{0, 1, \dots, 9\} \land a_n \neq 0$} $$
and I want to find a function $d\colon \mathbb{Z}^+ \to \mathbb{Z}^+;\, x \mapsto d(x)$ where $d(x)$ is the number of decimal digits of the positive integer $x$.
We want the following to be true. $$ \forall m \in \mathbb{Z}_{\geq 0}\;\, \Bigl(\;\!d\bigl(10^m\,\bigr) = m + 1\Bigr). \tag{1} $$
We know that $$ x \geq 10^n \tag{2} $$ or $$ (x = 10^n\;\!) \lor (x > 10^n\;\!) $$
because $$ \begin{alignat*}{99} x &= 10^n\, &&\text{ when } (a_n = 1) \,\land\, \biggl(\,\sum_{k=0}^{n-1}\;\, a_k \cdot 10^k = 0\biggr) \text{ and} \\ x &> 10^n\, &&\text{ either when } (a_n = 1) \,\land\, \biggl(\,\sum_{k=0}^{n-1}\;\, a_k \cdot 10^k > 0\biggr) \\ & &&\text{ or when } (a_n > 1) \,\land\, \biggl(\,\sum_{k=0}^{n-1}\;\, a_k \cdot 10^k = 0\biggr) \\ & && \text{ or when } (a_n > 1) \,\land\, \biggl(\,\sum_{k=0}^{n-1}\;\, a_k \cdot 10^k > 0\biggr). \end{alignat*} $$
We know that $$ 10^{n+1}\; > x \tag{3} $$ or $$ 10^{n+1} - x > 0 $$
because $$ \begin{align*} \min\bigl(10^{n+1} - x\bigr) &= 10^{n+1} \;-\; \max(x) \\ &= 10^{n+1} \;-\; 9 \cdot 10^n \\ &= 10^{n+1} \;-\; (10 - 1) \cdot 10^n \\ &= 10^{n+1} \;-\; (10^{n+1} \;-\; 10^n) \\ &= 10^n > 0. \end{align*} $$
So I tried to define $d(x)$ based on $(1)$, $(2)$, and $(3)$ as follows.
$$ d(x) := \begin{cases} 1, &\text{if $10^0 \leq x < 10^1$} \\ 2, &\text{if $10^1 \leq x < 10^2$} \\ \;\!\vdots & \\ n+1, &\text{if $10^n \leq x < 10^{n+1}\;.$} \end{cases} \tag{Definition} $$
Because we want $(1)$ to hold, we make an educated guess that $d(x)$ can also be expressed as a function composition involving the $\log_{10}\,$ function because the number of digits of any non-negative powers of ten and the log base-$10$ of said powers of ten only differ by one, i.e.,
$$ d\bigl(10^m\,\bigr) - \log_{10}\,\bigl(10^m\;\bigr) = (m + 1) - m = 1. $$
We know that $\log_{10}\,$ is strictly increasing $(a < b \implies f(a) < f(b))$ which means it preserves order such that
$$ 10^n \leq x < 10^{n+1} \implies \log_{10}\,\bigl(10^n\;\bigr) \leq \log_{10}\,(x) < \log_{10}\,\bigl(10^{n+1}\;\bigr) $$ or $$ n \leq \log_{10}\,(x) < n+1 \tag{4} $$
Next, if we try to plot the first 101 pairs of $(x, d(x))$, we will get the following graph
and we can notice that the $d$ behaves similar to the floor function, $\lfloor\cdot\rfloor$, for integer inputs.
So, we make another educated guess that $d(x)$ can be expressed as a function composition not only involving the $\log_{10}\,$ function but also the $\lfloor\cdot\rfloor$ function.
We know that $\lfloor\cdot\rfloor$ is strictly increasing $(a < b \implies f(a) < f(b))$ for integer inputs and only non-decreasing $(a \leq b \implies f(a) \leq f(b))$ for non-integer inputs which means we can infer from equation $(4)$ that
$$ n \leq \log_{10}\,(x) < n + 1 \implies \lfloor n\rfloor \leq \lfloor\log_{10}\,(x)\rfloor \leq \lfloor n + 1\rfloor \tag{notice the $\leq$ on the RHS instead of $<$} $$ or $$ n \leq \lfloor\log_{10}\,(x)\rfloor \leq n + 1. \tag{5} $$
We can simplify equation $(5)$ by noticing that $\lfloor\log_{10}\,(x)\rfloor \neq n + 1$ because we can find a counterexample, $x = 10^n\,$ for instance (see equation $(2)$), where $ \lfloor\log_{10}\,(x)\rfloor = \bigl\lfloor\log_{10}\,\bigl(10^n\;\bigr)\bigr\rfloor = \lfloor n \rfloor = n \neq n + 1$. Therefore, we have
$$ n \leq \lfloor\log_{10}\,(x)\rfloor < n + 1 $$ or $$ (n = \lfloor\log_{10}\,(x)\rfloor) \lor (n < \lfloor\log_{10}\,(x)\rfloor < n + 1) \tag{6} $$
Since $\lfloor\cdot\rfloor$ maps real numbers to integers, $\lfloor\log_{10}\,(x)\rfloor \in \mathbb{Z}$ and since there are no integers between $n$ and $n+1$ we know that $\neg(n < \lfloor\log_{10}\,(x)\rfloor < n + 1)$ and so it must be true that
$$ n = \lfloor\log_{10}\,(x)\rfloor. \tag{7} $$
We can conclude that by $\text{(Definition)}$ and by equation $(7)$, the following statement holds.
$$ \forall n \in \mathbb{Z}_{\geq 0}\;\;\; \forall a_k \in \{0, 1, \dots, 9\}\;\; \forall a_n \neq 0\;\; \forall x \in \mathbb{Z}^+\quad\Bigl(\bigl(x = \sum_{k=0}^n a_k \cdot 10^k \bigr) \land \bigl(10^n \leq x < 10^{n+1}\; \bigr) \implies d(x) = n + 1 = \lfloor\log_{10}\,(x)\rfloor + 1 \Bigr) \tag*{$\blacksquare$} $$
My question is: Is this way of deriving the formula for the number of decimal digits for positive integers correct or justified? If not where did I go wrong or how can I make this derivation better/more rigorous?