To show that the positive existential theory of $\mathbb{C}[t, e^{\lambda t} \mid \lambda \in \mathbb{C}]$ in the language $\{+, \cdot , ' , 0 , 1, t\}$ is undecidable we have to prove the following: $$n \in \mathbb{N} \leftrightarrow \exists x \left (x \in \mathbb{C} \land tx'=nx \land x(1)=1\right )$$

So do we have to do the following?

We suppose that the positive existential theory of $\mathbb{C}[t, e^{\lambda t} \mid \lambda \in \mathbb{C}]$ in the language $\{+, \cdot , ' , 0, 1, t\}$ is decidable, i.e., there is an algorithm that answers to positive existential questions over $(\mathbb{C}[t, e^{\lambda t} \mid \lambda \in \mathbb{C}];+, \cdot , ' , 0, 1, t)$.

We want to reduce the positive existential theory $\mathbb{N}$ into the positive existential theory of $\mathbb{C}[t, e^{\lambda t} \mid \lambda \in \mathbb{C}]$ in the language $\{+, \cdot , ' , 0, 1, t\}$.

Is this correct?