Theorem quad2

Description: The quadratic equation, without specifying the particular branch D to the square root. (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 ℂ$$
	quad2.d	$$⊢\phi \to D\in ℂ$$
	quad2.2	$$⊢\phi \to D^2=B^2-4AC$$
Assertion	quad2	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=\frac{-B+D}{2A}\vee X=\frac{-B-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		quad2.d	$$⊢\phi \to D\in ℂ$$
7		quad2.2	$$⊢\phi \to D^2=B^2-4AC$$
8		2cn	$$⊢2\in ℂ$$
9		mulcl	$$⊢\left(2\in ℂ\wedge A\in ℂ\right)\to 2A\in ℂ$$
10	8 1 9	sylancr	$$⊢\phi \to 2A\in ℂ$$
11	10 5	mulcld	$$⊢\phi \to 2AX\in ℂ$$
12	11 3	addcld	$$⊢\phi \to 2AX+B\in ℂ$$
13	12	sqcld	$$⊢\phi \to {\left(2AX+B\right)}^2\in ℂ$$
14	6	sqcld	$$⊢\phi \to D^2\in ℂ$$
15	13 14	subeq0ad	$$⊢\phi \to \left({\left(2AX+B\right)}^2-D^2=0\leftrightarrow {\left(2AX+B\right)}^2=D^2\right)$$
16	5	sqcld	$$⊢\phi \to X^2\in ℂ$$
17	1 16	mulcld	$$⊢\phi \to A{X}^2\in ℂ$$
18	3 5	mulcld	$$⊢\phi \to BX\in ℂ$$
19	18 4	addcld	$$⊢\phi \to BX+C\in ℂ$$
20	17 19	addcld	$$⊢\phi \to A{X}^2+BX+C\in ℂ$$
21		0cnd	$$⊢\phi \to 0\in ℂ$$
22		4cn	$$⊢4\in ℂ$$
23		mulcl	$$⊢\left(4\in ℂ\wedge A\in ℂ\right)\to 4A\in ℂ$$
24	22 1 23	sylancr	$$⊢\phi \to 4A\in ℂ$$
25	22	a1i	$$⊢\phi \to 4\in ℂ$$
26		4ne0	$$⊢4\ne 0$$
27	26	a1i	$$⊢\phi \to 4\ne 0$$
28	25 1 27 2	mulne0d	$$⊢\phi \to 4A\ne 0$$
29	20 21 24 28	mulcand	$$⊢\phi \to \left(4A\left(A{X}^2+BX+C\right)=4A\cdot 0\leftrightarrow A{X}^2+BX+C=0\right)$$
30	11	sqcld	$$⊢\phi \to {2AX}^2\in ℂ$$
31	11 3	mulcld	$$⊢\phi \to 2AXB\in ℂ$$
32		mulcl	$$⊢\left(2\in ℂ\wedge 2AXB\in ℂ\right)\to 22AXB\in ℂ$$
33	8 31 32	sylancr	$$⊢\phi \to 22AXB\in ℂ$$
34	1 4	mulcld	$$⊢\phi \to AC\in ℂ$$
35		mulcl	$$⊢\left(4\in ℂ\wedge AC\in ℂ\right)\to 4AC\in ℂ$$
36	22 34 35	sylancr	$$⊢\phi \to 4AC\in ℂ$$
37	30 33 36	addassd	$$⊢\phi \to {2AX}^2+22AXB+4AC={2AX}^2+22AXB+4AC$$
38	3	sqcld	$$⊢\phi \to B^2\in ℂ$$
39	30 33	addcld	$$⊢\phi \to {2AX}^2+22AXB\in ℂ$$
40	38 39 36	pnncand	$$⊢\phi \to B^2+\left({2AX}^2+22AXB\right)-\left(B^2-4AC\right)={2AX}^2+22AXB+4AC$$
41	10 5	sqmuld	$$⊢\phi \to {2AX}^2={2A}^2{X}^2$$
42		sq2	$$⊢2^2=4$$
43	42	a1i	$$⊢\phi \to 2^2=4$$
44	1	sqvald	$$⊢\phi \to A^2=AA$$
45	43 44	oveq12d	$$⊢\phi \to 2^2{A}^2=4AA$$
46		sqmul	$$⊢\left(2\in ℂ\wedge A\in ℂ\right)\to {2A}^2=2^2{A}^2$$
47	8 1 46	sylancr	$$⊢\phi \to {2A}^2=2^2{A}^2$$
48	25 1 1	mulassd	$$⊢\phi \to 4AA=4AA$$
49	45 47 48	3eqtr4d	$$⊢\phi \to {2A}^2=4AA$$
50	49	oveq1d	$$⊢\phi \to {2A}^2{X}^2=4AA{X}^2$$
51	24 1 16	mulassd	$$⊢\phi \to 4AA{X}^2=4AA{X}^2$$
52	41 50 51	3eqtrrd	$$⊢\phi \to 4AA{X}^2={2AX}^2$$
53	24 18 4	adddid	$$⊢\phi \to 4A\left(BX+C\right)=4ABX+4AC$$
54		2t2e4	$$⊢2\cdot 2=4$$
55	54	oveq1i	$$⊢2\cdot 2A=4A$$
56	8	a1i	$$⊢\phi \to 2\in ℂ$$
57	56 56 1	mulassd	$$⊢\phi \to 2\cdot 2A=22A$$
58	55 57	eqtr3id	$$⊢\phi \to 4A=22A$$
59	58	oveq1d	$$⊢\phi \to 4AB=22AB$$
60	56 10 3	mulassd	$$⊢\phi \to 22AB=22AB$$
61	59 60	eqtrd	$$⊢\phi \to 4AB=22AB$$
62	61	oveq1d	$$⊢\phi \to 4ABX=22ABX$$
63	10 3	mulcld	$$⊢\phi \to 2AB\in ℂ$$
64	56 63 5	mulassd	$$⊢\phi \to 22ABX=22ABX$$
65	62 64	eqtrd	$$⊢\phi \to 4ABX=22ABX$$
66	24 3 5	mulassd	$$⊢\phi \to 4ABX=4ABX$$
67	10 3 5	mul32d	$$⊢\phi \to 2ABX=2AXB$$
68	67	oveq2d	$$⊢\phi \to 22ABX=22AXB$$
69	65 66 68	3eqtr3d	$$⊢\phi \to 4ABX=22AXB$$
70	25 1 4	mulassd	$$⊢\phi \to 4AC=4AC$$
71	69 70	oveq12d	$$⊢\phi \to 4ABX+4AC=22AXB+4AC$$
72	53 71	eqtrd	$$⊢\phi \to 4A\left(BX+C\right)=22AXB+4AC$$
73	52 72	oveq12d	$$⊢\phi \to 4AA{X}^2+4A\left(BX+C\right)={2AX}^2+22AXB+4AC$$
74	37 40 73	3eqtr4rd	$$⊢\phi \to 4AA{X}^2+4A\left(BX+C\right)=B^2+\left({2AX}^2+22AXB\right)-\left(B^2-4AC\right)$$
75	24 17 19	adddid	$$⊢\phi \to 4A\left(A{X}^2+BX+C\right)=4AA{X}^2+4A\left(BX+C\right)$$
76		binom2	$$⊢\left(2AX\in ℂ\wedge B\in ℂ\right)\to {\left(2AX+B\right)}^2={2AX}^2+22AXB+B^2$$
77	11 3 76	syl2anc	$$⊢\phi \to {\left(2AX+B\right)}^2={2AX}^2+22AXB+B^2$$
78	39 38 77	comraddd	$$⊢\phi \to {\left(2AX+B\right)}^2=B^2+{2AX}^2+22AXB$$
79	78 7	oveq12d	$$⊢\phi \to {\left(2AX+B\right)}^2-D^2=B^2+\left({2AX}^2+22AXB\right)-\left(B^2-4AC\right)$$
80	74 75 79	3eqtr4d	$$⊢\phi \to 4A\left(A{X}^2+BX+C\right)={\left(2AX+B\right)}^2-D^2$$
81	24	mul01d	$$⊢\phi \to 4A\cdot 0=0$$
82	80 81	eqeq12d	$$⊢\phi \to \left(4A\left(A{X}^2+BX+C\right)=4A\cdot 0\leftrightarrow {\left(2AX+B\right)}^2-D^2=0\right)$$
83	29 82	bitr3d	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow {\left(2AX+B\right)}^2-D^2=0\right)$$
84	11 3	subnegd	$$⊢\phi \to 2AX-\left(-B\right)=2AX+B$$
85	84	oveq1d	$$⊢\phi \to {\left(2AX-\left(-B\right)\right)}^2={\left(2AX+B\right)}^2$$
86	85	eqeq1d	$$⊢\phi \to \left({\left(2AX-\left(-B\right)\right)}^2=D^2\leftrightarrow {\left(2AX+B\right)}^2=D^2\right)$$
87	15 83 86	3bitr4d	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow {\left(2AX-\left(-B\right)\right)}^2=D^2\right)$$
88	3	negcld	$$⊢\phi \to -B\in ℂ$$
89	11 88	subcld	$$⊢\phi \to 2AX-\left(-B\right)\in ℂ$$
90		sqeqor	$$⊢\left(2AX-\left(-B\right)\in ℂ\wedge D\in ℂ\right)\to \left({\left(2AX-\left(-B\right)\right)}^2=D^2\leftrightarrow \left(2AX-\left(-B\right)=D\vee 2AX-\left(-B\right)=-D\right)\right)$$
91	89 6 90	syl2anc	$$⊢\phi \to \left({\left(2AX-\left(-B\right)\right)}^2=D^2\leftrightarrow \left(2AX-\left(-B\right)=D\vee 2AX-\left(-B\right)=-D\right)\right)$$
92	11 88 6	subaddd	$$⊢\phi \to \left(2AX-\left(-B\right)=D\leftrightarrow -B+D=2AX\right)$$
93	88 6	addcld	$$⊢\phi \to -B+D\in ℂ$$
94		2ne0	$$⊢2\ne 0$$
95	94	a1i	$$⊢\phi \to 2\ne 0$$
96	56 1 95 2	mulne0d	$$⊢\phi \to 2A\ne 0$$
97	93 10 5 96	divmuld	$$⊢\phi \to \left(\frac{-B+D}{2A}=X\leftrightarrow 2AX=-B+D\right)$$
98		eqcom	$$⊢X=\frac{-B+D}{2A}\leftrightarrow \frac{-B+D}{2A}=X$$
99		eqcom	$$⊢-B+D=2AX\leftrightarrow 2AX=-B+D$$
100	97 98 99	3bitr4g	$$⊢\phi \to \left(X=\frac{-B+D}{2A}\leftrightarrow -B+D=2AX\right)$$
101	92 100	bitr4d	$$⊢\phi \to \left(2AX-\left(-B\right)=D\leftrightarrow X=\frac{-B+D}{2A}\right)$$
102	88 6	negsubd	$$⊢\phi \to -B+\left(-D\right)=-B-D$$
103	102	eqeq1d	$$⊢\phi \to \left(-B+\left(-D\right)=2AX\leftrightarrow -B-D=2AX\right)$$
104	6	negcld	$$⊢\phi \to -D\in ℂ$$
105	11 88 104	subaddd	$$⊢\phi \to \left(2AX-\left(-B\right)=-D\leftrightarrow -B+\left(-D\right)=2AX\right)$$
106	88 6	subcld	$$⊢\phi \to -B-D\in ℂ$$
107	106 10 5 96	divmuld	$$⊢\phi \to \left(\frac{-B-D}{2A}=X\leftrightarrow 2AX=-B-D\right)$$
108		eqcom	$$⊢X=\frac{-B-D}{2A}\leftrightarrow \frac{-B-D}{2A}=X$$
109		eqcom	$$⊢-B-D=2AX\leftrightarrow 2AX=-B-D$$
110	107 108 109	3bitr4g	$$⊢\phi \to \left(X=\frac{-B-D}{2A}\leftrightarrow -B-D=2AX\right)$$
111	103 105 110	3bitr4d	$$⊢\phi \to \left(2AX-\left(-B\right)=-D\leftrightarrow X=\frac{-B-D}{2A}\right)$$
112	101 111	orbi12d	$$⊢\phi \to \left(\left(2AX-\left(-B\right)=D\vee 2AX-\left(-B\right)=-D\right)\leftrightarrow \left(X=\frac{-B+D}{2A}\vee X=\frac{-B-D}{2A}\right)\right)$$
113	87 91 112	3bitrd	$$⊢\phi \to \left(A{X}^2+BX+C=0\leftrightarrow \left(X=\frac{-B+D}{2A}\vee X=\frac{-B-D}{2A}\right)\right)$$