LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

Sign rules for products: $(-a)b = -(ab)$ and $(-a)(-b) = ab$

Statement

In any field $F$ (Field), for all $a, b \in F$ we have $(-a)b = -(ab)$ and $(-a)(-b) = ab$ .

Facts & Assumptions

Given: A field $F$ and elements $a, b \in F$ .

[L1]

Field axioms (Field): multiplication distributes over addition and is commutative; $x + (-x) = 0$ for every $x$ ; the additive inverse of an element is unique, so if $u + v = 0$ then $v = -u$ ; and $-(-x) = x$ .

[L2]

For every $x \in F$ , $0 \cdot x = 0$ and $x \cdot 0 = 0$ (Multiplication by zero: $0 \cdot a = 0$ , using commutativity).

Proof

technique · direct

1.1

By distributivity, $ab + (-a)b = (a + (-a)) \cdot b$ .

1.2

Since $a + (-a) = 0$ , we have $(a + (-a)) \cdot b = 0 \cdot b$ .

1.3

$0 \cdot b = 0$ .

1.4

By distributivity, $ab + a(-b) = a \cdot (b + (-b))$ .

1.5

Since $b + (-b) = 0$ , we have $a \cdot (b + (-b)) = a \cdot 0$ .

1.6

$a \cdot 0 = 0$ .

1.7

By distributivity, $(-a)(-b) + a(-b) = ((-a) + a) \cdot (-b)$ .

1.8

Since $(-a) + a = 0$ , we have $((-a) + a) \cdot (-b) = 0 \cdot (-b)$ .

1.9

$0 \cdot (-b) = 0$ .

2.1

Chaining steps 1.1, 1.2, 1.3 gives $ab + (-a)b = 0$ .

step 1.1step 1.2step 1.3

2.2

Chaining steps 1.4, 1.5, 1.6 gives $ab + a(-b) = 0$ .

step 1.4step 1.5step 1.6

2.3

Chaining steps 1.7, 1.8, 1.9 gives $(-a)(-b) + a(-b) = 0$ .

step 1.7step 1.8step 1.9

3.1

Since $ab + (-a)b = 0$ , the inverse uniqueness axiom gives $(-a)b = -(ab)$ .

step 2.1L1

3.2

Since $ab + a(-b) = 0$ , the inverse uniqueness axiom gives $a(-b) = -(ab)$ .

step 2.2L1

3.3

Since $(-a)(-b) + a(-b) = 0$ , the inverse uniqueness axiom gives $(-a)(-b) = -(a(-b))$ .

step 2.3L1

4.1

Substituting $a(-b) = -(ab)$ into $(-a)(-b) = -(a(-b))$ gives $(-a)(-b) = -(-(ab)) = ab$ .

step 3.2step 3.3L1∎

Depends on

Used by

(-1)(-1) = 1 Corollary
FALSE: a^m/n := (a^1/n)ᵐ extends to negative bases False statement
FALSE: every real number has a real square root False statement
Basic properties of the absolute value Lemma
Sign rules for products and monotonicity of multiplication Lemma
Squares of nonzero elements are positive Lemma
When ab < b for positive a, b Proposition

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 2 results over 2 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)
Elias Zakon, Mathematical Analysis: Axioms and Basic Definitions (standard reference, not scraped)

Sign rules for products: (−a)b=−(ab)(-a)b = -(ab)(−a)b=−(ab) and (−a)(−b)=ab(-a)(-b) = ab(−a)(−b)=ab