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 (n \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}$ in the language $\{+, \cdot , 0, 1\}$ 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? 

But which is the mapping of the reduction?