PROOF 17
Prove.
log(ab) = log a + log b
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
Fix c greater than 1. For x > 0, log x denotes the s satisfying cˢ = x.
Proof.
(1)The logarithm asks the exponent in reverse: to what power must the base be raised to give x?convention
(2)For this definition to have meaning, such an s must exist and be unique.convention
∎
Lemma L1
If x > 0, an s satisfying cˢ = x exists and is unique.
Proof.
(1)The existence of such an s is guaranteed by A3.A3
(2)Take s, t with cˢ = x and cᵗ = x.assumption
(3)If s ≠ t, then s < t or t < s.A5
(4)If s < t, then cˢ < cᵗ.A2
(5)If t < s, then cᵗ < cˢ.A2
(6)Either way, cˢ ≠ cᵗ.(4), (5), A5
(7)This contradicts cˢ = cᵗ = x. Therefore s = t.(2), (6)
∎
Theorem T
If a > 0 and b > 0, then log(ab) = log a + log b
Proof.
(1)Set s = log a, t = log b.D1, L1
(2)cˢ = a and cᵗ = b.(1), D1
(3)cˢ⁺ᵗ = cˢ cᵗA1
(4)cˢ⁺ᵗ = ab(2), (3), E
(5)ab > 0.A4
(6)The u satisfying cᵘ = ab is unique.(5), L1
(7)s + t is that u.(4), (6)
(8)log(ab) = s + t = log a + log b(1), (7), D1
∎
Remark
Can A1 be removed from this proof?
Check whether turning multiplication into addition is a property of the logarithm or of the exponent.