Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

Absolute value in Z: ∣a∣≥0; ∣a∣=0 exactly when a=0; ∣−a∣=∣a∣; ∣ab∣=∣a∣ ∣b∣; −∣a∣≤a≤∣a∣; and ∣a∣≤c exactly when −c≤a≤c

Statement

Let a,b,c∈Z and let ∣⋅∣ be as in The absolute value ∣a∣ of an integer. Then

  1. ∣a∣≥0;
  2. ∣a∣=0 if and only if a=0;
  3. ∣−a∣=∣a∣;
  4. ∣ab∣=∣a∣ ∣b∣;
  5. −∣a∣≤a≤∣a∣;
  6. ∣a∣≤c if and only if −c≤a≤c.

Facts & Assumptions

Given: Integers a,b,c, and the absolute value of The absolute value ∣a∣ of an integer.

[L1]

Z is a commutative ring: addition and multiplication are associative and commutative, x+0=x, x⋅1=x, multiplication distributes over addition, and every x has an additive inverse −x; we write u−v for u+(−v). Its standard consequences are used freely: −(−x)=x, (−x)y=−(xy), (−x)(−y)=xy, x⋅0=0 and −0=0 (The integers form a commutative ring, Arithmetic on the integers).

[L2]

The order on Z is total, antisymmetric and transitive, is compatible with addition (x≤y implies x+z≤y+z), and positives are closed under multiplication (0<x and 0<y imply 0<xy); x<y means x≤y together with x≠y (The integers form a totally ordered ring, Order on the integers).

[L3]

∣x∣=x when x≥0, and ∣x∣=−x when x≤0; the second clause covers x=0 as well, since −0=0 (The absolute value ∣a∣ of an integer).

Proof

technique · cases
1.1L1L2

For every x: 0≤x if and only if −x≤0, and x≤0 if and only if 0≤−x. Adding −x to 0≤x gives −x≤0, and adding x to −x≤0 gives back 0≤x; the second equivalence is the same computation with x and −x interchanged, using −(−x)=x.

1.2L1L2

If 0≤u and 0≤v then 0≤uv. If u=0 or v=0 then uv=0; otherwise 0<u and 0<v, so 0<uv because positives are closed under multiplication.

1.3L2L3cases-exhaustive

By totality, at least one of 0≤a and a≤0 holds, and correspondingly ∣a∣=a or ∣a∣=−a; this is the case split used throughout, and it is exhaustive.

1.4assume-case nonnegL3

Case a≥0: ∣a∣=a≥0.

2.1assume-case nonposstep 1.1L3

Case a≤0: ∣a∣=−a, and 0≤−a by step 1.1, so ∣a∣≥0.

2.2step 1.3L1L3

If a=0 then ∣a∣=0 by the first clause. Conversely, if ∣a∣=0 then in the case a≥0 we get a=∣a∣=0, and in the case a≤0 we get −a=∣a∣=0, whence a=−(−a)=−0=0. This is claim 2.

2.3step 1.1L1L3

Claim 3. If a≥0 then −a≤0 by step 1.1, so ∣−a∣=−(−a)=a=∣a∣. If a≤0 then 0≤−a by step 1.1, so ∣−a∣=−a=∣a∣.

2.4assume-case posposstep 1.2L3

Claim 4, case a≥0 and b≥0: ab≥0 by step 1.2, so ∣ab∣=ab=∣a∣ ∣b∣.

2.5assume-case posnegstep 1.1step 1.2L1L3

Claim 4, case a≥0 and b≤0: 0≤−b by step 1.1, so 0≤a(−b)=−(ab) by step 1.2, hence ab≤0 by step 1.1 again; therefore ∣ab∣=−(ab)=a(−b)=∣a∣ ∣b∣.

2.6assume-case negposstep 1.1step 1.2L1L3

Claim 4, case a≤0 and b≥0: the same computation with the factors interchanged, using commutativity of multiplication, gives ∣ab∣=(−a)b=∣a∣ ∣b∣.

2.7assume-case negnegstep 1.1step 1.2L1L3

Claim 4, case a≤0 and b≤0: 0≤−a and 0≤−b by step 1.1, so 0≤(−a)(−b)=ab by step 1.2, hence ∣ab∣=ab=(−a)(−b)=∣a∣ ∣b∣.

2.8step 1.1step 1.3L1L2L3

Claim 5. If a≥0 then ∣a∣=a, so a≤∣a∣; and −∣a∣=−a≤0≤a by step 1.1, so −∣a∣≤a by transitivity. If a≤0 then ∣a∣=−a and 0≤−a by step 1.1, so a≤0≤∣a∣ by transitivity; and −∣a∣=−(−a)=a≤a.

2.9step 1.3L1L2L3

Claim 6, from right to left: suppose −c≤a≤c. If a≥0 then ∣a∣=a≤c. If a≤0 then ∣a∣=−a, and adding c−a to −c≤a gives −a≤c, that is ∣a∣≤c.

3.1step 1.3step 1.4step 2.1cases

Claim 1 holds: ∣a∣≥0 in both cases.

3.2step 1.3step 2.4step 2.5step 2.6step 2.7cases

The four sign combinations of step 2.4 to step 2.7 exhaust the possibilities by totality, so claim 4 holds for all a,b.

3.3step 2.8L1L2

Claim 6, from left to right: suppose ∣a∣≤c. Then a≤∣a∣≤c by step 2.8 and transitivity. Adding −c−∣a∣ to ∣a∣≤c gives −c≤−∣a∣, and −∣a∣≤a by step 2.8, so −c≤a by transitivity.

4.1step 3.1step 2.2step 2.3step 3.2step 2.8step 3.3step 2.9∎

Every one of the six claims is now established, claim 6 by its two halves.

Remarks

  • Claim 6 is stated with ≤ on both sides deliberately, and the strict form follows from it: ∣a∣<c holds exactly when −c<a<c. From left to right, a≤∣a∣<c and −c<−∣a∣≤a by claim 5. From right to left, −c<a<c gives ∣a∣≤c by claim 6, and ∣a∣=c is impossible, since ∣a∣ is a or −a and both a=c and −a=c are excluded by the two strict inequalities.

  • The list does not include the triangle inequality, which is not used anywhere on this page. What the proofs below actually reach for is claim 1, claim 2, claim 4 and the bound a≤∣a∣ of claim 5; claim 3 is used once, in the identification of the associate classes, and claim 6 is recorded for completeness rather than because something later needs it.

Depends on

Dependency tree · 2 levels

Sources