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 ) ) ) )

Metamath Proof Explorer

Theorem quad3d

Proof