PROOF 99
Prove.
The change-of-base formula
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
For a > 0, a ≠ 1 and x > 0, logₐ x denotes the y satisfying aʸ = x.
Proof.
(1)A2 guarantees the existence and uniqueness of such a y.A2
(2)The new base k is also taken to satisfy k > 0, k ≠ 1.convention
∎
Lemma L1
If k > 0, k ≠ 1 and a > 0, a ≠ 1, then logₖ a ≠ 0
Proof.
(1)Suppose logₖ a = 0.assumption
(2)By the definition, k⁰ = a.(1), D1
(3)k⁰ = 1.A3
(4)Therefore a = 1.(2), (3), E
(5)This contradicts a ≠ 1, so logₖ a ≠ 0.(4), assumption
∎
Theorem T
If a > 0, a ≠ 1, x > 0, k > 0, k ≠ 1, then logₐ x = logₖ x / logₖ a
Proof.
(1)Set y = logₐ x.D1
(2)aʸ = x.(1), D1
(3)Take the base-k logarithm of both sides. logₖ(aʸ) = logₖ x(2), D1, E
(4)logₖ(aʸ) = y logₖ a.A1
(5)y logₖ a = logₖ x(3), (4), E
(6)logₖ a ≠ 0.L1
(7)y = logₖ x / logₖ a(5), (6), A5
(8)logₐ x = logₖ x / logₖ a(1), (7)
∎
Corollary C
If x > 0 and x ≠ 1, then logₐ x = 1 / logₓ a
Proof.
(1)In the theorem, take the new base to be k = x.T, assumption
(2)x¹ = x, so logₓ x = 1.A4, D1
(3)logₐ x = logₓ x / logₓ a = 1 / logₓ a(1), (2)
∎
Remark
Can A1 be removed from this proof?
Find the line that connects two logarithms with different bases.