PROOF 93
Prove.
a^(1/2) is √a
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 denotes the x with x² = a and x > 0.
Proof.
(1)Such an x exists.A3
(2)This symbol refers only to the positive one of the two square roots.convention
∎
Definition D2
For rational t, aᵗ is the value fixed so that the law of exponents holds for rational exponents as well.
Proof.
(1)A1 holds when the exponents are integers.A1
(2)a^(1/2) and a^(1/4) have no meaning yet. Their values must be newly fixed.A1
(3)There is exactly one criterion for fixing them — keep the law of exponents intact up through rational exponents.A2
(4)aᵗ is determined as one real number for each rational t.(3), A2
∎
Lemma L1
(a^(1/2))² = a
Proof.
(1)(a^(1/2))² = a^((1/2)×2)D2, A2
(2)(1/2) × 2 = 1N
(3)a¹ = aA4
(4)(a^(1/2))² = a(1), (2), (3), E
∎
Lemma L2
If a > 0, then a^(1/2) > 0
Proof.
(1)a^(1/2) × a^(1/2) = aL1
(2)If a^(1/2) = 0, the left side becomes 0, giving a = 0(1), A6
(3)a > 0, so a^(1/2) ≠ 0(2), assumption
(4)a^(1/2) = a^((1/4)×2) = (a^(1/4))²D2, A2, N
(5)(a^(1/4))² ≥ 0A5
(6)a^(1/2) ≥ 0(4), (5)
(7)a^(1/2) > 0(3), (6)
∎
Lemma L3
If x² = y² and x > 0, y > 0, then x = y
Proof.
(1)x² − y² = 0assumption, E
(2)x² − y² = (x − y)(x + y)A7
(3)(x − y)(x + y) = 0(1), (2)
(4)x − y = 0 or x + y = 0(3), A8
(5)x > 0 and y > 0, so x + y > 0assumption, A9
(6)x − y = 0, that is, x = y(4), (5), E
∎
Theorem T
If a > 0, then a^(1/2) = √a
Proof.
(1)An x with x² = a and x > 0 exists, and it is √a.D1
(2)(a^(1/2))² = aL1
(3)a^(1/2) > 0L2
(4)Therefore a^(1/2) satisfies both conditions of (1).(1), (2), (3)
(5)Only one positive number satisfies those conditions.L3
(6)a^(1/2) = √a(4), (5), D1
∎
Remark
Can A2 be removed from this proof?
There are two square roots. Find where the ground for choosing one of them lies.