LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 \mathbb{R}$ with $a > 0$ , and let $m, p \in \mathbb{Z}$ and $n, q \in \mathbb{N}$ with $n, q \ge 1$ satisfy $m/n = p/q$ in $\mathbb{Q}$ (The rationals as equivalence classes of pairs of integers). Then

$\big(a^{1/n}\big)^{m} = \big(a^{1/q}\big)^{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 \mathbb{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 \ge 1$ with $m/n = p/q$ in $\mathbb{Q}$ .

[L1]

Roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ ): $a^{1/n}$ is the unique $s \ge 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 \ne 0$ and integers $j, k$ , $(x^{j})^{k} = x^{jk}$ and $x^{j} \ne 0$ .

[L3]

Injectivity of $x \mapsto x^{N}$ on the nonnegatives for $N \ge 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 \mathbb{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 $mq = pn$ in $\mathbb{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 $\mathbb{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 $\mathbb{Z}$ ; a positive integer is the image of a unique natural $\ge 1$ , so then $m \ge 1$ .

Proof

technique · direct

1.1

Put $u := \big(a^{1/n}\big)^{m}$ and $v := \big(a^{1/q}\big)^{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 $mq = pn$ in $\mathbb{Z}$ , and $nq \ge 1$ .

2.1

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

step 1.1L1L2

2.2

The same computation for $v$ : $v^{nq} = \big(\big(a^{1/q}\big)^{p}\big)^{nq} = \big(a^{1/q}\big)^{pnq} = \big(\big(a^{1/q}\big)^{q}\big)^{pn} = a^{pn}$ .

step 1.1L1L2

3.1

Since $mq = pn$ , the two right-hand sides agree, so $u^{nq} = a^{mq} = a^{pn} = v^{nq}$ .

step 2.1step 2.2step 1.2

4.1

Both $u$ and $v$ are positive and $nq \ge 1$ , so injectivity of $x \mapsto x^{nq}$ 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 \ge 1$ has $m > 0$ in $\mathbb{Z}$ , hence $m \ge 1$ , so $\big(0^{1/n}\big)^{m} = 0^{m} = 0$ for all of them.

step 3.1step 1.1step 1.2L1L3L5∎

Depends on

Used by

The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞ Definition
FALSE: a^m/n := (a^1/n)ᵐ extends to negative bases False statement
Laws of rational exponents Lemma
Monotonicity of r ↦ aʳ and of a ↦ aʳ Lemma

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 71 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)