The Logarithm and General Powers

Since it is the inverse of the continuous strictly increasing exponential, $\log$ is continuous, strictly increasing, and maps $(0,\infty)$ onto $\mathbb R$.

The equality $\exp(\log x+\log y)=\exp(\log x)\exp(\log y)=xy=\exp(\log(xy))$ and injectivity of $\exp$ give $\log(xy)=\log x+\log y$.

Since $x/y=x(1/y)$ and $\exp(-\log y)=1/y$ by [L3], step 1.2 gives $\log(x/y)=\log x-\log y$ and $\log(1/x)=-\log x$.

As $\exp(0)=1$, the inverse identity gives $\log 1=0$.

At $u=\log x$, $\exp'(u)=\exp(u)=x\ne0$; hence the inverse rule gives $\log'(x)=1/\exp(\log x)=1/x$.

The function $t\mapsto1/t$ is continuous on $(0,\infty)$, so $I(x):=\int_1^xdt/t$ satisfies $I'(x)=1/x$ and $I(1)=0$.

The difference $x\mapsto\log x-I(x)$ has derivative zero on $(0,\infty)$, and is zero at $1$, so it is identically zero.

For $q\ge1$, the product law for $\log$ gives $\log((a^{p/q})^q)=q\log(a^{p/q})=p\log a=\log(a^p)$.

Injectivity of $\log$ gives $\log(a^{p/q})=(p/q)\log a$, and exponentiating gives $a^{p/q}=\exp((p/q)\log a)$.

This is the new real power at exponent $p/q$; negative rational exponents follow by reciprocals, and the stated $0^r$ convention agrees with Rational powers $a^r$ of a positive base for $r>0$.

Expanding $a^{r+s}$ by [L1] and applying [L3] gives $a^{r+s}=\exp(r\log a)\exp(s\log a)=a^ra^s$.

Expanding $(ab)^r$ and using $\log(ab)=\log a+\log b$ gives $(ab)^r=a^rb^r$.

The same calculation with $\log(a/b)=\log a-\log b$ and [L3] gives $(a/b)^r=a^r/b^r$.

Since $\log(a^r)=\log(\exp(r\log a))=r\log a$, expanding $(a^r)^s$ gives $a^{rs}$.

The chain rule applied to $a^x=\exp(x\log a)$ gives $(a^x)'=\exp(x\log a)\log a=a^x\log a$.

The chain rule applied to $x^\alpha=\exp(\alpha\log x)$ gives $(x^\alpha)'=\exp(\alpha\log x)\alpha/x=\alpha x^{\alpha-1}$.

Both functions are continuous on their stated domains because the displayed derivatives exist there.

By [L1] and [L2], $b^{\log_bx}=\exp((\log x/\log b)\log b)=\exp(\log x)=x$.

Likewise $\log_b(b^u)=\log(\exp(u\log b))/\log b=u$.

Dividing $\log x$ first by $\log c$ and then by $\log b/\log c$ gives $\log_bx=\log_cx/\log_cb$.

Assume $a>1$. For every rational $q<x$, strict increase of $t\mapsto a^t$ gives $a^q<a^x$, so $a^x$ is an upper bound of $S_a(x)$.

Given $\varepsilon>0$, continuity of $t\mapsto a^t$ at $x$ supplies $\delta>0$ such that $|t-x|<\delta$ implies $|a^t-a^x|<\varepsilon$; density supplies rational $q$ with $x-\delta<q<x$, hence $a^x-\varepsilon<a^q\in S_a(x)$.

By the supremum characterisation, steps 1.1 and 1.2 give $a^{[x]}=a^x$ when $a>1$.

For $a=1$ both values are $1$. For $0<a<1$ the base $a^{-1}$ exceeds $1$, so step 2.1 applied to that base and the same exponent $x$ gives $(a^{-1})^{[x]}=(a^{-1})^{x}$; the subunit clause of [L1] then gives $a^{[x]}=1/\bigl((a^{-1})^{x}\bigr)$. By [L4] with $r=-1$ and $s=x$, $(a^{-1})^{x}=a^{-x}$; and by [L4] again, $a^{-x}a^{x}=a^{-x+x}=a^{0}=1$, so $1/a^{-x}=a^{x}$. Hence $a^{[x]}=a^{x}$.

For every $n$, rational-exponent agreement gives $a^{q_n}=\exp(q_n\log a)$.

Continuity of $t\mapsto a^t$ gives $a^{q_n}\to a^x$.

Since $a^{[x]}=a^x$, this limit is independent of the chosen rational sequence and has the asserted supremum value.

If $x=1$, every displayed summand is $0$, so the limit is $\log1=0$.

Suppose $x\ne1$ and put $h_n=(\log x)/2^n$. Then $h_n\to0$ and $x^{1/2^n}=\exp(h_n)$.

We have $2^n(x^{1/2^n}-1)=\log x\,(\exp(h_n)-1)/h_n$.

The derivative limit in [L2] makes the right-hand side tend to $\log x$, proving the claim together with step 1.1.

Integrating the series of [L2] from $0$ to $x$ gives $\sum_{n\ge1}(-1)^{n+1}x^n/n$.

By [L1], the integral of $1/(1+t)$ from $0$ to $x$ is $\log(1+x)$, so the displayed series formula holds for $-1<x<1$.

At $x=1$ the series is alternating harmonic and converges by [L4]; Abel's theorem and step 2.1 identify its sum with $\log2$.

At $x=-1$ every term is $-1/n$, so the series is the negative harmonic series and diverges.

By [L1], choose $N$ such that $|p_n|\le1/2$ for $n\ge N$; then $1+p_n\ge1/2>0$ on that tail.

For $|t|\le1/2$, the tail of the series in [L2] has absolute value at most $\sum_{k\ge2}|t|^k\le2t^2$, hence $|\log(1+t)-t|\le2t^2$.

Conversely, a nonzero limit of those positive tail products has a logarithm; continuity of $\log$ and the same finite-product identity make the tail logarithm partial sums converge.

Applying step 1.2 to $p_n$ and using [L3] shows that $\sum_{n\ge N}(\log(1+p_n)-p_n)$ converges absolutely.

By [L4], $\sum_n p_n$ converges if and only if $\sum_{n\ge N}\log(1+p_n)$ converges.

The $m$-th tail product equals $\exp(\sum_{n=N}^{N+m-1}\log(1+p_n))$ by repeated use of [L5], so convergence of the logarithm series gives a nonzero tail-product limit.

Steps 3.1, 4.1, and 1.3 prove both directions, and [L6] makes finite initial zero factors harmless.

Put $t=\log x$. As $x\to+\infty$, the inverse relation and [L1] give $t\to+\infty$.

By [L3], $\log x/x^\alpha=t/\exp(\alpha t)$.

The right-hand side tends to $0$ by [L2], which proves the claim.

If $p\le0$, then $1/k^p\ge1$ for $k\ge1$, so the terms do not tend to zero and the series diverges.

Suppose $p>0$ and set $f(t)=(t+1)^{-p}$. By [L2] this is nonnegative and nonincreasing on $[0,\infty)$, and its sampled series is $\sum_{k\ge0}1/(k+1)^p$.

If $p=1$, then $\int_0^Nf(t)\,dt=\log(N+1)$, which is unbounded by [L3].

If $p\ne1$, the power derivative gives $\int_0^Nf(t)\,dt=((N+1)^{1-p}-1)/(1-p)$; this is bounded exactly when $p>1$, using the exponential limits in [L3].

The integral test gives convergence exactly for $p>1$ when $p>0$, and step 1.1 handles $p\le0$.