PROOF 127

Prove.

The exponential function is always positive

On the positive reals.

A way to read this proof

First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.

Definition D1

Set a¹ = a, and for a natural number n define aⁿ⁺¹ = aⁿ · a.

Proof.

These two lines determine aⁿ for every natural number n.convention

∎

Definition D2

Define a⁰ = 1.

Proof.

The value of the zero exponent is fixed by this convention.convention

∎

Definition D3

For a natural number n, define a⁻ⁿ = (aⁿ)⁻¹.

Proof.

For this convention to be meaningful, aⁿ ≠ 0 is required. That is obtained together with L1.convention

∎

Definition D4

For an integer m and a natural number n, a^(m/n) means the t > 0 satisfying tⁿ = aᵐ.

Proof.

Whether such a t exists and is unique is verified in T2.convention

∎

Lemma L1

For every natural number n, 0 < aⁿ

Proof.

(1)For n = 1, a¹ = a and 0 < a.D1, A1

(2)Suppose 0 < aⁿ for some natural number n.assumption

(3)0 < a and 0 < aⁿ, so 0 < aⁿ·a(2), A1, A2

(4)aⁿ⁺¹ = aⁿ·a, so 0 < aⁿ⁺¹(3), D1

(5)By induction, 0 < aⁿ for every natural number n.(1), (4), A9

(6)By trichotomy, aⁿ ≠ 0, so the convention of D3 is meaningful.(5), A7, D3

∎

Lemma L2

If 0 < u, then 0 < u⁻¹

Proof.

(1)0 < u, so by trichotomy u ≠ 0, and u·u⁻¹ = 1.assumption, A7, A5

(2)If u⁻¹ = 0, then u·u⁻¹ = 0, contradicting 0 < 1.(1), A6, A3, A7

(3)Suppose u⁻¹ < 0. Since 0 < u, u⁻¹·u < 0assumption, A4

(4)u⁻¹·u = u·u⁻¹ = 1, so 1 < 0, contradicting 0 < 1.(1), (3), A10, A3, A7

(5)By trichotomy, the only remaining case is 0 < u⁻¹.(2), (4), A7

∎

Theorem T1

If n is an integer, then 0 < aⁿ

Proof.

(1)If n is a natural number, then 0 < aⁿ.L1

(2)If n = 0, then a⁰ = 1 and 0 < 1.D2, A3

(3)If n is a negative integer, there is a natural number m with n = −m, and a⁻ᵐ = (aᵐ)⁻¹.D3

(4)0 < aᵐ, so 0 < (aᵐ)⁻¹(3), L1, L2

(5)The three cases cover all integers, so 0 < aⁿ for every integer n.(1), (2), (4)

∎

Theorem T2

For an integer m and a natural number n, a^(m/n) exists, is unique, and 0 < a^(m/n)

Proof.

(1)m is an integer, so 0 < aᵐ.T1

(2)There exists a unique t > 0 satisfying tⁿ = aᵐ.(1), A8

(3)By D4, a^(m/n) is that t, and t > 0.(2), D4

∎

Corollary C

For rational exponents, a^(m/n) is neither 0 nor less than 0. Therefore the graph does not meet the x-axis and does not go below it.

Proof.

(1)0 < a^(m/n)T2

(2)By trichotomy, a^(m/n) = 0 and a^(m/n) < 0 cannot also hold.(1), A7

(3)The y-coordinate of every point on the graph is always positive.(1), (2)

∎

Remark

Can A2 be removed from this proof?

Look at the four cases separately. Checking which case stands on which axiom shows what will collapse.