ThmDex – An index of mathematical definitions, results, and conjectures.
Binary subadditivity of basic real square root function

Let $x, y \in [0, \infty)$ each be an D4767: Unsigned real number.
Then $$\sqrt{x + y} \leq \sqrt{x} + \sqrt{y}$$

Let $x, y \in [0, \infty)$ each be an D4767: Unsigned real number.
Then $$(x + y)^{1/2} \leq x^{1/2} + y^{1/2}$$
Proofs
Proof 0
Let $x, y \in [0, \infty)$ each be an D4767: Unsigned real number.
If $x = 0$ or $y = 0$, then the claim clearly holds with equality, so assume that $x \neq 0 \neq y$. Then $2 \sqrt{x y} > 0$, so that $$x + y < x + 2 \sqrt{x y} + y$$ Applying result R4261: Real binomial theorem for exponent two to the expression $x + 2 \sqrt{x y} + y$ with $a : = \sqrt{x}$ and $b : = \sqrt{y}$, we have $$x + 2 \sqrt{x y} + y = (\sqrt{x} + \sqrt{y})^2$$ Thus, applying R4260: Real square root function is strictly isotone, we conclude $$\sqrt{x + y} < \sqrt{x + 2 \sqrt{x y} + y} = \sqrt{(\sqrt{x} + \sqrt{y})^2} = (\sqrt{x} + \sqrt{y})^{\frac{1}{2} \cdot 2} = \sqrt{x} + \sqrt{y}$$ $\square$