Theorem quad

Description: The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	quad.a	$$⊢\phi \to A\in ℂ$$
	quad.z	$$⊢\phi \to A\ne 0$$
	quad.b	$$⊢\phi \to B\in ℂ$$
	quad.c	$$⊢\phi \to C\in ℂ$$
	quad.x	$$⊢\phi \to X\in ℂ$$
	quad.d	$$⊢\phi \to D=B^2-4AC$$
Assertion	quad	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=\frac{-B+\sqrt{D}}{2A}\vee X=\frac{-B-\sqrt{D}}{2A}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		quad.a	$$⊢\phi \to A\in ℂ$$
2		quad.z	$$⊢\phi \to A\ne 0$$
3		quad.b	$$⊢\phi \to B\in ℂ$$
4		quad.c	$$⊢\phi \to C\in ℂ$$
5		quad.x	$$⊢\phi \to X\in ℂ$$
6		quad.d	$$⊢\phi \to D=B^2-4AC$$
7	3	sqcld	$$⊢\phi \to B^2\in ℂ$$
8		4cn	$$⊢4\in ℂ$$
9	1 4	mulcld	$$⊢\phi \to AC\in ℂ$$
10		mulcl	$$⊢\left(4\in ℂ\wedge AC\in ℂ\right)\to 4AC\in ℂ$$
11	8 9 10	sylancr	$$⊢\phi \to 4AC\in ℂ$$
12	7 11	subcld	$$⊢\phi \to B^2-4AC\in ℂ$$
13	6 12	eqeltrd	$$⊢\phi \to D\in ℂ$$
14	13	sqrtcld	$$⊢\phi \to \sqrt{D}\in ℂ$$
15	13	sqsqrtd	$$⊢\phi \to {\sqrt{D}}^2=D$$
16	15 6	eqtrd	$$⊢\phi \to {\sqrt{D}}^2=B^2-4AC$$
17	1 2 3 4 5 14 16	quad2	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=\frac{-B+\sqrt{D}}{2A}\vee X=\frac{-B-\sqrt{D}}{2A}\right)\right)$$