Implication with absolute value
Task number: 2781
In the real domain show that \((x \le y) \land (-x\le y) \Longrightarrow |x|\le y\).
Resolution
We will prove the contrapositive, i.e. \(|x|> y \Longrightarrow (x> y) \lor (-x> y)\).
For \(x\ge 0\) we have \(x=|x|>y\), whereas for \(x\le 0\) we have \(|x|=-x>y\).
