Metamath Proof Explorer

Theorem quad3

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

Ref Expression
Hypotheses quad3.1 ⊢ 𝑋 ∈ ℂ
quad3.2 ⊢ 𝐴 ∈ ℂ
quad3.3 ⊢ 𝐴 ≠ 0
quad3.4 ⊢ 𝐵 ∈ ℂ
quad3.5 ⊢ 𝐶 ∈ ℂ
quad3.6 ⊢ ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0
Assertion quad3 ( 𝑋 = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) )

Proof

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