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	mullidi	⊢ ( 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 · 𝐴 ) ) )