Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)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.

Monotonicity of r↦arr \mapsto a^{r} and of a↦ara \mapsto a^{r}

Statement

Let a∈Ra \in \mathbb{R} with a>0a > 0 and let r,s∈Qr, s \in \mathbb{Q} with r<sr < s (Order on the rationals), with rational powers as in Rational powers ara^r of a positive base.

  1. In the exponent. If a>1a > 1 then ar<asa^{r} < a^{s}; if a=1a = 1 then ar=as=1a^{r} = a^{s} = 1; if 0<a<10 < a < 1 then ar>asa^{r} > a^{s}.
  2. In the base. If r∈Qr \in \mathbb{Q} with r>0r > 0 and 0<a<b0 < a < b, then ar<bra^{r} < b^{r}; so a↦ara \mapsto a^{r} is strictly increasing on {a∈R:a>0}\{a \in \mathbb{R} : a > 0\}.
  3. Comparison with 11. For rational t>0t > 0: a>1a > 1 implies at>1a^{t} > 1, and 0<a<10 < a < 1 implies at<1a^{t} < 1.

Facts & Assumptions

Given: A real a>0a > 0 and rationals r<sr < s; write t:=s−rt := s - r, a rational with t>0t > 0.

[L1]

Positive rationals have positive representatives: t>0t > 0 can be written t=m/Nt = m/N with m,Nm, N naturals and m≥1m \ge 1, N≥1N \ge 1. Every rational has a representative with positive denominator (Every rational has a positive-denominator representative); on such a representative m/N>0m/N > 0 holds exactly when m>0m > 0 in Z\mathbb{Z} (Order on the rationals, Order on the integers); and a positive integer is the image of a unique natural ≥1\ge 1 (The naturals embed in the integers), which is what turns both the numerator m>0m > 0 and the denominator N>0N > 0 into naturals ≥1\ge 1. The last passage is a genuine step and is what Rational powers do not depend on the representative uses at its own [L5].

[L2]

Rational power laws (Laws of rational exponents, Rational powers do not depend on the representative, Rational powers ara^r of a positive base): ar>0a^{r} > 0; ar+t=arata^{r+t} = a^{r} a^{t}; and at=(a1/N)ma^{t} = \big(a^{1/N}\big)^{m} for the representative t=m/Nt = m/N.

[L3]

Roots (Existence and uniqueness of nn-th roots: a unique a1/n≥0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a): a1/Na^{1/N} is the unique x≥0x \ge 0 with xN=ax^{N} = a, and it is >0> 0 when a>0a > 0.

[L4]

Integer power monotonicity (Monotonicity of x↦xnx \mapsto x^n and of n↦ann \mapsto a^n): for N≥1N \ge 1, x↦xNx \mapsto x^{N} is strictly increasing on {x≥0}\{x \ge 0\} (claim 2); for m≥1m \ge 1, x>1x > 1 implies xm≥x>1x^{m} \ge x > 1 (claim 3), while 0≤x<10 \le x < 1 implies xm<1m=1x^{m} < 1^{m} = 1, which is claim 2 again with 11 as the larger base and NOT claim 3, whose nonstrict xm≤1x^{m} \le 1 would not suffice; and 1m=11^{m} = 1 for every integer mm, by claim 4 for natural mm together with 1−k=(1k)−1=11^{-k} = (1^{k})^{-1} = 1 (Laws of integer exponents).

[L5]

Order arithmetic: for c>0c > 0, x<y  ⟺  cx<cyx < y \iff cx < cy; and trichotomy, exactly one of a<1a < 1, a=1a = 1, a>1a > 1 holds (Sign rules for products and monotonicity of multiplication, Ordered field).

Proof

technique · cases
1.1

Write t=s−rt = s - r, so tt is rational with t>0t > 0, and fix a representative t=m/Nt = m/N with naturals m,N≥1m, N \ge 1; then as=ar+t=arata^{s} = a^{r+t} = a^{r} a^{t} with ar>0a^{r} > 0, so the comparison of asa^{s} with ara^{r} is exactly the comparison of ata^{t} with 11.

L1L2L5
1.2

Claim 2, which needs no case split: let r>0r > 0 be rational with representative r=m/Nr = m/N, m,N≥1m, N \ge 1, and let 0<a<b0 < a < b; then a1/N<b1/Na^{1/N} < b^{1/N}, since b1/N≤a1/Nb^{1/N} \le a^{1/N} would give b=(b1/N)N≤(a1/N)N=ab = \big(b^{1/N}\big)^{N} \le \big(a^{1/N}\big)^{N} = a; raising to the power mm preserves the strict inequality between nonnegatives, so ar=(a1/N)m<(b1/N)m=bra^{r} = \big(a^{1/N}\big)^{m} < \big(b^{1/N}\big)^{m} = b^{r}.

L2L3L4
2.1

Case a>1a > 1: then a1/N>1a^{1/N} > 1, because a1/N≤1a^{1/N} \le 1 would give a=(a1/N)N≤1a = \big(a^{1/N}\big)^{N} \le 1; hence at=(a1/N)m≥a1/N>1a^{t} = \big(a^{1/N}\big)^{m} \ge a^{1/N} > 1, and multiplying 1<at1 < a^{t} by ar>0a^{r} > 0 gives ar<arat=asa^{r} < a^{r} a^{t} = a^{s}.

assume-case bigstep 1.1L3L4L5
2.2

Case a=1a = 1: then 1N=11^{N} = 1 shows a1/N=1a^{1/N} = 1 by uniqueness of the nonnegative NN-th root, so au=1m′=1a^{u} = 1^{m'} = 1 for every rational uu with representative m′/N′m'/N'; in particular ar=as=1a^{r} = a^{s} = 1.

assume-case onestep 1.1L2L3L4
2.3

Case 0<a<10 < a < 1: then 0≤a1/N<10 \le a^{1/N} < 1, because a1/N≥1a^{1/N} \ge 1 would give a=(a1/N)N≥1a = \big(a^{1/N}\big)^{N} \ge 1; hence at=(a1/N)m<1m=1a^{t} = \big(a^{1/N}\big)^{m} < 1^{m} = 1 by strict monotonicity of x↦xmx \mapsto x^{m} on the nonnegatives, m≥1m \ge 1, and multiplying at<1a^{t} < 1 by ar>0a^{r} > 0 gives as=arat<ara^{s} = a^{r} a^{t} < a^{r}.

assume-case smallstep 1.1L3L4L5
3.1

The three cases a>1a > 1, a=1a = 1, 0<a<10 < a < 1 exhaust the possibilities for a>0a > 0 by trichotomy, so claim 1 holds; claim 3 is the comparison of ata^{t} with 11 established inside the first and third cases; and claim 2 is step 1.2.

cases-exhaustivestep 2.1step 2.2step 2.3step 1.2L5∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 74 results over 25 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