Formally deriving a vacuous truth from a definition involving conjoined implications > Definition of absolute value: > > $\forall x \in \mathbb{R}, (x \geq 0 \Longrightarrow |x| = x) \wedge (x < 0 \Longrightarrow |x| = -x)$ I want to use this definition in one of my proofs. So I instantiate it below. > Let $x \in \mathbb{R}.$ Let us assume $x \geq 0$. > > Since $x \geq 0 \Longrightarrow |x| = x$, we can conclude that $|x| = x$ directly, by _modus ponendo ponens_. I believe the above statements are correct. But is the following line also correct? > Since $x < 0 \Longrightarrow |x| = -x$, we can also conclude that $|x| = -x$, as the implication is vacuously true. If so, is the justification rigorous enough? Is there a logical name for this derivation (analogous to _modus ponendo ponens_ )?

I am not exactly sure what your question is here, but hopefully this will help:

If $x \geq 0$, then given (one part of) the definition, you can then indeed infer $|x| = x$, by Modus Ponens

And yes, given that $x \geq 0$, it is indeed (vacuously) true that $x < 0 \to |x| = -x$ ... but of course you already could have gotten that from your very definition.

What does _not_ follow, however, is that $|x| = -x$. That is, just because $x < 0 \to |x| = -x$ is true does not mean that $|x| = -x$ is true.