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.

Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a

Statement

Let a,b,c,d,x,y∈Z and let ∣ be divisibility (Divisibility in Z: d∣a when a=dq for some integer q). Then

  1. reflexivity: a∣a;
  2. transitivity: d∣a and a∣b imply d∣b;
  3. linearity: d∣a and d∣b imply d∣ax+by; in particular d∣a+b and d∣a−b;
  4. d∣a implies d∣ac;
  5. d∣a implies −d∣a and d∣−a.

Consequently the four statements d∣a, −d∣a, d∣−a and −d∣−a are equivalent.

Facts & Assumptions

Given: Integers a,b,c,d,x,y.

[L1]

d∣a means a=dq for some q∈Z; a=a⋅1 exhibits a∣a (Divisibility in Z: d∣a when a=dq for some integer q).

[L2]

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, with −(−x)=x, (−x)y=−(xy) and (−x)(−y)=xy; we write u−v for u+(−v) (The integers form a commutative ring, Arithmetic on the integers).

Proof

technique · direct
1.1L1L2

Reflexivity: a=a⋅1, so a∣a.

1.2L1L2

Transitivity: suppose a=dm and b=an. Then b=(dm)n=d(mn) by associativity, so d∣b.

1.3L1L2

Linearity: suppose a=dm and b=dn. Then ax+by=(dm)x+(dn)y=d(mx+ny) by associativity, commutativity and distributivity, so d∣ax+by.

1.4L1L2

Clause 4: suppose a=dm. Then ac=(dm)c=d(mc), so d∣ac.

1.5L1L2

Clause 5: suppose a=dm. Then a=(−d)(−m), so −d∣a; and −a=−(dm)=d(−m), so d∣−a.

2.1step 1.3L2

The two special cases in clause 3: taking x=y=1 gives d∣a+b, and taking x=1, y=−1 gives d∣a⋅1+b⋅(−1)=a−b.

2.2step 1.5L2

The four equivalent forms: clause 5 gives d∣a⇒−d∣a and d∣a⇒d∣−a; applying each to −d in place of d, or to −a in place of a, and using −(−x)=x, gives the reverse implications, so all four statements are equivalent.

3.1step 1.1step 1.2step 1.3step 1.4step 1.5step 2.1step 2.2∎

Clauses 1 to 5 and the two consequences are established.

Remarks

Depends on

Dependency tree · 2 levels

Sources