Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)
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.

vp(ab)=vp(a)+vp(b) for nonzero integers a,b, and vp(a+b)≥min⁡{vp(a),vp(b)} whenever a, b and a+b are all nonzero

Statement

Let p be a prime (Prime and composite integers: p is prime when p>1 and its only positive divisors are 1 and p) and let a,b∈Z be nonzero, with vp as in The p-adic valuation vp(a) of a nonzero integer: the greatest k∈N with pk∣a. Then ab≠0 and

vp(ab)  =  vp(a)+vp(b),

the sum taken in N (Addition of natural numbers). If moreover a+b≠0, then

vp(a+b)  ≥  min⁡{ vp(a), vp(b) },

the minimum of two natural numbers, which exists because the order on N is total (≤ is a linear order on N).

Facts & Assumptions

Given: A prime p and nonzero integers a,b; α:=vp(a) and β:=vp(b).

[L3]

If p is prime and p∣uv then p∣u or p∣v (Euclid's lemma: if p is prime and p∣ab then p∣a or p∣b).

[L5]

A product of two nonzero integers is nonzero, and xz=yz with z≠0 gives x=y (The integers have no zero divisors; multiplicative cancellation).

[L6]

Z is a commutative ring: multiplication is associative and commutative and x⋅1=x (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals); its order is total, antisymmetric and transitive (The integers form a totally ordered ring, Order on the integers, The naturals embed in the integers).

[L7]

On N: ≤ is a linear order, so any two naturals are comparable and have a minimum (≤ is a linear order on N); m≤n means m+c=n for some c (Order on the natural numbers); σ(k)=k+1 (Addition of natural numbers, The natural numbers N (von Neumann)); m<n exactly when σ(m)≤n (Discreteness: σ(n) is the immediate successor), and m<σ(n) exactly when m≤n (On N the order is membership: m<n  ⟺  m∈n).

Proof

technique · direct
1.1

ab≠0, so vp(ab) is defined.

L5
1.2

Fix a′ and b′ with a=pαa′, b=pβb′, both nonzero, and p∤a′, p∤b′.

L1choose
1.3

Now assume also a+b≠0, and put m:=min⁡{α,β}, which exists because ≤ is total on N; then m≤α and m≤β.

L7
2.1

ab=(pαa′)(pβb′)=(pαpβ)(a′b′)=pα+β(a′b′), using commutativity, associativity and the exponent law.

step 1.2L2L6
2.2

p∤a′b′: otherwise [L3] would give p∣a′ or p∣b′, both excluded by step 1.2.

step 1.2L3
2.3

By [L1], pm∣a and pm∣b, so pm∣a+b by linearity; since a+b≠0, [L1] applied to a+b gives m≤vp(a+b), which is the second assertion.

step 1.3L1L4
3.1

pα+β≠0, since ab≠0 and ab=pα+β(a′b′) would otherwise be 0.

step 1.1step 2.1L6
3.2

pα+β∣ab by step 2.1, so α+β≤vp(ab).

step 1.1step 2.1L1L4
4.1

Suppose α+β<vp(ab). Then α+β+1≤vp(ab), so pα+β+1∣ab; fix c with ab=pα+β+1c=pα+β(pc), using the exponent law. Cancelling pα+β≠0 against step 2.1 gives a′b′=pc, that is p∣a′b′, contradicting step 2.2.

step 2.1step 2.2step 3.1L1L2L4L5L7
5.1

Hence vp(ab)=α+β by totality and antisymmetry of the order on N, which is the first assertion.

step 3.2step 4.1L7
6.1

Both assertions are established.

step 5.1step 2.3∎

Remarks

Depends on

Used by

Dependency tree · two levels

68 results within two dependency steps 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