LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)verified 2026-07-26 (claude-opus-5)

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.

Rational powers do not depend on the representative

Statement

Let $a \in R$ with $a > 0$ , and let $m, p \in Z$ and $n, q \in N$ with $n, q \geq 1$ satisfy $m / n = p / q$ in $Q$ (The rationals as equivalence classes of pairs of integers). Then

$(a^{1 / n})^{m} = (a^{1 / q})^{p} .$

Consequently the value $a^{r}$ of Rational powers $a^{r}$ of a positive base depends only on the rational $r$ and not on the representative $m / n$ chosen for it, so Rational powers $a^{r}$ of a positive base really does define a function $(a, r) \mapsto a^{r}$ on ${a > 0} \times Q$ . The same conclusion holds in the supplementary case $a = 0$ with $r > 0$ (Order on the rationals), where every representative gives the value $0$ .

Facts & Assumptions

Given: A real $a > 0$ , integers $m, p$ , and naturals $n, q \geq 1$ with $m / n = p / q$ in $Q$ .

[L1]

Roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): $a^{1 / n}$ is the unique $s \geq 0$ with $s^{n} = a$ , and $s > 0$ when $a > 0$ ; likewise for $q$ .

[L2]

Laws of integer exponents (Laws of integer exponents, Integer powers $a^{m}$ ): for $x \neq 0$ and integers $j, k$ , $(x^{j})^{k} = x^{j k}$ and $x^{j} \neq 0$ .

[L3]

Injectivity of $x \mapsto x^{N}$ on the nonnegatives for $N \geq 1$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ); and a positive element has positive integer powers, since $x > 0$ gives $x^{k} > 0$ for $k \in N$ and $x^{- k} = (x^{k})^{- 1} > 0$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Inverses of positives are positive, and reciprocation reverses order).

[L4]

Equality of rationals (The rationals as equivalence classes of pairs of integers): $m / n = p / q$ holds exactly when $m q = p n$ in $Z$ .

[L5]

Positivity of a rational and of its numerator (Order on the rationals, Order on the integers, The naturals embed in the integers): the order on $Q$ is read off any representative with positive denominator, and on such a representative $m / n$ one has $m / n > 0$ exactly when $m > 0$ in $Z$ ; a positive integer is the image of a unique natural $\geq 1$ , so then $m \geq 1$ .

Proof

technique · direct

1.1

Put $u : = (a^{1 / n})^{m}$ and $v : = (a^{1 / q})^{p}$ ; since $a > 0$ we have $a^{1 / n} > 0$ and $a^{1 / q} > 0$ , hence $u > 0$ and $v > 0$ .

L1L3

1.2

The hypothesis $m / n = p / q$ says exactly that $m q = p n$ in $Z$ , and $n q \geq 1$ .

2.1

Raising $u$ to the power $n q$ and using the iterated-power law twice: $u^{n q} = ((a^{1 / n})^{m})^{n q} = (a^{1 / n})^{m n q} = ((a^{1 / n})^{n})^{m q} = a^{m q}$ .

step 1.1L1L2

2.2

The same computation for $v$ : $v^{n q} = ((a^{1 / q})^{p})^{n q} = (a^{1 / q})^{p n q} = ((a^{1 / q})^{q})^{p n} = a^{p n}$ .

step 1.1L1L2

3.1

Since $m q = p n$ , the two right-hand sides agree, so $u^{n q} = a^{m q} = a^{p n} = v^{n q}$ .

step 2.1step 2.2step 1.2

4.1

Both $u$ and $v$ are positive and $n q \geq 1$ , so injectivity of $x \mapsto x^{n q}$ on the nonnegatives forces $u = v$ , which is the displayed identity; hence $a^{r}$ is independent of the representative, and in the supplementary case $a = 0$ with $r > 0$ every representative $m / n$ of $r$ with $n \geq 1$ has $m > 0$ in $Z$ , hence $m \geq 1$ , so $(0^{1 / n})^{m} = 0^{m} = 0$ for all of them.

step 3.1step 1.1step 1.2L1L3L5∎

Depends on

Used by

Cited to discharge well-definedness by Rational powers aʳ of a positive base.

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

J. Lebl, Basic Analysis I (standard reference, not scraped)
Radicals and rational exponents (Emory University) (standard reference, not scraped)
Exponentiation (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §5.6 (standard reference, not scraped)