quad3d - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > quad3d		Structured version Visualization version GIF version

Theorem quad3d 33275

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

**Hypotheses**
Ref	Expression
quad3d.1	⊢ (𝜑 → 𝑋 ∈ ℂ)
quad3d.2	⊢ (𝜑 → 𝐴 ∈ ℂ)
quad3d.3	⊢ (𝜑 → 𝐴 ≠ 0)
quad3d.4	⊢ (𝜑 → 𝐵 ∈ ℂ)
quad3d.5	⊢ (𝜑 → 𝐶 ∈ ℂ)
quad3d.6	⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)

**Assertion**
Ref	Expression
quad3d	⊢ (𝜑 → (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))

**Proof of Theorem quad3d**
Step	Hyp	Ref	Expression
1		2cnd 12391	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
2		quad3d.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1, 2	mulcld 11301	. . . . 5 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
4		quad3d.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
5		quad3d.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
6		2ne0 12419	. . . . . . . . 9 ⊢ 2 ≠ 0
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
8		quad3d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ 0)
9	1, 2, 7, 8	mulne0d 11938	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
10	5, 3, 9	divcld 12063	. . . . . 6 ⊢ (𝜑 → (𝐵 / (2 · 𝐴)) ∈ ℂ)
11	4, 10	addcld 11300	. . . . 5 ⊢ (𝜑 → (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ)
12	3, 11	sqmuld 14270	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)))
13	4, 10	binom2d 14330	. . . . . . 7 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)))
14	4	sqcld 14256	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
15	2, 14	mulcld 11301	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
16	5, 4	mulcld 11301	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
17	15, 16, 2, 8	divdird 12101	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)))
18	14, 2, 8	divcan3d 12068	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2))
19	5, 4, 2, 8	div23d 12100	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋))
20	18, 19	oveq12d 7426	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)))
21	17, 20	eqtr2d 2796	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴))
22	5, 2, 8	divcld 12063	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ)
23	22, 4	mulcomd 11302	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)))
24	4, 22	mulcld 11301	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐵 / 𝐴)) ∈ ℂ)
25	24, 1, 7	divcan2d 12065	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)))
26	4, 22, 1, 7	divassd 12098	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)))
27	5, 2, 1, 8, 7	divdiv1d 12094	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)))
28	2, 1	mulcomd 11302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 2) = (2 · 𝐴))
29	28	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)))
30	27, 29	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)))
31	30	oveq2d 7424	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))))
32	26, 31	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))))
33	32	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
34	23, 25, 33	3eqtr2d 2801	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
35	34	oveq2d 7424	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))))
36	15, 16	addcld 11300	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ)
37		quad3d.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
38	15, 16, 37	addassd 11303	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)))
39	36, 37, 38	mvlraddd 11696	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶))
40		quad3d.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)
41	40	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶))
42		df-neg 11516	. . . . . . . . . . . 12 ⊢ -𝐶 = (0 − 𝐶)
43	41, 42	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶)
44	39, 43	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶)
45	44	oveq1d 7423	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴))
46	21, 35, 45	3eqtr3d 2803	. . . . . . . 8 ⊢ (𝜑 → ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴))
47	46	oveq1d 7423	. . . . . . 7 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
48	13, 47	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
49	37	negcld 11628	. . . . . . . 8 ⊢ (𝜑 → -𝐶 ∈ ℂ)
50	49, 2, 8	divcld 12063	. . . . . . 7 ⊢ (𝜑 → (-𝐶 / 𝐴) ∈ ℂ)
51	10	sqcld 14256	. . . . . . 7 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ)
52	50, 51	addcomd 11484	. . . . . 6 ⊢ (𝜑 → ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)))
53	5, 3, 9	sqdivd 14271	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)))
54		4cn 12398	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
56	55, 2	mulcld 11301	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
57		4ne0 12424	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ≠ 0)
59	55, 2, 58, 8	mulne0d 11938	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
60	56, 56, 49, 2, 59, 8	divmuldivd 12104	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)))
61	56, 59	dividd 12061	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) / (4 · 𝐴)) = 1)
62	61	eqcomd 2766	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = ((4 · 𝐴) / (4 · 𝐴)))
63	62	oveq1d 7423	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)))
64	50	mullidd 11299	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
65	63, 64	eqtr3d 2797	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
66	37	mulm1d 11738	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 · 𝐶) = -𝐶)
67	66	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝐶 = (-1 · 𝐶))
68	67	oveq2d 7424	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
69		neg1cn 12275	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -1 ∈ ℂ)
71	56, 70, 37	mulassd 11304	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
72	68, 71	eqtr4d 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶))
73	56, 70	mulcomd 11302	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -1) = (-1 · (4 · 𝐴)))
74	73	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((-1 · (4 · 𝐴)) · 𝐶))
75	70, 56, 37	mulassd 11304	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-1 · (4 · 𝐴)) · 𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
76	72, 74, 75	3eqtrd 2799	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
77	55, 2, 37	mulassd 11304	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
78	77	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · ((4 · 𝐴) · 𝐶)) = (-1 · (4 · (𝐴 · 𝐶))))
79	2, 37	mulcld 11301	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
80	55, 79	mulcld 11301	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
81	80	mulm1d 11738	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · (4 · (𝐴 · 𝐶))) = -(4 · (𝐴 · 𝐶)))
82	76, 78, 81	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)))
83		2t2e4 12476	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 2) = 4)
85	84	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 4 = (2 · 2))
86	85	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (4 · 𝐴) = ((2 · 2) · 𝐴))
87	86	oveq1d 7423	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (((2 · 2) · 𝐴) · 𝐴))
88	1, 1, 2	mulassd 11304	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
89	88	oveq1d 7423	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 2) · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
90	87, 89	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
91	1, 3	mulcomd 11302	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (2 · 𝐴)) = ((2 · 𝐴) · 2))
92	91	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐴) = (((2 · 𝐴) · 2) · 𝐴))
93	3, 1, 2	mulassd 11304	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
94	90, 92, 93	3eqtrd 2799	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
95	3	sqvald 14255	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴)))
96	94, 95	eqtr4d 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴)↑2))
97	82, 96	oveq12d 7426	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
98	60, 65, 97	3eqtr3d 2803	. . . . . . . 8 ⊢ (𝜑 → (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
99	53, 98	oveq12d 7426	. . . . . . 7 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
100	5	sqcld 14256	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
101	80	negcld 11628	. . . . . . . 8 ⊢ (𝜑 → -(4 · (𝐴 · 𝐶)) ∈ ℂ)
102	3	sqcld 14256	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ∈ ℂ)
103	3, 3, 9, 9	mulne0d 11938	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝐴) · (2 · 𝐴)) ≠ 0)
104	95, 103	eqnetrd 3022	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ≠ 0)
105	100, 101, 102, 104	divdird 12101	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
106	100, 80	negsubd 11647	. . . . . . . 8 ⊢ (𝜑 → ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
107	106	oveq1d 7423	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
108	99, 105, 107	3eqtr2d 2801	. . . . . 6 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
109	48, 52, 108	3eqtrd 2799	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
110	109	oveq2d 7424	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))))
111	100, 80	subcld 11641	. . . . 5 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ)
112	111, 102, 104	divcan2d 12065	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
113	12, 110, 112	3eqtrd 2799	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
114	3, 11	mulcld 11301	. . . 4 ⊢ (𝜑 → ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ)
115		eqsqrtor 15502	. . . 4 ⊢ ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ) → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
116	114, 111, 115	syl2anc 596	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
117	113, 116	mpbid 235	. 2 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
118	111	sqrtcld 15575	. . . . 5 ⊢ (𝜑 → (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
119	3, 11, 118, 9	rdiv 12122	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
120	118, 3, 9	divcld 12063	. . . . 5 ⊢ (𝜑 → ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
121	4, 10, 120	addlsub 11702	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
122	5, 3, 9	divnegd 12076	. . . . . . . 8 ⊢ (𝜑 → -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)))
123	122	oveq2d 7424	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
124	120, 10	negsubd 11647	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
125	5	negcld 11628	. . . . . . . . 9 ⊢ (𝜑 → -𝐵 ∈ ℂ)
126	125, 3, 9	divcld 12063	. . . . . . . 8 ⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ)
127	120, 126	addcomd 11484	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
128	123, 124, 127	3eqtr3d 2803	. . . . . 6 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
129	125, 118, 3, 9	divdird 12101	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
130	128, 129	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
131	130	eqeq2d 2771	. . . 4 ⊢ (𝜑 → (𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
132	119, 121, 131	3bitrd 308	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
133	118	negcld 11628	. . . . 5 ⊢ (𝜑 → -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
134	3, 11, 133, 9	rdiv 12122	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
135	133, 3, 9	divcld 12063	. . . . 5 ⊢ (𝜑 → (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
136	4, 10, 135	addlsub 11702	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
137	122	oveq2d 7424	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
138	135, 10	negsubd 11647	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
139	135, 126	addcomd 11484	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
140	137, 138, 139	3eqtr3d 2803	. . . . . 6 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
141	125, 133, 3, 9	divdird 12101	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
142	125, 118	negsubd 11647	. . . . . . 7 ⊢ (𝜑 → (-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
143	142	oveq1d 7423	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
144	140, 141, 143	3eqtr2d 2801	. . . . 5 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
145	144	eqeq2d 2771	. . . 4 ⊢ (𝜑 → (𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
146	134, 136, 145	3bitrd 308	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
147	132, 146	orbi12d 932	. 2 ⊢ (𝜑 → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) ↔ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))))
148	117, 147	mpbid 235	1 ⊢ (𝜑 → (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ‘cfv 6527 (class class class)co 7408 ℂcc 11170 0cc0 11172 1c1 11173 + caddc 11175 · cmul 11177 − cmin 11513 -cneg 11514 / cdiv 11943 2c2 12367 4c4 12369 ↑cexp 14173 √csqrt 15368

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248 ax-pre-mulgt0 11249 ax-pre-sup 11250

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-2nd 7985 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-er 8695 df-en 8952 df-dom 8953 df-sdom 8954 df-sup 9412 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516 df-div 11944 df-nn 12306 df-2 12375 df-3 12376 df-4 12377 df-n0 12577 df-z 12664 df-uz 12936 df-rp 13091 df-seq 14114 df-exp 14174 df-cj 15234 df-re 15235 df-im 15236 df-sqrt 15370 df-abs 15371

This theorem is used by: constrfin 34312

W3C validator