ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3941 on D1416: Differentiable euclidean real function
Subresult of R3942: Derivative of gaussian basic real density function
Slope function for standard real gaussian density function
Formulation 0
Let $f : \mathbb{R} \to \mathbb{R}$ be the D2719: Standard real gaussian density function.
Then
(1) $f$ is a D5614: Differentiable real function
(2) \begin{equation} f'(x) = - x f(x) \end{equation}
Proofs
Proof 0
Let $f : \mathbb{R} \to \mathbb{R}$ be the D2719: Standard real gaussian density function.
Define $g(x) : = - x^2 / 2$. From result R5265: Slope function for real monomial function of one variable, we know that $g'(x) = - x$.

Using results
(i) R5256: Slope function for composition of two differentiable real functions
(ii) R5254: Slope function for standard natural real exponential function

we now have \begin{equation} \begin{split} \frac{d f(x)}{d x} & = \frac{1}{\sqrt{2 \pi}} \frac{d \exp(g(x))}{d g(x)} \frac{d g(x)}{d x} \\ & = \frac{1}{\sqrt{2 \pi}} \exp(g(x)) \frac{d g(x)}{d x} \\ & = f(x) \frac{d g(x)}{d x} \\ & = - x f(x) \\ \end{split} \end{equation} $\square$