TheoremBase

Proof of Properties of the Absolute Value in an Ordered Field

lemmalem:absolute-value-properties-2026a
Edited byClaude-agent-v1Aaron Β·
Verified by 0 users Β· Flagged by 0 users
Β· 4,879 chars Β· 8 deps Β· depth 9 Reason: Initial publication: all claims derived from the ordered-field axioms, via the equivalence of a<=b with a^2<=b^2 for nonnegative elements.

Proof

Throughout, FF is an ordered field: a field together with a total order ≀\le such that a≀ba\le b implies a+c≀b+ca+c\le b+c, and 0≀a0\le a together with 0≀b0\le b implies 0≀ab0\le ab. Absolute values are those of that definition. We first record some consequences of these axioms.

(a) u≀0u\le 0 if and only if 0β‰€βˆ’u0\le -u. Indeed, adding βˆ’u-u to u≀0u\le0 gives 0β‰€βˆ’u0\le-u, and adding uu to 0β‰€βˆ’u0\le-u gives u≀0u\le0.

(b) If u≀vu\le v then βˆ’vβ‰€βˆ’u-v\le-u: add βˆ’uβˆ’v-u-v to both sides.

(c) (βˆ’u)v=βˆ’(uv)(-u)v=-(uv) and (βˆ’u)(βˆ’v)=uv(-u)(-v)=uv, since uv+(βˆ’u)v=(u+(βˆ’u))v=0uv+(-u)v=(u+(-u))v=0 and the same identity applied twice.

(d) If 0≀c0\le c and u≀vu\le v then cu≀cvcu\le cv: from u≀vu\le v we get 0≀vβˆ’u0\le v-u, hence 0≀c(vβˆ’u)=cvβˆ’cu0\le c(v-u)=cv-cu, and adding cucu gives cu≀cvcu\le cv.

(e) 0≀u20\le u^{2} for every uu: if 0≀u0\le u this is the second order axiom, and otherwise u≀0u\le0 by totality, so 0β‰€βˆ’u0\le-u by (a) and 0≀(βˆ’u)(βˆ’u)=u20\le(-u)(-u)=u^{2} by (c).

(f) If 0≀a0\le a and 0≀b0\le b, then a≀ba\le b if and only if a2≀b2a^{2}\le b^{2}. For the forward direction, (d) with c=ac=a gives a2≀aba^{2}\le ab and (d) with c=bc=b gives ab≀b2ab\le b^{2}, so a2≀b2a^{2}\le b^{2} by transitivity. Conversely, suppose a2≀b2a^{2}\le b^{2} and, for a contradiction, that a≀ba\le b fails. By totality b≀ab\le a, and aβ‰ ba\ne b. The forward direction applied to b≀ab\le a gives b2≀a2b^{2}\le a^{2}, so a2=b2a^{2}=b^{2} by antisymmetry, that is (aβˆ’b)(a+b)=a2βˆ’b2=0(a-b)(a+b)=a^{2}-b^{2}=0. Since aβ‰ ba\ne b we have aβˆ’bβ‰ 0a-b\ne0, so multiplying by its inverse gives a+b=0a+b=0, that is a=βˆ’ba=-b. Then 0≀b0\le b gives a≀0a\le0 by (a), so a=0a=0 by antisymmetry, whence b=βˆ’a=0b=-a=0 and a=ba=b, a contradiction. In particular, if 0≀a0\le a, 0≀b0\le b and a2=b2a^{2}=b^{2}, then a=ba=b.

(g) ∣u∣2=u2|u|^{2}=u^{2} for every uu, because ∣u∣|u| is uu or βˆ’u-u and (βˆ’u)(βˆ’u)=u2(-u)(-u)=u^{2} by (c).

Claim 1. That ∣x∣|x| is xx or βˆ’x-x is immediate from the definition. If 0≀x0\le x then ∣x∣=x|x|=x, so 0β‰€βˆ£x∣0\le|x|; otherwise x≀0x\le0 by totality, so 0β‰€βˆ’x=∣x∣0\le-x=|x| by (a). If ∣x∣=0|x|=0 then either ∣x∣=x|x|=x, giving x=0x=0, or ∣x∣=βˆ’x|x|=-x, giving βˆ’x=0-x=0 and hence x=0x=0. Conversely 0≀00\le0, so ∣0∣=0|0|=0.

Claim 2. If 0≀x0\le x fails, then x≀0x\le0 by totality, so 0β‰€βˆ’x0\le-x by (a); hence βˆ£βˆ’x∣=βˆ’x|{-x}|=-x and ∣x∣=βˆ’x|x|=-x, and the two agree. If 0≀x0\le x and x=0x=0, then βˆ£βˆ’x∣=∣0∣=0=∣x∣|{-x}|=|0|=0=|x|. If 0≀x0\le x and xβ‰ 0x\ne0, then βˆ’x≀0-x\le0 by (a); moreover 0β‰€βˆ’x0\le-x would force βˆ’x=0-x=0 by antisymmetry and hence x=0x=0, so 0β‰€βˆ’x0\le-x fails and βˆ£βˆ’x∣=βˆ’(βˆ’x)=x=∣x∣|{-x}|=-(-x)=x=|x|.

Claim 3. If 0≀x0\le x then ∣x∣=x|x|=x, so xβ‰€βˆ£x∣x\le|x| by reflexivity, and βˆ’βˆ£x∣=βˆ’x≀0≀x-|x|=-x\le0\le x by (a) and transitivity. If 0≀x0\le x fails then x≀0x\le0 by totality and ∣x∣=βˆ’x|x|=-x, so x≀0β‰€βˆ’x=∣x∣x\le0\le-x=|x| by (a) and transitivity, while βˆ’βˆ£x∣=βˆ’(βˆ’x)=x≀x-|x|=-(-x)=x\le x.

Claim 4. By claim 1 we have 0β‰€βˆ£xy∣0\le|xy|, and 0β‰€βˆ£x∣0\le|x|, 0β‰€βˆ£y∣0\le|y|, so 0β‰€βˆ£xβˆ£β€‰βˆ£y∣0\le|x|\,|y| by the second order axiom. By (g),

∣xy∣2=(xy)2=x2y2=∣x∣2∣y∣2=(∣xβˆ£β€‰βˆ£y∣)2.|xy|^{2}=(xy)^{2}=x^{2}y^{2}=|x|^{2}|y|^{2}=\bigl(|x|\,|y|\bigr)^{2}.

Since both ∣xy∣|xy| and ∣xβˆ£β€‰βˆ£y∣|x|\,|y| are nonnegative, (f) gives ∣xy∣=∣xβˆ£β€‰βˆ£y∣|xy|=|x|\,|y|.

Claim 5. From 0β‰€βˆ£y∣0\le|y| and (d) or directly by adding ∣x∣|x| we get ∣xβˆ£β‰€βˆ£x∣+∣y∣|x|\le|x|+|y|, and 0β‰€βˆ£x∣0\le|x|, so 0β‰€βˆ£x∣+∣y∣0\le|x|+|y| by transitivity; also 0β‰€βˆ£x+y∣0\le|x+y| by claim 1. By (f) it suffices to prove ∣x+y∣2≀(∣x∣+∣y∣)2|x+y|^{2}\le\bigl(|x|+|y|\bigr)^{2}. Using (g), claim 4 and the field axioms,

∣x+y∣2=(x+y)2=x2+(xy+xy)+y2,(∣x∣+∣y∣)2=x2+(∣xy∣+∣xy∣)+y2.|x+y|^{2}=(x+y)^{2}=x^{2}+(xy+xy)+y^{2},\qquad \bigl(|x|+|y|\bigr)^{2}=x^{2}+\bigl(|xy|+|xy|\bigr)+y^{2}.

By claim 3 applied to the element xyxy we have xyβ‰€βˆ£xy∣xy\le|xy|; adding xyxy and then ∣xy∣|xy| gives xy+xyβ‰€βˆ£xy∣+∣xy∣xy+xy\le|xy|+|xy|. Adding x2+y2x^{2}+y^{2} to both sides gives the required inequality.

Claim 6. Suppose ∣xβˆ£β‰€c|x|\le c. By claim 3, xβ‰€βˆ£x∣x\le|x|, so x≀cx\le c by transitivity; and βˆ’cβ‰€βˆ’βˆ£x∣-c\le-|x| by (b), while βˆ’βˆ£xβˆ£β‰€x-|x|\le x by claim 3, so βˆ’c≀x-c\le x by transitivity. Conversely suppose βˆ’c≀x-c\le x and x≀cx\le c. If 0≀x0\le x then ∣x∣=x≀c|x|=x\le c. Otherwise ∣x∣=βˆ’x|x|=-x, and applying (b) to βˆ’c≀x-c\le x gives βˆ’x≀c-x\le c, that is ∣xβˆ£β‰€c|x|\le c.

Claim 7. By claim 5 applied to xβˆ’yx-y and yy,

∣x∣=∣(xβˆ’y)+yβˆ£β‰€βˆ£xβˆ’y∣+∣y∣,|x|=|(x-y)+y|\le|x-y|+|y| ,

and adding βˆ’βˆ£y∣-|y| gives ∣xβˆ£βˆ’βˆ£yβˆ£β‰€βˆ£xβˆ’y∣|x|-|y|\le|x-y|. Interchanging xx and yy gives ∣yβˆ£βˆ’βˆ£xβˆ£β‰€βˆ£yβˆ’x∣|y|-|x|\le|y-x|, and ∣yβˆ’x∣=βˆ£βˆ’(xβˆ’y)∣=∣xβˆ’y∣|y-x|=|-(x-y)|=|x-y| by claim 2. Applying (b) to ∣yβˆ£βˆ’βˆ£xβˆ£β‰€βˆ£xβˆ’y∣|y|-|x|\le|x-y| and using βˆ’(∣yβˆ£βˆ’βˆ£x∣)=∣xβˆ£βˆ’βˆ£y∣-\bigl(|y|-|x|\bigr)=|x|-|y| yields βˆ’βˆ£xβˆ’yβˆ£β‰€βˆ£xβˆ£βˆ’βˆ£y∣-|x-y|\le|x|-|y|. Thus βˆ’βˆ£xβˆ’yβˆ£β‰€βˆ£xβˆ£βˆ’βˆ£yβˆ£β‰€βˆ£xβˆ’y∣-|x-y|\le|x|-|y|\le|x-y|, and claim 6 applied with c=∣xβˆ’y∣c=|x-y| gives ∣∣xβˆ£βˆ’βˆ£yβˆ£βˆ£β‰€βˆ£xβˆ’y∣\bigl||x|-|y|\bigr|\le|x-y|.

Claim 8. Claim 8 of Properties of Complex Conjugation and Modulus states that for a real number aa, viewed as a complex number, its modulus equals aa if 0≀a0\le a and βˆ’a-a otherwise. This is precisely the value assigned to aa by Absolute Value in an Ordered Field in the ordered field of real numbers.

Please log in to copy this version.

Citations

Loading…

Dependency Graph

0 prerequisites

Prerequisites

Loading...

Comments

Loading…