# Metamath Proof Explorer

Description: Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019)

Ref Expression
Hypotheses quad3.1 ${⊢}{X}\in ℂ$
quad3.2 ${⊢}{A}\in ℂ$
quad3.3 ${⊢}{A}\ne 0$
quad3.4 ${⊢}{B}\in ℂ$
quad3.5 ${⊢}{C}\in ℂ$
quad3.6 ${⊢}{A}{{X}}^{2}+{B}{X}+{C}=0$
Assertion quad3 ${⊢}\left({X}=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\vee {X}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$

### Proof

Step Hyp Ref Expression
1 quad3.1 ${⊢}{X}\in ℂ$
2 quad3.2 ${⊢}{A}\in ℂ$
3 quad3.3 ${⊢}{A}\ne 0$
4 quad3.4 ${⊢}{B}\in ℂ$
5 quad3.5 ${⊢}{C}\in ℂ$
6 quad3.6 ${⊢}{A}{{X}}^{2}+{B}{X}+{C}=0$
7 2cn ${⊢}2\in ℂ$
8 7 2 mulcli ${⊢}2{A}\in ℂ$
9 2ne0 ${⊢}2\ne 0$
10 7 2 9 3 mulne0i ${⊢}2{A}\ne 0$
11 4 8 10 divcli ${⊢}\frac{{B}}{2{A}}\in ℂ$
12 1 11 addcli ${⊢}{X}+\left(\frac{{B}}{2{A}}\right)\in ℂ$
13 8 12 sqmuli ${⊢}{2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={2{A}}^{2}{\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}$
14 1 11 binom2i ${⊢}{\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={{X}}^{2}+2{X}\left(\frac{{B}}{2{A}}\right)+{\left(\frac{{B}}{2{A}}\right)}^{2}$
15 1 sqcli ${⊢}{{X}}^{2}\in ℂ$
16 2 15 mulcli ${⊢}{A}{{X}}^{2}\in ℂ$
17 4 1 mulcli ${⊢}{B}{X}\in ℂ$
18 16 17 2 3 divdiri ${⊢}\frac{{A}{{X}}^{2}+{B}{X}}{{A}}=\left(\frac{{A}{{X}}^{2}}{{A}}\right)+\left(\frac{{B}{X}}{{A}}\right)$
19 15 2 3 divcan3i ${⊢}\frac{{A}{{X}}^{2}}{{A}}={{X}}^{2}$
20 4 1 2 3 div23i ${⊢}\frac{{B}{X}}{{A}}=\left(\frac{{B}}{{A}}\right){X}$
21 19 20 oveq12i ${⊢}\left(\frac{{A}{{X}}^{2}}{{A}}\right)+\left(\frac{{B}{X}}{{A}}\right)={{X}}^{2}+\left(\frac{{B}}{{A}}\right){X}$
22 18 21 eqtr2i ${⊢}{{X}}^{2}+\left(\frac{{B}}{{A}}\right){X}=\frac{{A}{{X}}^{2}+{B}{X}}{{A}}$
23 4 2 3 divcli ${⊢}\frac{{B}}{{A}}\in ℂ$
24 23 1 mulcomi ${⊢}\left(\frac{{B}}{{A}}\right){X}={X}\left(\frac{{B}}{{A}}\right)$
25 1 23 mulcli ${⊢}{X}\left(\frac{{B}}{{A}}\right)\in ℂ$
26 25 7 9 divcan2i ${⊢}2\left(\frac{{X}\left(\frac{{B}}{{A}}\right)}{2}\right)={X}\left(\frac{{B}}{{A}}\right)$
27 1 23 7 9 divassi ${⊢}\frac{{X}\left(\frac{{B}}{{A}}\right)}{2}={X}\left(\frac{\frac{{B}}{{A}}}{2}\right)$
28 2 3 pm3.2i ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)$
29 7 9 pm3.2i ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
30 divdiv1 ${⊢}\left({B}\in ℂ\wedge \left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\frac{{B}}{{A}}}{2}=\frac{{B}}{{A}\cdot 2}$
31 4 28 29 30 mp3an ${⊢}\frac{\frac{{B}}{{A}}}{2}=\frac{{B}}{{A}\cdot 2}$
32 2 7 mulcomi ${⊢}{A}\cdot 2=2{A}$
33 32 oveq2i ${⊢}\frac{{B}}{{A}\cdot 2}=\frac{{B}}{2{A}}$
34 31 33 eqtri ${⊢}\frac{\frac{{B}}{{A}}}{2}=\frac{{B}}{2{A}}$
35 34 oveq2i ${⊢}{X}\left(\frac{\frac{{B}}{{A}}}{2}\right)={X}\left(\frac{{B}}{2{A}}\right)$
36 27 35 eqtri ${⊢}\frac{{X}\left(\frac{{B}}{{A}}\right)}{2}={X}\left(\frac{{B}}{2{A}}\right)$
37 36 oveq2i ${⊢}2\left(\frac{{X}\left(\frac{{B}}{{A}}\right)}{2}\right)=2{X}\left(\frac{{B}}{2{A}}\right)$
38 24 26 37 3eqtr2i ${⊢}\left(\frac{{B}}{{A}}\right){X}=2{X}\left(\frac{{B}}{2{A}}\right)$
39 38 oveq2i ${⊢}{{X}}^{2}+\left(\frac{{B}}{{A}}\right){X}={{X}}^{2}+2{X}\left(\frac{{B}}{2{A}}\right)$
40 16 17 5 addassi ${⊢}{A}{{X}}^{2}+{B}{X}+{C}={A}{{X}}^{2}+{B}{X}+{C}$
41 40 eqcomi ${⊢}{A}{{X}}^{2}+{B}{X}+{C}={A}{{X}}^{2}+{B}{X}+{C}$
42 41 oveq1i ${⊢}{A}{{X}}^{2}+\left({B}{X}+{C}\right)-{C}=\left({A}{{X}}^{2}+{B}{X}\right)+{C}-{C}$
43 16 17 addcli ${⊢}{A}{{X}}^{2}+{B}{X}\in ℂ$
44 43 5 pncan3oi ${⊢}\left({A}{{X}}^{2}+{B}{X}\right)+{C}-{C}={A}{{X}}^{2}+{B}{X}$
45 42 44 eqtr2i ${⊢}{A}{{X}}^{2}+{B}{X}={A}{{X}}^{2}+\left({B}{X}+{C}\right)-{C}$
46 6 oveq1i ${⊢}{A}{{X}}^{2}+\left({B}{X}+{C}\right)-{C}=0-{C}$
47 df-neg ${⊢}-{C}=0-{C}$
48 46 47 eqtr4i ${⊢}{A}{{X}}^{2}+\left({B}{X}+{C}\right)-{C}=-{C}$
49 45 48 eqtri ${⊢}{A}{{X}}^{2}+{B}{X}=-{C}$
50 49 oveq1i ${⊢}\frac{{A}{{X}}^{2}+{B}{X}}{{A}}=\frac{-{C}}{{A}}$
51 22 39 50 3eqtr3i ${⊢}{{X}}^{2}+2{X}\left(\frac{{B}}{2{A}}\right)=\frac{-{C}}{{A}}$
52 51 oveq1i ${⊢}{{X}}^{2}+2{X}\left(\frac{{B}}{2{A}}\right)+{\left(\frac{{B}}{2{A}}\right)}^{2}=\left(\frac{-{C}}{{A}}\right)+{\left(\frac{{B}}{2{A}}\right)}^{2}$
53 14 52 eqtri ${⊢}{\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}=\left(\frac{-{C}}{{A}}\right)+{\left(\frac{{B}}{2{A}}\right)}^{2}$
54 5 negcli ${⊢}-{C}\in ℂ$
55 54 2 3 divcli ${⊢}\frac{-{C}}{{A}}\in ℂ$
56 11 sqcli ${⊢}{\left(\frac{{B}}{2{A}}\right)}^{2}\in ℂ$
57 55 56 addcomi ${⊢}\left(\frac{-{C}}{{A}}\right)+{\left(\frac{{B}}{2{A}}\right)}^{2}={\left(\frac{{B}}{2{A}}\right)}^{2}+\left(\frac{-{C}}{{A}}\right)$
58 4 8 10 sqdivi ${⊢}{\left(\frac{{B}}{2{A}}\right)}^{2}=\frac{{{B}}^{2}}{{2{A}}^{2}}$
59 4cn ${⊢}4\in ℂ$
60 59 2 mulcli ${⊢}4{A}\in ℂ$
61 4ne0 ${⊢}4\ne 0$
62 59 2 61 3 mulne0i ${⊢}4{A}\ne 0$
63 60 60 54 2 62 3 divmuldivi ${⊢}\left(\frac{4{A}}{4{A}}\right)\left(\frac{-{C}}{{A}}\right)=\frac{4{A}\left(-{C}\right)}{4{A}{A}}$
64 60 62 dividi ${⊢}\frac{4{A}}{4{A}}=1$
65 64 eqcomi ${⊢}1=\frac{4{A}}{4{A}}$
66 65 oveq1i ${⊢}1\left(\frac{-{C}}{{A}}\right)=\left(\frac{4{A}}{4{A}}\right)\left(\frac{-{C}}{{A}}\right)$
67 55 mulid2i ${⊢}1\left(\frac{-{C}}{{A}}\right)=\frac{-{C}}{{A}}$
68 66 67 eqtr3i ${⊢}\left(\frac{4{A}}{4{A}}\right)\left(\frac{-{C}}{{A}}\right)=\frac{-{C}}{{A}}$
69 5 mulm1i ${⊢}-1{C}=-{C}$
70 69 eqcomi ${⊢}-{C}=-1{C}$
71 70 oveq2i ${⊢}4{A}\left(-{C}\right)=4{A}-1{C}$
72 neg1cn ${⊢}-1\in ℂ$
73 60 72 5 mulassi ${⊢}4{A}-1{C}=4{A}-1{C}$
74 71 73 eqtr4i ${⊢}4{A}\left(-{C}\right)=4{A}-1{C}$
75 60 72 mulcomi ${⊢}4{A}-1=-14{A}$
76 75 oveq1i ${⊢}4{A}-1{C}=-14{A}{C}$
77 72 60 5 mulassi ${⊢}-14{A}{C}=-14{A}{C}$
78 74 76 77 3eqtri ${⊢}4{A}\left(-{C}\right)=-14{A}{C}$
79 59 2 5 mulassi ${⊢}4{A}{C}=4{A}{C}$
80 79 oveq2i ${⊢}-14{A}{C}=-14{A}{C}$
81 2 5 mulcli ${⊢}{A}{C}\in ℂ$
82 59 81 mulcli ${⊢}4{A}{C}\in ℂ$
83 82 mulm1i ${⊢}-14{A}{C}=-4{A}{C}$
84 78 80 83 3eqtri ${⊢}4{A}\left(-{C}\right)=-4{A}{C}$
85 2t2e4 ${⊢}2\cdot 2=4$
86 85 eqcomi ${⊢}4=2\cdot 2$
87 86 oveq1i ${⊢}4{A}=2\cdot 2{A}$
88 87 oveq1i ${⊢}4{A}{A}=2\cdot 2{A}{A}$
89 7 7 2 mulassi ${⊢}2\cdot 2{A}=22{A}$
90 89 oveq1i ${⊢}2\cdot 2{A}{A}=22{A}{A}$
91 88 90 eqtri ${⊢}4{A}{A}=22{A}{A}$
92 7 8 mulcomi ${⊢}22{A}=2{A}\cdot 2$
93 92 oveq1i ${⊢}22{A}{A}=2{A}\cdot 2{A}$
94 8 7 2 mulassi ${⊢}2{A}\cdot 2{A}=2{A}2{A}$
95 91 93 94 3eqtri ${⊢}4{A}{A}=2{A}2{A}$
96 8 sqvali ${⊢}{2{A}}^{2}=2{A}2{A}$
97 95 96 eqtr4i ${⊢}4{A}{A}={2{A}}^{2}$
98 84 97 oveq12i ${⊢}\frac{4{A}\left(-{C}\right)}{4{A}{A}}=\frac{-4{A}{C}}{{2{A}}^{2}}$
99 63 68 98 3eqtr3i ${⊢}\frac{-{C}}{{A}}=\frac{-4{A}{C}}{{2{A}}^{2}}$
100 58 99 oveq12i ${⊢}{\left(\frac{{B}}{2{A}}\right)}^{2}+\left(\frac{-{C}}{{A}}\right)=\left(\frac{{{B}}^{2}}{{2{A}}^{2}}\right)+\left(\frac{-4{A}{C}}{{2{A}}^{2}}\right)$
101 4 sqcli ${⊢}{{B}}^{2}\in ℂ$
102 82 negcli ${⊢}-4{A}{C}\in ℂ$
103 8 sqcli ${⊢}{2{A}}^{2}\in ℂ$
104 8 8 10 10 mulne0i ${⊢}2{A}2{A}\ne 0$
105 96 104 eqnetri ${⊢}{2{A}}^{2}\ne 0$
106 101 102 103 105 divdiri ${⊢}\frac{{{B}}^{2}+\left(-4{A}{C}\right)}{{2{A}}^{2}}=\left(\frac{{{B}}^{2}}{{2{A}}^{2}}\right)+\left(\frac{-4{A}{C}}{{2{A}}^{2}}\right)$
107 101 82 negsubi ${⊢}{{B}}^{2}+\left(-4{A}{C}\right)={{B}}^{2}-4{A}{C}$
108 107 oveq1i ${⊢}\frac{{{B}}^{2}+\left(-4{A}{C}\right)}{{2{A}}^{2}}=\frac{{{B}}^{2}-4{A}{C}}{{2{A}}^{2}}$
109 100 106 108 3eqtr2i ${⊢}{\left(\frac{{B}}{2{A}}\right)}^{2}+\left(\frac{-{C}}{{A}}\right)=\frac{{{B}}^{2}-4{A}{C}}{{2{A}}^{2}}$
110 53 57 109 3eqtri ${⊢}{\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}=\frac{{{B}}^{2}-4{A}{C}}{{2{A}}^{2}}$
111 110 oveq2i ${⊢}{2{A}}^{2}{\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={2{A}}^{2}\left(\frac{{{B}}^{2}-4{A}{C}}{{2{A}}^{2}}\right)$
112 101 82 subcli ${⊢}{{B}}^{2}-4{A}{C}\in ℂ$
113 112 103 105 divcan2i ${⊢}{2{A}}^{2}\left(\frac{{{B}}^{2}-4{A}{C}}{{2{A}}^{2}}\right)={{B}}^{2}-4{A}{C}$
114 13 111 113 3eqtri ${⊢}{2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={{B}}^{2}-4{A}{C}$
115 8 12 mulcli ${⊢}2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)\in ℂ$
116 115 112 pm3.2i ${⊢}\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)\in ℂ\wedge {{B}}^{2}-4{A}{C}\in ℂ\right)$
117 eqsqrtor ${⊢}\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)\in ℂ\wedge {{B}}^{2}-4{A}{C}\in ℂ\right)\to \left({2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={{B}}^{2}-4{A}{C}↔\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}\vee 2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}\right)\right)$
118 116 117 ax-mp ${⊢}{2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)}^{2}={{B}}^{2}-4{A}{C}↔\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}\vee 2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}\right)$
119 114 118 mpbi ${⊢}\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}\vee 2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}\right)$
120 sqrtcl ${⊢}{{B}}^{2}-4{A}{C}\in ℂ\to \sqrt{{{B}}^{2}-4{A}{C}}\in ℂ$
121 112 120 ax-mp ${⊢}\sqrt{{{B}}^{2}-4{A}{C}}\in ℂ$
122 121 8 12 10 divmuli ${⊢}\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}={X}+\left(\frac{{B}}{2{A}}\right)↔2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}$
123 eqcom ${⊢}\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}={X}+\left(\frac{{B}}{2{A}}\right)↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
124 122 123 bitr3i ${⊢}2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
125 121 8 10 divcli ${⊢}\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\in ℂ$
126 125 11 1 subadd2i ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)={X}↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
127 eqcom ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)={X}↔{X}=\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
128 126 127 bitr3i ${⊢}{X}+\left(\frac{{B}}{2{A}}\right)=\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}↔{X}=\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
129 divneg ${⊢}\left({B}\in ℂ\wedge 2{A}\in ℂ\wedge 2{A}\ne 0\right)\to -\frac{{B}}{2{A}}=\frac{-{B}}{2{A}}$
130 4 8 10 129 mp3an ${⊢}-\frac{{B}}{2{A}}=\frac{-{B}}{2{A}}$
131 130 oveq2i ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(-\frac{{B}}{2{A}}\right)=\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(\frac{-{B}}{2{A}}\right)$
132 125 11 negsubi ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(-\frac{{B}}{2{A}}\right)=\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
133 4 negcli ${⊢}-{B}\in ℂ$
134 133 8 10 divcli ${⊢}\frac{-{B}}{2{A}}\in ℂ$
135 125 134 addcomi ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(\frac{-{B}}{2{A}}\right)=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
136 131 132 135 3eqtr3i ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
137 133 121 8 10 divdiri ${⊢}\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
138 136 137 eqtr4i ${⊢}\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
139 138 eqeq2i ${⊢}{X}=\left(\frac{\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)↔{X}=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
140 124 128 139 3bitri ${⊢}2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}↔{X}=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
141 121 negcli ${⊢}-\sqrt{{{B}}^{2}-4{A}{C}}\in ℂ$
142 141 8 12 10 divmuli ${⊢}\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}={X}+\left(\frac{{B}}{2{A}}\right)↔2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}$
143 eqcom ${⊢}\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}={X}+\left(\frac{{B}}{2{A}}\right)↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
144 142 143 bitr3i ${⊢}2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
145 141 8 10 divcli ${⊢}\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\in ℂ$
146 145 11 1 subadd2i ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)={X}↔{X}+\left(\frac{{B}}{2{A}}\right)=\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
147 eqcom ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)={X}↔{X}=\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
148 146 147 bitr3i ${⊢}{X}+\left(\frac{{B}}{2{A}}\right)=\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}↔{X}=\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
149 130 oveq2i ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(-\frac{{B}}{2{A}}\right)=\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(\frac{-{B}}{2{A}}\right)$
150 145 11 negsubi ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(-\frac{{B}}{2{A}}\right)=\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)$
151 145 134 addcomi ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)+\left(\frac{-{B}}{2{A}}\right)=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
152 149 150 151 3eqtr3i ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
153 133 141 8 10 divdiri ${⊢}\frac{-{B}+\left(-\sqrt{{{B}}^{2}-4{A}{C}}\right)}{2{A}}=\left(\frac{-{B}}{2{A}}\right)+\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
154 133 121 negsubi ${⊢}-{B}+\left(-\sqrt{{{B}}^{2}-4{A}{C}}\right)=-{B}-\sqrt{{{B}}^{2}-4{A}{C}}$
155 154 oveq1i ${⊢}\frac{-{B}+\left(-\sqrt{{{B}}^{2}-4{A}{C}}\right)}{2{A}}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
156 152 153 155 3eqtr2i ${⊢}\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
157 156 eqeq2i ${⊢}{X}=\left(\frac{-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)-\left(\frac{{B}}{2{A}}\right)↔{X}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
158 144 148 157 3bitri ${⊢}2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}↔{X}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}$
159 140 158 orbi12i ${⊢}\left(2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=\sqrt{{{B}}^{2}-4{A}{C}}\vee 2{A}\left({X}+\left(\frac{{B}}{2{A}}\right)\right)=-\sqrt{{{B}}^{2}-4{A}{C}}\right)↔\left({X}=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\vee {X}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$
160 119 159 mpbi ${⊢}\left({X}=\frac{-{B}+\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\vee {X}=\frac{-{B}-\sqrt{{{B}}^{2}-4{A}{C}}}{2{A}}\right)$