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 
|- ( ph -> X e. CC )
quad3d.2 
|- ( ph -> A e. CC )
quad3d.3 
|- ( ph -> A =/= 0 )
quad3d.4 
|- ( ph -> B e. CC )
quad3d.5 
|- ( ph -> C e. CC )
quad3d.6 
|- ( ph -> ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 )
Assertion quad3d 
|- ( ph -> ( X = ( ( -u B + ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqrt ` ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) ) ) / ( 2 x. A ) ) ) )

Proof

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