ThmDex – An index of mathematical definitions, results, and conjectures.
Euclidean volume function under scaling
Formulation 0
Let $\mathsf{P I} (\mathbb{R}^N)$ be a D1737: Set of real n-intervals.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Then \begin{equation} \forall \, I \in \mathsf{P I} (\mathbb{R}^N) : \forall \, \lambda \in \mathbb{R} : \mathsf{Vol}(\lambda I) = |\lambda|^N \mathsf{Vol}(I) \end{equation}
Proofs
Proof 0
Let $\mathsf{P I} (\mathbb{R}^N)$ be a D1737: Set of real n-intervals.
Let $\mathsf{Vol}$ be the D1738: Euclidean real volume function on $\mathbb{R}^N$.
Let $I \subseteq \mathbb{R}^N$ be a Euclidean real interval and let $\lambda \in \mathbb{R}$. By definition, $I$ is a finite Cartesian product of some basic real intervals $I_1, \dots, I_N$. Denote the respective endpoints of these intervals by $a_1, b_1, \dots, a_N, b_N$.

Result R2973: The four classes of real intervals under reflection shows, among other things, that a reflection of an interval preserves its length. Therefore, we may assume that $\lambda \geq 0$. Result R2972: The four classes of real intervals are each closed under dilation shows that the dilated intervals $\lambda I_1, \dots, \lambda I_N$ have respective endpoints $\lambda a_1, \lambda b_1, \dots, \lambda a_N, \lambda b_N$. In the case that $\lambda$ equals zero, we may treat all intervals as closed, without this affecting the respective lengths, so that the respective endpoints stay well-defined.

Thus, applying R2969: Euclidean real Cartesian product of scaled sets, one concludes \begin{equation} \begin{split} \mathsf{Vol}(\lambda I) & = \mathsf{Vol} \Big( \lambda \prod_{n = 1}^N I_n \Big) \\ & = \mathsf{Vol} \Big( \prod_{n = 1}^N \lambda I_n \Big) \\ & = \prod_{n = 1}^N |\lambda b_n - \lambda a_n| \\ & = |\lambda|^N \prod_{n = 1}^N |b_n - a_n| \\ & = |\lambda|^N \mathsf{Vol} \Big( \prod_{n = 1}^N I_n \Big) \\ & = |\lambda|^N \mathsf{Vol} (I) \\ \end{split} \end{equation} $\square$