Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-04 (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.

Laws of rational exponents

Statement

Let a,b∈R with a,b>0 and let r,s∈Q, with rational powers as in Rational powers ar of a positive base. Then:

  1. ar>0.
  2. ar+s=aras.
  3. (ab)r=arbr; in particular (ab)1/N=a1/Nb1/N for every natural N≥1.
  4. a−r=(ar)−1=1/ar.
  5. (ar)s=ars.

Claims 2 and 3 persist in the supplementary case of Rational powers ar of a positive base: for a,b≥0 and rationals r,s>0 (Order on the rationals) one still has (ab)r=arbr and ar+s=aras. The two identities degenerate differently, and it is worth saying how. In the product identity, a zero base on either side makes both sides 0. In the addition identity only the base a occurs, so it degenerates only when a=0, and then both sides are 0; when a>0 that identity holds with no hypothesis on b at all.

Facts & Assumptions

Given: Reals a,b>0 and rationals r,s.

[L1]

Definition and well-definedness (Rational powers ar of a positive base, Rational powers do not depend on the representative): for ANY representative r=m/N with m∈Z and N≥1 natural, ar=(a1/N)m; and a1/N is the unique x≥0 with xN=a (Existence and uniqueness of n-th roots: a unique a1/n≥0 with (a1/n)n=a), which is >0 when a>0.

[L2]

Laws of integer exponents (Laws of integer exponents, Integer powers am): for x,y≠0 and integers j,k, xj+k=xjxk, (xj)k=xjk, (xy)j=xjyj and x−j=(xj)−1.

[L3]

Positivity and injectivity: x>0 implies xj>0 for every NATURAL j (Monotonicity of x↦xn and of n↦an, claim 1), and hence for every integer j, since x−j=(xj)−1 (Laws of integer exponents, claim 2) and the inverse of a positive element is positive (Inverses of positives are positive, and reciprocation reverses order); and x↦xN is injective on {x≥0} for N≥1 (Monotonicity of x↦xn and of n↦an, claim 2).

[L4]

Rational arithmetic (Arithmetic on the rationals, The rationals as equivalence classes of pairs of integers): any two rationals can be written with a common positive denominator, m/N+k/N=(m+k)/N, −(m/N)=(−m)/N, and (m/n)(p/q)=(mp)/(nq).

[L5]

The order on Q (The rationals form a totally ordered field, Order on the rationals) is compatible with addition, so r>0 and s>0 imply r+s>0.

[L6]

The supplementary clause of Rational powers ar of a positive base: 0t=0 for every rational t>0, while 0t is left undefined for rational t<0 and the convention 00=1 of Integer powers am is untouched. In a field, a product with a factor 0 is 0 (Multiplication by zero: 0⋅a=0).

Proof

technique · direct
1.1

Choose a common denominator: there are a natural N≥1 and integers m,k with r=m/N and s=k/N; then r+s=(m+k)/N and −r=(−m)/N.

L4
1.2

Roots of a product: for a,b>0 and N≥1 the element a1/Nb1/N is positive and satisfies (a1/Nb1/N)N=(a1/N)N(b1/N)N=ab, so by uniqueness of the nonnegative N-th root (ab)1/N=a1/Nb1/N.

L1L2L3
2.1

Claim 1: ar=(a1/N)m with a1/N>0, and a positive element has positive integer powers, so ar>0.

step 1.1L1L3
2.2

Claim 3: (ab)r=((ab)1/N)m=(a1/Nb1/N)m=(a1/N)m(b1/N)m=arbr, using the root-of-a-product identity and then the integer product law.

step 1.1step 1.2L1L2
3.1

Claim 2: ar+s=(a1/N)m+k=(a1/N)m(a1/N)k=aras, the middle equality being the integer addition law applied to the nonzero base a1/N.

step 1.1step 2.1L1L2
3.2

Claim 4: a−r=(a1/N)−m=((a1/N)m)−1=(ar)−1.

step 1.1step 2.1L1L2
3.3

Claim 5: write r=m/n and s=p/q with n,q≥1, and put x:=a1/(nq), so x>0 and xnq=a; then (xq)n=xqn=a with xq>0, so xq=a1/n by uniqueness of the nonnegative n-th root; putting z:=xm we get z>0 and zq=(xm)q=(xq)m=(a1/n)m=ar, so z is the nonnegative q-th root of ar, that is z=(ar)1/q; therefore (ar)s=((ar)1/q)p=zp=(xm)p=xmp=(a1/(nq))mp=a(mp)/(nq)=ars.

step 2.1L1L2L3L4
3.4

The supplementary nonnegative case, product identity: let a,b≥0 and let r>0 be rational; if a>0 and b>0 this is step 2.2, and otherwise a=0 or b=0, so ab=0 and the left side is 0r=0, while the right side arbr has a factor 0r=0 and is therefore 0 as well.

step 2.2L6
4.1

The supplementary nonnegative case, addition identity: the identity ar+s=aras involves the base a only, so nothing need be assumed about b; for a>0 it is step 3.1 verbatim, which uses only a>0, and both sides are then positive rather than 0; for a=0 the exponents satisfy r+s>0, so the left side is 0r+s=0 and the right side is 0⋅0=0.

step 3.1L5L6
5.1

All five claims hold for positive bases and arbitrary rational exponents, together with the two supplementary identities for nonnegative bases and positive rational exponents.

step 2.1step 3.1step 3.2step 2.2step 3.3step 3.4step 4.1∎

Depends on

Used by

Dependency tree · two levels

41 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