Definition D1
A root of ax² + bx + c = 0 (a ≠ 0) is a real number x for which substitution makes the equality hold.
Proof.
(1)a ≠ 0 is the condition for the equation to be quadratic, and is assumed in every block below.convention
(2)a − b denotes a + (−b), and a² denotes a × a. Subtraction and squaring are notation.convention
∎
Lemma L1
For all a, a × 0 = 0
Proof.
(1)0 + 0 = 0A6
(2)a(0 + 0) = a × 0(1), E
(3)a×0 + a×0 = a×0(2), A1
(4)Add −(a×0) to both sides.(3), E
(5)a×0 + (a×0 + (−(a×0))) = 0(4), A4, A7
(6)a × 0 = 0(5), A7, A6
∎
Lemma L2
For all u, v, (u + v)² = u² + 2uv + v²
Proof.
(1)(u + v)² = (u + v)(u + v)convention
(2) = u(u + v) + v(u + v)(1), A1, A3
(3) = (u² + uv) + (vu + v²)(2), A1
(4)vu = uvA3
(5)uv + uv = (1 + 1)uv = 2uvA1, A3, A8
(6)(u + v)² = u² + 2uv + v²(3), (4), (5), A4, A5
∎
Lemma L3
For a ≠ 0, ax² + bx + c = 0 and (2ax + b)² = b² − 4ac are the same condition.
Proof.
(1)Since a ≠ 0, 4a ≠ 0 and 2a ≠ 0.A11, A10
(2)Suppose ax² + bx + c = 0.assumption
(3)4a(ax² + bx + c) = 4a × 0(2), E
(4)4a × 0 = 0L1
(5)4a(ax² + bx + c) = 4a²x² + 4abx + 4acA1, A2, A3
(6)4a²x² + 4abx + 4ac = 0(3), (4), (5)
(7)Adding b² − 4ac to both sides, 4a²x² + 4abx + b² = b² − 4ac(6), E, A4, A5, A7, A6
(8)(2ax + b)² = (2ax)² + 2(2ax)b + b² = 4a²x² + 4abx + b²L2, A2, A3
(9)(2ax + b)² = b² − 4ac(7), (8)
(10)Conversely, adding 4ac − b² to both sides of (9) gives 4a(ax² + bx + c) = 0.(9), (5), (8), E, A4, A5, A7, A6
(11)Since 4a ≠ 0, multiplying both sides by (4a)⁻¹ gives ax² + bx + c = 0.(1), (10), A9, A2, A8, L1
∎
Theorem T1
If b² − 4ac ≥ 0, the roots are x = (−b ± √(b² − 4ac)) / 2a, and there are no others.
Proof.
(1)ax² + bx + c = 0 ⟺ (2ax + b)² = b² − 4acL3
(2)Since b² − 4ac ≥ 0, a unique s ≥ 0 with s² = b² − 4ac exists.assumption, A12
(3)Write that s as √(b² − 4ac).(2), convention
(4)(2ax + b)² = s²(1), (2)
(5)2ax + b = ±s(4), A13
(6)Adding −b to both sides, 2ax = −b ± s(5), E, A4, A7, A6
(7)Since 2a ≠ 0, multiplying both sides by (2a)⁻¹ gives x = (−b ± s) / 2a(6), A11, A10, A9, A2, A8
(8)(1) and (5) are all equivalences, so these two values are all the roots.(1), (5), (7)
∎
Corollary C
If b² − 4ac < 0, no real root exists.
Proof.
(1)Suppose b² − 4ac < 0.assumption
(2)If there were a root x, then (2ax + b)² = b² − 4ac.L3
(3)0 ≤ (2ax + b)²A14
(4)Then 0 ≤ b² − 4ac, contradicting (1).(2), (3)
(5)No such x exists.(4)
∎