This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem quad3d

Description: Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019) Deduction version. (Revised by Thierry Arnoux, 6-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 quad3d.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2 quad3d.2 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3 quad3d.3 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
4 quad3d.4 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
5 quad3d.5 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 quad3d.6 ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) = 0 )
7 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
8 7 2 mulcld ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℂ )
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
11 7 2 10 3 mulne0d ⊢ ( 𝜑 → ( 2 · 𝐴 ) ≠ 0 )
12 4 8 11 divcld ⊢ ( 𝜑 → ( 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
13 1 12 addcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ∈ ℂ )
14 8 13 sqmuld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ↑ 2 ) = ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ↑ 2 ) ) )
15 1 12 binom2d ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ) + ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ) )
16 1 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
17 2 16 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
18 4 1 mulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ ℂ )
19 17 18 2 3 divdird ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) / 𝐴 ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) + ( ( 𝐵 · 𝑋 ) / 𝐴 ) ) )
20 16 2 3 divcan3d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) = ( 𝑋 ↑ 2 ) )
21 4 1 2 3 div23d ⊢ ( 𝜑 → ( ( 𝐵 · 𝑋 ) / 𝐴 ) = ( ( 𝐵 / 𝐴 ) · 𝑋 ) )
22 20 21 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) / 𝐴 ) + ( ( 𝐵 · 𝑋 ) / 𝐴 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) )
23 19 22 eqtr2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) / 𝐴 ) )
24 4 2 3 divcld ⊢ ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℂ )
25 24 1 mulcomd ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = ( 𝑋 · ( 𝐵 / 𝐴 ) ) )
26 1 24 mulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝐵 / 𝐴 ) ) ∈ ℂ )
27 26 7 10 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( 𝑋 · ( 𝐵 / 𝐴 ) ) / 2 ) ) = ( 𝑋 · ( 𝐵 / 𝐴 ) ) )
28 1 24 7 10 divassd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐵 / 𝐴 ) ) / 2 ) = ( 𝑋 · ( ( 𝐵 / 𝐴 ) / 2 ) ) )
29 4 2 7 3 10 divdiv1d ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) / 2 ) = ( 𝐵 / ( 𝐴 · 2 ) ) )
30 2 7 mulcomd ⊢ ( 𝜑 → ( 𝐴 · 2 ) = ( 2 · 𝐴 ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝐵 / ( 𝐴 · 2 ) ) = ( 𝐵 / ( 2 · 𝐴 ) ) )
32 29 31 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) / 2 ) = ( 𝐵 / ( 2 · 𝐴 ) ) )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝐵 / 𝐴 ) / 2 ) ) = ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) )
34 28 33 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐵 / 𝐴 ) ) / 2 ) = ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) )
35 34 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 𝑋 · ( 𝐵 / 𝐴 ) ) / 2 ) ) = ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) )
36 25 27 35 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐵 / 𝐴 ) · 𝑋 ) = ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) )
37 36 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( ( 𝐵 / 𝐴 ) · 𝑋 ) ) = ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ) )
38 17 18 addcld ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) ∈ ℂ )
39 17 18 5 addassd ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) + 𝐶 ) = ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) )
40 38 5 39 mvlraddd ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) = ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) − 𝐶 ) )
41 6 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) − 𝐶 ) = ( 0 − 𝐶 ) )
42 df-neg ⊢ - 𝐶 = ( 0 − 𝐶 )
43 41 42 eqtr4di ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐵 · 𝑋 ) + 𝐶 ) ) − 𝐶 ) = - 𝐶 )
44 40 43 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) = - 𝐶 )
45 44 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 𝑋 ↑ 2 ) ) + ( 𝐵 · 𝑋 ) ) / 𝐴 ) = ( - 𝐶 / 𝐴 ) )
46 23 37 45 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ) = ( - 𝐶 / 𝐴 ) )
47 46 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 2 · ( 𝑋 · ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ) + ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ) = ( ( - 𝐶 / 𝐴 ) + ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ) )
48 15 47 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ↑ 2 ) = ( ( - 𝐶 / 𝐴 ) + ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ) )
49 5 negcld ⊢ ( 𝜑 → - 𝐶 ∈ ℂ )
50 49 2 3 divcld ⊢ ( 𝜑 → ( - 𝐶 / 𝐴 ) ∈ ℂ )
51 12 sqcld ⊢ ( 𝜑 → ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ∈ ℂ )
52 50 51 addcomd ⊢ ( 𝜑 → ( ( - 𝐶 / 𝐴 ) + ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) ) = ( ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) + ( - 𝐶 / 𝐴 ) ) )
53 4 8 11 sqdivd ⊢ ( 𝜑 → ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
54 4cn ⊢ 4 ∈ ℂ
55 54 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
56 55 2 mulcld ⊢ ( 𝜑 → ( 4 · 𝐴 ) ∈ ℂ )
57 4ne0 ⊢ 4 ≠ 0
58 57 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
59 55 2 58 3 mulne0d ⊢ ( 𝜑 → ( 4 · 𝐴 ) ≠ 0 )
60 56 56 49 2 59 3 divmuldivd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) / ( 4 · 𝐴 ) ) · ( - 𝐶 / 𝐴 ) ) = ( ( ( 4 · 𝐴 ) · - 𝐶 ) / ( ( 4 · 𝐴 ) · 𝐴 ) ) )
61 56 59 dividd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) / ( 4 · 𝐴 ) ) = 1 )
62 61 eqcomd ⊢ ( 𝜑 → 1 = ( ( 4 · 𝐴 ) / ( 4 · 𝐴 ) ) )
63 62 oveq1d ⊢ ( 𝜑 → ( 1 · ( - 𝐶 / 𝐴 ) ) = ( ( ( 4 · 𝐴 ) / ( 4 · 𝐴 ) ) · ( - 𝐶 / 𝐴 ) ) )
64 50 mullidd ⊢ ( 𝜑 → ( 1 · ( - 𝐶 / 𝐴 ) ) = ( - 𝐶 / 𝐴 ) )
65 63 64 eqtr3d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) / ( 4 · 𝐴 ) ) · ( - 𝐶 / 𝐴 ) ) = ( - 𝐶 / 𝐴 ) )
66 5 mulm1d ⊢ ( 𝜑 → ( - 1 · 𝐶 ) = - 𝐶 )
67 66 eqcomd ⊢ ( 𝜑 → - 𝐶 = ( - 1 · 𝐶 ) )
68 67 oveq2d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · - 𝐶 ) = ( ( 4 · 𝐴 ) · ( - 1 · 𝐶 ) ) )
69 neg1cn ⊢ - 1 ∈ ℂ
70 69 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
71 56 70 5 mulassd ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · - 1 ) · 𝐶 ) = ( ( 4 · 𝐴 ) · ( - 1 · 𝐶 ) ) )
72 68 71 eqtr4d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · - 𝐶 ) = ( ( ( 4 · 𝐴 ) · - 1 ) · 𝐶 ) )
73 56 70 mulcomd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · - 1 ) = ( - 1 · ( 4 · 𝐴 ) ) )
74 73 oveq1d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · - 1 ) · 𝐶 ) = ( ( - 1 · ( 4 · 𝐴 ) ) · 𝐶 ) )
75 70 56 5 mulassd ⊢ ( 𝜑 → ( ( - 1 · ( 4 · 𝐴 ) ) · 𝐶 ) = ( - 1 · ( ( 4 · 𝐴 ) · 𝐶 ) ) )
76 72 74 75 3eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · - 𝐶 ) = ( - 1 · ( ( 4 · 𝐴 ) · 𝐶 ) ) )
77 55 2 5 mulassd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐶 ) = ( 4 · ( 𝐴 · 𝐶 ) ) )
78 77 oveq2d ⊢ ( 𝜑 → ( - 1 · ( ( 4 · 𝐴 ) · 𝐶 ) ) = ( - 1 · ( 4 · ( 𝐴 · 𝐶 ) ) ) )
79 2 5 mulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
80 55 79 mulcld ⊢ ( 𝜑 → ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
81 80 mulm1d ⊢ ( 𝜑 → ( - 1 · ( 4 · ( 𝐴 · 𝐶 ) ) ) = - ( 4 · ( 𝐴 · 𝐶 ) ) )
82 76 78 81 3eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · - 𝐶 ) = - ( 4 · ( 𝐴 · 𝐶 ) ) )
83 2t2e4 ⊢ ( 2 · 2 ) = 4
84 83 a1i ⊢ ( 𝜑 → ( 2 · 2 ) = 4 )
85 84 eqcomd ⊢ ( 𝜑 → 4 = ( 2 · 2 ) )
86 85 oveq1d ⊢ ( 𝜑 → ( 4 · 𝐴 ) = ( ( 2 · 2 ) · 𝐴 ) )
87 86 oveq1d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐴 ) = ( ( ( 2 · 2 ) · 𝐴 ) · 𝐴 ) )
88 7 7 2 mulassd ⊢ ( 𝜑 → ( ( 2 · 2 ) · 𝐴 ) = ( 2 · ( 2 · 𝐴 ) ) )
89 88 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · 𝐴 ) · 𝐴 ) = ( ( 2 · ( 2 · 𝐴 ) ) · 𝐴 ) )
90 87 89 eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐴 ) = ( ( 2 · ( 2 · 𝐴 ) ) · 𝐴 ) )
91 7 8 mulcomd ⊢ ( 𝜑 → ( 2 · ( 2 · 𝐴 ) ) = ( ( 2 · 𝐴 ) · 2 ) )
92 91 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( 2 · 𝐴 ) ) · 𝐴 ) = ( ( ( 2 · 𝐴 ) · 2 ) · 𝐴 ) )
93 8 7 2 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 2 ) · 𝐴 ) = ( ( 2 · 𝐴 ) · ( 2 · 𝐴 ) ) )
94 90 92 93 3eqtrd ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐴 ) = ( ( 2 · 𝐴 ) · ( 2 · 𝐴 ) ) )
95 8 sqvald ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ↑ 2 ) = ( ( 2 · 𝐴 ) · ( 2 · 𝐴 ) ) )
96 94 95 eqtr4d ⊢ ( 𝜑 → ( ( 4 · 𝐴 ) · 𝐴 ) = ( ( 2 · 𝐴 ) ↑ 2 ) )
97 82 96 oveq12d ⊢ ( 𝜑 → ( ( ( 4 · 𝐴 ) · - 𝐶 ) / ( ( 4 · 𝐴 ) · 𝐴 ) ) = ( - ( 4 · ( 𝐴 · 𝐶 ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
98 60 65 97 3eqtr3d ⊢ ( 𝜑 → ( - 𝐶 / 𝐴 ) = ( - ( 4 · ( 𝐴 · 𝐶 ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
99 53 98 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) + ( - 𝐶 / 𝐴 ) ) = ( ( ( 𝐵 ↑ 2 ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) + ( - ( 4 · ( 𝐴 · 𝐶 ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) ) )
100 4 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
101 80 negcld ⊢ ( 𝜑 → - ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ )
102 8 sqcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ↑ 2 ) ∈ ℂ )
103 8 8 11 11 mulne0d ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( 2 · 𝐴 ) ) ≠ 0 )
104 95 103 eqnetrd ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) ↑ 2 ) ≠ 0 )
105 100 101 102 104 divdird ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) + - ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) + ( - ( 4 · ( 𝐴 · 𝐶 ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) ) )
106 100 80 negsubd ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + - ( 4 · ( 𝐴 · 𝐶 ) ) ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
107 106 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 ↑ 2 ) + - ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
108 99 105 107 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝐵 / ( 2 · 𝐴 ) ) ↑ 2 ) + ( - 𝐶 / 𝐴 ) ) = ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
109 48 52 108 3eqtrd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ↑ 2 ) = ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) )
110 109 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ↑ 2 ) ) = ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) ) )
111 100 80 subcld ⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ )
112 111 102 104 divcan2d ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) ↑ 2 ) · ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) / ( ( 2 · 𝐴 ) ↑ 2 ) ) ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
113 14 110 112 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) )
114 8 13 mulcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ∈ ℂ )
115 eqsqrtor ⊢ ( ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ∈ ℂ ∧ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ∈ ℂ ) → ( ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ↔ ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∨ ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) ) )
116 114 111 115 syl2anc ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ↔ ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∨ ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) ) )
117 113 116 mpbid ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∨ ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) )
118 111 sqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∈ ℂ )
119 8 13 118 11 rdiv ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ↔ ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
120 118 8 11 divcld ⊢ ( 𝜑 → ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
121 1 12 120 addlsub ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ↔ 𝑋 = ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) ) )
122 4 8 11 divnegd ⊢ ( 𝜑 → - ( 𝐵 / ( 2 · 𝐴 ) ) = ( - 𝐵 / ( 2 · 𝐴 ) ) )
123 122 oveq2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + - ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + ( - 𝐵 / ( 2 · 𝐴 ) ) ) )
124 120 12 negsubd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + - ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) )
125 4 negcld ⊢ ( 𝜑 → - 𝐵 ∈ ℂ )
126 125 8 11 divcld ⊢ ( 𝜑 → ( - 𝐵 / ( 2 · 𝐴 ) ) ∈ ℂ )
127 120 126 addcomd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + ( - 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
128 123 124 127 3eqtr3d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
129 125 118 8 11 divdird ⊢ ( 𝜑 → ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
130 128 129 eqtr4d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) )
131 130 eqeq2d ⊢ ( 𝜑 → ( 𝑋 = ( ( ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) ↔ 𝑋 = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) )
132 119 121 131 3bitrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ↔ 𝑋 = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) )
133 118 negcld ⊢ ( 𝜑 → - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∈ ℂ )
134 8 13 133 11 rdiv ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ↔ ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
135 133 8 11 divcld ⊢ ( 𝜑 → ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ∈ ℂ )
136 1 12 135 addlsub ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ↔ 𝑋 = ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) ) )
137 122 oveq2d ⊢ ( 𝜑 → ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + - ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + ( - 𝐵 / ( 2 · 𝐴 ) ) ) )
138 135 12 negsubd ⊢ ( 𝜑 → ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + - ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) )
139 135 126 addcomd ⊢ ( 𝜑 → ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) + ( - 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
140 137 138 139 3eqtr3d ⊢ ( 𝜑 → ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
141 125 133 8 11 divdird ⊢ ( 𝜑 → ( ( - 𝐵 + - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 / ( 2 · 𝐴 ) ) + ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) ) )
142 125 118 negsubd ⊢ ( 𝜑 → ( - 𝐵 + - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) = ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) )
143 142 oveq1d ⊢ ( 𝜑 → ( ( - 𝐵 + - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) )
144 140 141 143 3eqtr2d ⊢ ( 𝜑 → ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) )
145 144 eqeq2d ⊢ ( 𝜑 → ( 𝑋 = ( ( - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) / ( 2 · 𝐴 ) ) − ( 𝐵 / ( 2 · 𝐴 ) ) ) ↔ 𝑋 = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) )
146 134 136 145 3bitrd ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ↔ 𝑋 = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) )
147 132 146 orbi12d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ∨ ( ( 2 · 𝐴 ) · ( 𝑋 + ( 𝐵 / ( 2 · 𝐴 ) ) ) ) = - ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) ↔ ( 𝑋 = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) ) )
148 117 147 mpbid ⊢ ( 𝜑 → ( 𝑋 = ( ( - 𝐵 + ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ∨ 𝑋 = ( ( - 𝐵 − ( √ ‘ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ) ) / ( 2 · 𝐴 ) ) ) )