LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 = - (a b)$ and $(- a) (- b) = a b$

Statement

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

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, $a b + (- 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, $a b + 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 $a b + (- a) b = 0$ .

step 1.1step 1.2step 1.3

2.2

Chaining steps 1.4, 1.5, 1.6 gives $a b + 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 $a b + (- a) b = 0$ , the inverse uniqueness axiom gives $(- a) b = - (a b)$ .

step 2.1L1

3.2

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

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) = - (a b)$ into $(- a) (- b) = - (a (- b))$ gives $(- a) (- b) = - (- (a b)) = a b$ .

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 · one level

2 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

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) and (−a)(−b)=ab(−a)(−b)=ab