LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Real and complex modulus product and triangle inequalities

Statement

For real $x, y$ , $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ and $∣ x + y ∣ \leq ∣ x ∣ + ∣ y ∣$ . For complex $z, w$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ , and if $w \neq 0$ then $∣ z / w ∣ = ∣ z ∣ / ∣ w ∣$ .

Facts & Assumptions

Given: The ordered field and modulus definitions in Dedekind-complete ordered real field and Real intervals, complex rectangles and ball enclosures.

[L1]

Dedekind-complete ordered real field: real absolute value is $∣ x ∣ = x$ for $x \geq 0$ and $∣ x ∣ = - x$ for $x < 0$ .

[L2]

Real intervals, complex rectangles and ball enclosures: for $z = x + i y$ , $∣ z ∣ = \sqrt{x^{2} + y^{2}}$ ; for $z \neq 0$ , $1 / z = (x - i y) / (x^{2} + y^{2})$ .

[L3]

Nonnegative real square roots exist uniquely: the square root is the unique nonnegative root of each nonnegative input.

Proof

1.1givenL1algebra

By [L1], $- ∣ x ∣ \leq x \leq ∣ x ∣$ and $- ∣ y ∣ \leq y \leq ∣ y ∣$ . Adding gives $- (∣ x ∣ + ∣ y ∣) \leq x + y \leq ∣ x ∣ + ∣ y ∣$ , hence $∣ x + y ∣ \leq ∣ x ∣ + ∣ y ∣$ . The product identity follows by considering the four sign choices for $x$ and $y$ in the piecewise definition [L1].

1.2givenL2L3algebra

For $z = x + i y$ and $w = u + i v$ , expansion gives $∣ z w ∣^{2} = (x u - y v)^{2} + (x v + y u)^{2} = (x^{2} + y^{2}) (u^{2} + v^{2}) = ∣ z ∣^{2} ∣ w ∣^{2} .$ Both moduli are nonnegative by [L2], so uniqueness of nonnegative square roots [L3] gives $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ . Also, if $0 \leq a \leq b$ and $r = \sqrt{a}$ , $s = \sqrt{b}$ , then $r, s \geq 0$ . If $r > s$ , then $a - b = r^{2} - s^{2} = (r - s) (r + s) > 0$ , a contradiction. Thus the square-root map is increasing on nonnegative inputs.

2.1step 1.2L2L3algebra∎

The identity $(x^{2} + y^{2}) (u^{2} + v^{2}) - (x u + y v)^{2} = (x v - y u)^{2} \geq 0.$ Thus $(x u + y v)^{2} \leq ∣ z ∣^{2} ∣ w ∣^{2}$ . The increasing property proved in step 1.2 gives $∣ x u + y v ∣ \leq ∣ z ∣ ∣ w ∣$ , hence $x u + y v \leq ∣ z ∣ ∣ w ∣$ . Thus $∣ z + w ∣^{2} = ∣ z ∣^{2} + ∣ w ∣^{2} + 2 (x u + y v) \leq (∣ z ∣ + ∣ w ∣)^{2}$ ; applying the same increasing property gives $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ . By the reciprocal formula in [L2], $w (1 / w) = (u + i v) (u - i v) / (u^{2} + v^{2}) = 1$ . Step 1.2 gives $∣ w ∣ ∣ 1 / w ∣ = ∣ 1 ∣ = 1$ . Here $∣ w ∣ > 0$ : otherwise $u^{2} + v^{2} = 0$ forces $u = v = 0$ because each square is nonnegative, contrary to $w \neq 0$ . Hence $∣ 1 / w ∣ = 1 / ∣ w ∣$ , and another application of step 1.2 yields $∣ z / w ∣ = ∣ z ∣ / ∣ w ∣$ .

Depends on

Used by

Dependency tree · one level

3 results within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Steven G. Krantz, Foundations of Analysis, §1.2 (standard reference, not scraped)