Does $\sin (y) + y = x^3 + x$ determine $y$ as a function of $x$? I was teaching my calculus class, and we were learning implicit differentiation. I learned it quite differently when I was at school, but regardless we found that $\sin (y) + y = x^3 + x$ has the derivative $\frac{dy}{dx} = \frac{3x^2 + 1}{\cos (y)+1}$, and is therefore vertical when $y = (2k+1)\pi$ for all integers $k$. However, this only occurs locally at a single point, and while we're unable to find a function $y = f(x)$ (or vice versa) that would allow us to find a value of $x$ for the aforementioned value of $y$, I'm inclined to believe that it's a function. My students were very curious about the idea (even though it was slightly off topic, we were tryin to find the tangent line at $(0,0)$ ) and so I presented as evidence to my guess that it would be a function that the derivative never goes negative, and is only undefined at a point. How might I prove this more rigorously.
 A: It's equivalent to asking if $f(x)=\sin(x)+x$ is injective. The fact that $f$ is injective almost follows from the mean value theorem, although you need a bit of care since $f'(x)=\cos(x)+1$ hits zero. On any interval $[a,b]$, however, $f'(x)$ is nonnegative and continuous and attains a positive value, so $f(b)=f(a)+\int_a^bf'$ is strictly greater than $f(a)$.

Expanding on the first sentence: we need to make sure that, if $(x,y_1)$ and $(x,y_2)$ are solutions to $\sin(y)+y=x^3+x$, then $y_1=y_2$. Since $\sin(y_1)+y_1=\sin(y_2)+y_2$, we're really just checking that $y\mapsto \sin(y)+y$ is injective.
A: I think it's an implicitly-defined function. Let's take a look at the two sides of the equation separately.
Let $u = x^3+x$. Then, $u$ is a function of $x$, and more importantly, it's a one-to-one function. This follows pretty easily from the fact that it's strictly increasing on $\mathbb{R}$: $u'(x) = 3x^2 + 1 > 0$.
So, for any $x$ we choose in $\mathbb{R}$, there is a unique $u$ associated with it, and for any $u$ we choose in the range (also $\mathbb{R}$), there is a unique $x$ associated with it.
The same thing holds for the left-hand side. Let $v = \sin(y) + y$. Then, $v$ is strictly increasing in $y$. We can't get there using the derivative alone: $v'(y) = \cos(y)+1 \ge 0$. We'll end up with $v' = 0$ periodically (the same vertical tangents your class found).
A strictly positive derivative is sufficient for strict monotonicity, but it's not necessary. We have a weakly increasing function from the derivative, and we also know that the intercepts of $v'$ are isolated points. Together, that still gives us that for any $y_1$ and $y_2$ in $\mathbb{R}$, $y_1 < y_2 \Rightarrow v(y_1) < v(y_2)$, i.e., $v$ is strictly monotonic in $y$. This in turn means that $v$ and $y$ have a one-to-one relationship.
Then, combining the two paragraphs above, we have $u = v$, obviously strictly monotonic, therefore also one-to-one. That lets us map a one-to-one relation between $x$ and $y$: for any specific $x$, there is exactly one $u$. For any given $u$, there is exactly one $v$. And for any specific $v$, there is exactly one $y$.
