Main derivation
S01 · definition
Before
|x|
After
|x|=x\ \ (x\geq 0),\qquad |x|=-x\ \ (x<0)
Conditions: none
Rule: mko_abs_def · Uses: G1, G2, mko_abs_def
Leaf basis: mko_abs_def + order_basics
State the piecewise definition from the MKO. By trichotomy each real x satisfies exactly one of x<0, x=0, x>0, and x≥0 means x>0 or x=0; so each x falls in exactly one branch, |x| has a single value, and A really is a function ℝ→ℝ. Which branch applies depends on the sign of the number x, not on whether a minus sign appears in an expression.
S02 · implies
Before
x\geq 0
After
|x|=x\geq 0
Conditions: x\geq 0
Rule: def_unfold · Uses: S01
Leaf basis: def_unfold
Case one: x≥0. The first branch gives |x|=x, and x≥0 is the assumption of this case, so |x|≥0.
S03 · implies
Before
x<0
After
|x|=-x>0
Conditions: x<0
Rule: L_sign · Uses: S01, L_sign
Leaf basis: def_unfold + order_basics + add_inverse
Case two: x<0. The second branch gives |x|=−x, and by Lemma L_sign, x<0 implies 0<−x. So in this case |x|>0. The expression −x carries a minus sign, but the number it names is positive.
S04 · implies
Before
x\geq 0\ \lor\ x<0
After
\forall x\in\mathbb{R}:\ |x|\geq 0Conditions: none
Rule: case_analysis · Uses: S02, S03, order_basics
Leaf basis: case_analysis + order_basics + forall_intro
By trichotomy every real satisfies x≥0 or x<0; S02 gives |x|≥0 in the first case and S03 gives |x|>0, hence ≥0, in the second. Since x was arbitrary, |x|≥0 for every real x. This proves the clause '|x|≥0' of the MKO.
S05 · implies
Before
x\neq 0
After
|x|>0,\ \text{hence}\ |x|\neq 0;\ \text{so}\ |x|=0\Rightarrow x=0Conditions: none
Rule: contrapositive · Uses: S02, S03, order_basics
Leaf basis: contrapositive + case_analysis + order_basics
Suppose x≠0; then x>0 or x<0. If x>0 then |x|=x>0 (S02); if x<0 then |x|=−x>0 (S03). In both cases |x|>0, so |x|≠0. This proves x≠0 ⇒ |x|≠0, whose contrapositive is |x|=0 ⇒ x=0.
S06 · implies
Before
x=0
After
|0|=0;\ \ \text{hence}\ |x|=0\Leftrightarrow x=0Conditions: none
Rule: iff_intro · Uses: S01, S05
Leaf basis: iff_intro + def_unfold
Since 0≥0, the number 0 falls in the first branch and |0|=0, so x=0 ⇒ |x|=0. Together with S05 this gives |x|=0 ⇔ x=0: the absolute value vanishes only at 0.
S07 · implies
Before
x>0
After
|-x|=-(-x)=x=|x|
Conditions: x>0
Rule: def_unfold · Uses: S01, L_sign, L_inv_unique
Leaf basis: def_unfold + L_sign + L_inv_unique
Case x>0 of |−x|=|x|: by L_sign, −x<0, so the second branch applies to the number −x: |−x|=−(−x). By Lemma L_inv_unique, −(−x)=x, and for x>0, |x|=x. Hence |−x|=|x|.
S08 · implies
Before
x<0
After
|-x|=-x=|x|
Conditions: x<0
Rule: def_unfold · Uses: S01, L_sign
Leaf basis: def_unfold + L_sign
Case x<0: by L_sign, −x>0, so the first branch applies to −x: |−x|=−x. And for x<0, |x|=−x by the second branch. The two agree, so |−x|=|x|.
S09 · implies
Before
x>0\ \lor\ x<0\ \lor\ x=0
After
\forall x\in\mathbb{R}:\ |-x|=|x|Conditions: none
Rule: case_analysis · Uses: S07, S08, L_inv_unique
Leaf basis: case_analysis + order_basics + forall_intro
The remaining case x=0: by L_inv_unique, −0=0, so |−0|=|0|. The three cases cover every real by trichotomy, so by proof by cases and generalization, |−x|=|x| for every real x.
S10 · implies
Before
(a-b)+(b-a)
After
(a-b)+(b-a)=0,\ \text{hence}\ b-a=-(a-b)Conditions: none
Rule: L_inv_unique · Uses: L_inv_unique, add_assoc, add_comm, add_inverse, add_zero
Leaf basis: L_inv_unique + add_assoc + add_comm + add_inverse + add_zero
(a−b)+(b−a)=a+(−b)+b+(−a), which associativity and commutativity rearrange as (a+(−a))+(b+(−b))=0+0=0. By Lemma L_inv_unique with u=a−b and v=b−a, b−a=−(a−b).
S11 · implies
Before
|b-a|
After
|b-a|=|-(a-b)|=|a-b|
Conditions: none
Rule: forall_elim · Uses: S09, S10
Leaf basis: forall_elim + eq_replace
By S10 replace b−a by the equal number −(a−b), then apply S09 with x=a−b: |−(a−b)|=|a−b|. So |a−b|=|b−a| for all reals a, b: the distance between two points of the number line does not change when the endpoints are swapped.
S12 · implies
Before
|-3|
After
|-3|=-(-3)=3
Conditions: -3<0
Rule: def_unfold · Uses: S01, L_inv_unique
Leaf basis: def_unfold + L_inv_unique + numeric_evaluation
−3<0, so the second branch applies: |−3|=−(−3)=3 (L_inv_unique). The result 3 is ≥0, as S04 requires.
S13 · implies
Before
|2-7|,\ |7-2|
After
|2-7|=|-5|=5,\ \ |7-2|=|5|=5
Conditions: none
Rule: def_unfold · Uses: S01, S11
Leaf basis: def_unfold + numeric_evaluation
First compute the number inside: 2−7=−5<0, so the second branch gives |−5|=−(−5)=5; 7−2=5≥0, so the first branch gives |5|=5. They agree, as S11 says for a=2 and b=7: 2 and 7 are 5 apart on the number line.
S14 · implies
Before
\forall x\in\mathbb{R}:\ |x|=xAfter
\text{false, since}\ |-3|=3\neq -3Conditions: none
Rule: quantifier_negation · Uses: S12
Leaf basis: quantifier_negation + exists_intro + order_basics
Counterexample: the negation of 'for every real x, |x|=x' is 'some x has |x|≠x'. The number x=−3 is such an x: |−3|=3, and 3>0>−3, so 3≠−3. This counterexample refutes the equality for all x, so |x|=x cannot be used unconditionally as a general rule; this step does not derive every equality case from one example.
S15 · implies
Before
S04,\ S06,\ S09,\ S11
After
|x|\geq 0,\ \ |x|=0\Leftrightarrow x=0,\ \ |-x|=|x|,\ \ |a-b|=|b-a|
Conditions: none
Rule: and_intro_elim · Uses: S04, S06, S09, S11
Leaf basis: and_intro_elim
The four goals are established by S04, S06, S09 and S11, all resting only on the piecewise definition and on the order and addition of the reals.
Error controls and negative controls
|x| is not always x
The first mistake named by the MKO is always writing |x| as x. |x|=x is only the branch for x≥0; for x<0, |x|=−x. Counterexample: at x=−3, |x|=3 while x=−3. Before using an absolute value, decide the sign of the number inside.
Absolute value is not a rule for deleting minus signs
The second mistake named by the MKO is treating the absolute value as deleting minus signs. Deleting the minus sign in |2−7| gives 2+7=9, but 2−7=−5 and |−5|=5. Likewise, for x=−2, |−x|=|2|=2, while deleting the minus sign would give x=−2. The definition looks at the sign of the value, not at how the symbols look.
|x| is never negative, and −x need not be negative
The third mistake named by the MKO is believing |x| can be negative. The second branch reads |x|=−x and looks negative, but it is used only when x<0, and by L_sign then −x>0; for example x=−3 gives −x=3. So S04 proves |x|≥0 for every real.
- For every real x, |x|=x →
reject — At x=−3, |x|=3≠−3. - |2−7|=2+7=9 →
reject — 2−7=−5 and |−5|=5. - For every real x, |−x|=x →
reject — At x=−2, |−x|=|2|=2≠−2; the correct statement is |−x|=|x|. - Some real x has |x|<0 →
reject — S04 proves |x|≥0 for every real x. - Since a−b≠b−a when a≠b, |a−b| and |b−a| are in general different →
reject — b−a=−(a−b) and |−x|=|x| (S11); for example |2−7|=|7−2|=5.