Proof of Properties of Real Powers

Every power $t^{a}$ with $t>0$ is $\exp(a\log t)$ by Real Powers (i), and every power $0^{a}$ with $a>0$ is $0$ by Real Powers (ii); the rules for $\exp$ are those of Basic Properties of the Exponential Function.

Natural exponents. Let $t>0$. For $n=0$, $t^{0}=\exp(0)=1$ by Basic Properties of the Exponential Function (i), and $1$ is the power $t^{0}$ of Powers with Exponents in the Natural Numbers with Zero (ii). For $n\in\mathbb{N}$ we show $\exp(n\log t)=t^{n}$, the right side being the power of Powers with Exponents in the Natural Numbers with Zero (i), by induction on $n$ (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)). For $n=1$, $\exp(\log t)=t=t^{1}$ by The Natural Logarithm (ii) and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii). If $\exp(n\log t)=t^{n}$, then, the sum $n+1$ being the same in $\mathbb{N}$ and in $\mathbb{R}$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi)),

$$\exp\bigl((n+1)\log t\bigr)=\exp(n\log t)\exp(\log t)=t^{n}\,t=t^{n+1}$$

by Basic Properties of the Exponential Function (ii), the induction hypothesis, The Natural Logarithm (ii), and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i) with Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii). Finally let $t=0$ and $n\ge1$. Then the real power is $0^{n}=0$ by Real Powers (ii), because $n>0$, and the power of Powers with Exponents in the Natural Numbers with Zero (i) is $0^{n}=0$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii). In particular, for every $t\ge0$ the real power $t^{1}$ equals the power $t^{1}$ of Powers with Exponents in the Natural Numbers with Zero (i), which is $t$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii); so $t^{1}=t$.

Sign. For $t>0$, $t^{a}=\exp(a\log t)>0$ by Basic Properties of the Exponential Function (iii). Since $0^{a}=0$ for $a>0$, it follows that $t^{a}\ge0$ for $t\ge0$ and $a>0$, with $t^{a}=0$ exactly when $t=0$.

Logarithm. For $t>0$, $\log t^{a}=\log\exp(a\log t)=a\log t$ by The Natural Logarithm (ii).

Exponent laws. Let $t>0$. Then $t^{a}>0$ by (ii), so $(t^{a})^{b}$ is defined, and $\log t^{a}=a\log t$ by (iii). By Basic Properties of the Exponential Function (ii) and Basic Properties of the Exponential Function (iv),

$$t^{a+b}=\exp(a\log t+b\log t)=\exp(a\log t)\exp(b\log t)=t^{a}t^{b},$$ $$(t^{a})^{b}=\exp(b\log t^{a})=\exp(ab\log t)=t^{ab},\qquad t^{-a}=\exp(-a\log t)=\frac{1}{\exp(a\log t)}=\frac{1}{t^{a}} .$$

Let now $t=0$ and $a,b>0$. Then $a+b>0$ and $ab>0$, and $0^{a+b}$, $0^{a}0^{b}$, $(0^{a})^{b}=0^{b}$ and $0^{ab}$ are all $0$.

Products and quotients. Let $s,t>0$. Then $\log(st)=\log s+\log t$ and $\log(s/t)=\log s-\log t$ by Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1 (ii) and Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1 (iii), so, by Basic Properties of the Exponential Function (ii) and Basic Properties of the Exponential Function (iv),

$$(st)^{a}=\exp(a\log s)\exp(a\log t)=s^{a}t^{a},\qquad\Bigl(\frac{s}{t}\Bigr)^{a}=\exp(a\log s)\exp(-a\log t)=\frac{s^{a}}{t^{a}} .$$

Let now $a>0$. If $s=0$ or $t=0$, then $st=0$ and both sides of the first identity are $0$, by (ii). If $s=0$ and $t>0$, then $s/t=0$ and both sides of the second identity are $0$.

Monotonicity. Let $a>0$ and $0\le s<t$. Then $t>0$, so $t^{a}>0$ by (ii). If $s=0$, then $s^{a}=0<t^{a}$. If $s>0$, then $\log s<\log t$ by Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1 (iv), hence $a\log s<a\log t$, and $s^{a}<t^{a}$ by Basic Properties of the Exponential Function (ix).

Inverse. Let $a>0$, so that $1/a>0$; by (ii), $P_{a}$ and $P_{1/a}$ are functions from $[0,\infty)$ to $[0,\infty)$. For $t>0$, (iv) and (i) give

$$(t^{a})^{1/a}=t^{a\cdot(1/a)}=t^{1}=t,\qquad (t^{1/a})^{a}=t^{(1/a)\cdot a}=t^{1}=t,$$

and for $t=0$ both sides of each identity are $0$. Thus $P_{1/a}\circ P_{a}$ and $P_{a}\circ P_{1/a}$ are the identity of $[0,\infty)$, and $P_{a}$ is bijective with inverse $P_{1/a}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (vii).

Continuity. Let $a>0$. Continuity is used in the $\varepsilon$-$\delta$ form of The Real Line: Standing Notation and Background for Calculus on Intervals (vi).

At a point $t>0$. The function $u\mapsto au$ is continuous on $\mathbb{R}$ (for $\varepsilon>0$ take $\delta=\varepsilon/(|a|+1)$), $\log$ is continuous on $(0,\infty)$ by Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1 (v), and $\exp$ is continuous on $\mathbb{R}$ by Basic Properties of the Exponential Function (viii). By the composition rule of The Real Line: Standing Notation and Background for Calculus on Intervals (vi), the function $(0,\infty)\to\mathbb{R}$, $u\mapsto\exp(a\log u)=u^{a}$, is continuous on $(0,\infty)$. Given $\varepsilon>0$, choose $\delta'>0$ such that every $u>0$ with $|u-t|<\delta'$ satisfies $|u^{a}-t^{a}|<\varepsilon$, and put $\delta=\min\{\delta',t\}$. Every $u\in[0,\infty)$ with $|u-t|<\delta$ satisfies $u>t-t=0$, and hence $|u^{a}-t^{a}|<\varepsilon$.

At $0$. Given $\varepsilon>0$, put $\delta=\varepsilon^{1/a}$, which is positive by (ii). Every $u\in[0,\infty)$ with $|u-0|<\delta$ satisfies $0\le u<\delta$, so, by (vi) and (vii),

$$|u^{a}-0^{a}|=u^{a}<\delta^{a}=(\varepsilon^{1/a})^{a}=\varepsilon .$$

So $t\mapsto t^{a}$ is continuous on $[0,\infty)$. The absolute value $\mathbb{R}\to[0,\infty)$, $u\mapsto|u|$, is continuous on $\mathbb{R}$, since $\bigl||u|-|v|\bigr|\le|u-v|$ (take $\delta=\varepsilon$). Hence $u\mapsto|u|^{a}$, the composition of the absolute value with $t\mapsto t^{a}$, is continuous on $\mathbb{R}$, by the composition rule of The Real Line: Standing Notation and Background for Calculus on Intervals (vi) with $A=\mathbb{R}$ and $B=[0,\infty)$.