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 32822

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 12259	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
2		quad3d.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1, 2	mulcld 11165	. . . . 5 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
4		quad3d.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
5		quad3d.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
6		2ne0 12285	. . . . . . . . 9 ⊢ 2 ≠ 0
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
8		quad3d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ 0)
9	1, 2, 7, 8	mulne0d 11802	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
10	5, 3, 9	divcld 11931	. . . . . 6 ⊢ (𝜑 → (𝐵 / (2 · 𝐴)) ∈ ℂ)
11	4, 10	addcld 11164	. . . . 5 ⊢ (𝜑 → (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ)
12	3, 11	sqmuld 14120	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)))
13	4, 10	binom2d 14180	. . . . . . 7 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)))
14	4	sqcld 14106	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
15	2, 14	mulcld 11165	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
16	5, 4	mulcld 11165	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
17	15, 16, 2, 8	divdird 11969	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)))
18	14, 2, 8	divcan3d 11936	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2))
19	5, 4, 2, 8	div23d 11968	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋))
20	18, 19	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)))
21	17, 20	eqtr2d 2773	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴))
22	5, 2, 8	divcld 11931	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ)
23	22, 4	mulcomd 11166	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)))
24	4, 22	mulcld 11165	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐵 / 𝐴)) ∈ ℂ)
25	24, 1, 7	divcan2d 11933	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)))
26	4, 22, 1, 7	divassd 11966	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)))
27	5, 2, 1, 8, 7	divdiv1d 11962	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)))
28	2, 1	mulcomd 11166	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 2) = (2 · 𝐴))
29	28	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)))
30	27, 29	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)))
31	30	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))))
32	26, 31	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))))
33	32	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
34	23, 25, 33	3eqtr2d 2778	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
35	34	oveq2d 7383	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))))
36	15, 16	addcld 11164	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ)
37		quad3d.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
38	15, 16, 37	addassd 11167	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)))
39	36, 37, 38	mvlraddd 11560	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶))
40		quad3d.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)
41	40	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶))
42		df-neg 11380	. . . . . . . . . . . 12 ⊢ -𝐶 = (0 − 𝐶)
43	41, 42	eqtr4di 2790	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶)
44	39, 43	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶)
45	44	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴))
46	21, 35, 45	3eqtr3d 2780	. . . . . . . 8 ⊢ (𝜑 → ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴))
47	46	oveq1d 7382	. . . . . . 7 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
48	13, 47	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
49	37	negcld 11492	. . . . . . . 8 ⊢ (𝜑 → -𝐶 ∈ ℂ)
50	49, 2, 8	divcld 11931	. . . . . . 7 ⊢ (𝜑 → (-𝐶 / 𝐴) ∈ ℂ)
51	10	sqcld 14106	. . . . . . 7 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ)
52	50, 51	addcomd 11348	. . . . . 6 ⊢ (𝜑 → ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)))
53	5, 3, 9	sqdivd 14121	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)))
54		4cn 12266	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
56	55, 2	mulcld 11165	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
57		4ne0 12289	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ≠ 0)
59	55, 2, 58, 8	mulne0d 11802	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
60	56, 56, 49, 2, 59, 8	divmuldivd 11972	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)))
61	56, 59	dividd 11929	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) / (4 · 𝐴)) = 1)
62	61	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = ((4 · 𝐴) / (4 · 𝐴)))
63	62	oveq1d 7382	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)))
64	50	mullidd 11163	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
65	63, 64	eqtr3d 2774	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
66	37	mulm1d 11602	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 · 𝐶) = -𝐶)
67	66	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝐶 = (-1 · 𝐶))
68	67	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
69		neg1cn 12144	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -1 ∈ ℂ)
71	56, 70, 37	mulassd 11168	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
72	68, 71	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶))
73	56, 70	mulcomd 11166	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -1) = (-1 · (4 · 𝐴)))
74	73	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((-1 · (4 · 𝐴)) · 𝐶))
75	70, 56, 37	mulassd 11168	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-1 · (4 · 𝐴)) · 𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
76	72, 74, 75	3eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
77	55, 2, 37	mulassd 11168	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
78	77	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · ((4 · 𝐴) · 𝐶)) = (-1 · (4 · (𝐴 · 𝐶))))
79	2, 37	mulcld 11165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
80	55, 79	mulcld 11165	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
81	80	mulm1d 11602	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · (4 · (𝐴 · 𝐶))) = -(4 · (𝐴 · 𝐶)))
82	76, 78, 81	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)))
83		2t2e4 12340	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 2) = 4)
85	84	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 4 = (2 · 2))
86	85	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (4 · 𝐴) = ((2 · 2) · 𝐴))
87	86	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (((2 · 2) · 𝐴) · 𝐴))
88	1, 1, 2	mulassd 11168	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
89	88	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 2) · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
90	87, 89	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
91	1, 3	mulcomd 11166	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (2 · 𝐴)) = ((2 · 𝐴) · 2))
92	91	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐴) = (((2 · 𝐴) · 2) · 𝐴))
93	3, 1, 2	mulassd 11168	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
94	90, 92, 93	3eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
95	3	sqvald 14105	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴)))
96	94, 95	eqtr4d 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴)↑2))
97	82, 96	oveq12d 7385	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
98	60, 65, 97	3eqtr3d 2780	. . . . . . . 8 ⊢ (𝜑 → (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
99	53, 98	oveq12d 7385	. . . . . . 7 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
100	5	sqcld 14106	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
101	80	negcld 11492	. . . . . . . 8 ⊢ (𝜑 → -(4 · (𝐴 · 𝐶)) ∈ ℂ)
102	3	sqcld 14106	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ∈ ℂ)
103	3, 3, 9, 9	mulne0d 11802	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝐴) · (2 · 𝐴)) ≠ 0)
104	95, 103	eqnetrd 3000	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ≠ 0)
105	100, 101, 102, 104	divdird 11969	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
106	100, 80	negsubd 11511	. . . . . . . 8 ⊢ (𝜑 → ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
107	106	oveq1d 7382	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
108	99, 105, 107	3eqtr2d 2778	. . . . . 6 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
109	48, 52, 108	3eqtrd 2776	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
110	109	oveq2d 7383	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))))
111	100, 80	subcld 11505	. . . . 5 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ)
112	111, 102, 104	divcan2d 11933	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
113	12, 110, 112	3eqtrd 2776	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
114	3, 11	mulcld 11165	. . . 4 ⊢ (𝜑 → ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ)
115		eqsqrtor 15329	. . . 4 ⊢ ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ) → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
116	114, 111, 115	syl2anc 585	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
117	113, 116	mpbid 232	. 2 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
118	111	sqrtcld 15402	. . . . 5 ⊢ (𝜑 → (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
119	3, 11, 118, 9	rdiv 11990	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
120	118, 3, 9	divcld 11931	. . . . 5 ⊢ (𝜑 → ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
121	4, 10, 120	addlsub 11566	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
122	5, 3, 9	divnegd 11944	. . . . . . . 8 ⊢ (𝜑 → -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)))
123	122	oveq2d 7383	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
124	120, 10	negsubd 11511	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
125	5	negcld 11492	. . . . . . . . 9 ⊢ (𝜑 → -𝐵 ∈ ℂ)
126	125, 3, 9	divcld 11931	. . . . . . . 8 ⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ)
127	120, 126	addcomd 11348	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
128	123, 124, 127	3eqtr3d 2780	. . . . . 6 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
129	125, 118, 3, 9	divdird 11969	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
130	128, 129	eqtr4d 2775	. . . . 5 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
131	130	eqeq2d 2748	. . . 4 ⊢ (𝜑 → (𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
132	119, 121, 131	3bitrd 305	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
133	118	negcld 11492	. . . . 5 ⊢ (𝜑 → -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
134	3, 11, 133, 9	rdiv 11990	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
135	133, 3, 9	divcld 11931	. . . . 5 ⊢ (𝜑 → (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
136	4, 10, 135	addlsub 11566	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
137	122	oveq2d 7383	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
138	135, 10	negsubd 11511	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
139	135, 126	addcomd 11348	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
140	137, 138, 139	3eqtr3d 2780	. . . . . 6 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
141	125, 133, 3, 9	divdird 11969	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
142	125, 118	negsubd 11511	. . . . . . 7 ⊢ (𝜑 → (-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
143	142	oveq1d 7382	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
144	140, 141, 143	3eqtr2d 2778	. . . . 5 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
145	144	eqeq2d 2748	. . . 4 ⊢ (𝜑 → (𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
146	134, 136, 145	3bitrd 305	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
147	132, 146	orbi12d 919	. 2 ⊢ (𝜑 → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) ↔ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))))
148	117, 147	mpbid 232	1 ⊢ (𝜑 → (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ‘cfv 6499 (class class class)co 7367 ℂcc 11036 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 − cmin 11377 -cneg 11378 / cdiv 11807 2c2 12236 4c4 12238 ↑cexp 14023 √csqrt 15195

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-sup 9355 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-n0 12438 df-z 12525 df-uz 12789 df-rp 12943 df-seq 13964 df-exp 14024 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198

This theorem is referenced by: constrfin 33890

W3C validator