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 33222

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 12346	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
2		quad3d.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1, 2	mulcld 11256	. . . . 5 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
4		quad3d.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
5		quad3d.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
6		2ne0 12374	. . . . . . . . 9 ⊢ 2 ≠ 0
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
8		quad3d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ 0)
9	1, 2, 7, 8	mulne0d 11893	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
10	5, 3, 9	divcld 12018	. . . . . 6 ⊢ (𝜑 → (𝐵 / (2 · 𝐴)) ∈ ℂ)
11	4, 10	addcld 11255	. . . . 5 ⊢ (𝜑 → (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ)
12	3, 11	sqmuld 14224	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)))
13	4, 10	binom2d 14284	. . . . . . 7 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)))
14	4	sqcld 14210	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
15	2, 14	mulcld 11256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
16	5, 4	mulcld 11256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
17	15, 16, 2, 8	divdird 12056	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)))
18	14, 2, 8	divcan3d 12023	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2))
19	5, 4, 2, 8	div23d 12055	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋))
20	18, 19	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)))
21	17, 20	eqtr2d 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴))
22	5, 2, 8	divcld 12018	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ)
23	22, 4	mulcomd 11257	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)))
24	4, 22	mulcld 11256	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐵 / 𝐴)) ∈ ℂ)
25	24, 1, 7	divcan2d 12020	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)))
26	4, 22, 1, 7	divassd 12053	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)))
27	5, 2, 1, 8, 7	divdiv1d 12049	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)))
28	2, 1	mulcomd 11257	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 2) = (2 · 𝐴))
29	28	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)))
30	27, 29	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)))
31	30	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))))
32	26, 31	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))))
33	32	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
34	23, 25, 33	3eqtr2d 2803	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
35	34	oveq2d 7432	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))))
36	15, 16	addcld 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ)
37		quad3d.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
38	15, 16, 37	addassd 11258	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)))
39	36, 37, 38	mvlraddd 11651	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶))
40		quad3d.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)
41	40	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶))
42		df-neg 11471	. . . . . . . . . . . 12 ⊢ -𝐶 = (0 − 𝐶)
43	41, 42	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶)
44	39, 43	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶)
45	44	oveq1d 7431	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴))
46	21, 35, 45	3eqtr3d 2805	. . . . . . . 8 ⊢ (𝜑 → ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴))
47	46	oveq1d 7431	. . . . . . 7 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
48	13, 47	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
49	37	negcld 11583	. . . . . . . 8 ⊢ (𝜑 → -𝐶 ∈ ℂ)
50	49, 2, 8	divcld 12018	. . . . . . 7 ⊢ (𝜑 → (-𝐶 / 𝐴) ∈ ℂ)
51	10	sqcld 14210	. . . . . . 7 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ)
52	50, 51	addcomd 11439	. . . . . 6 ⊢ (𝜑 → ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)))
53	5, 3, 9	sqdivd 14225	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)))
54		4cn 12353	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
56	55, 2	mulcld 11256	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
57		4ne0 12379	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ≠ 0)
59	55, 2, 58, 8	mulne0d 11893	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
60	56, 56, 49, 2, 59, 8	divmuldivd 12059	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)))
61	56, 59	dividd 12016	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) / (4 · 𝐴)) = 1)
62	61	eqcomd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = ((4 · 𝐴) / (4 · 𝐴)))
63	62	oveq1d 7431	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)))
64	50	mullidd 11254	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
65	63, 64	eqtr3d 2799	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
66	37	mulm1d 11693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 · 𝐶) = -𝐶)
67	66	eqcomd 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝐶 = (-1 · 𝐶))
68	67	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
69		neg1cn 12230	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -1 ∈ ℂ)
71	56, 70, 37	mulassd 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
72	68, 71	eqtr4d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶))
73	56, 70	mulcomd 11257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -1) = (-1 · (4 · 𝐴)))
74	73	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((-1 · (4 · 𝐴)) · 𝐶))
75	70, 56, 37	mulassd 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-1 · (4 · 𝐴)) · 𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
76	72, 74, 75	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
77	55, 2, 37	mulassd 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
78	77	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · ((4 · 𝐴) · 𝐶)) = (-1 · (4 · (𝐴 · 𝐶))))
79	2, 37	mulcld 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
80	55, 79	mulcld 11256	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
81	80	mulm1d 11693	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · (4 · (𝐴 · 𝐶))) = -(4 · (𝐴 · 𝐶)))
82	76, 78, 81	3eqtrd 2801	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)))
83		2t2e4 12431	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 2) = 4)
85	84	eqcomd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 4 = (2 · 2))
86	85	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (4 · 𝐴) = ((2 · 2) · 𝐴))
87	86	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (((2 · 2) · 𝐴) · 𝐴))
88	1, 1, 2	mulassd 11259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
89	88	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 2) · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
90	87, 89	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
91	1, 3	mulcomd 11257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (2 · 𝐴)) = ((2 · 𝐴) · 2))
92	91	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐴) = (((2 · 𝐴) · 2) · 𝐴))
93	3, 1, 2	mulassd 11259	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
94	90, 92, 93	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
95	3	sqvald 14209	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴)))
96	94, 95	eqtr4d 2800	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴)↑2))
97	82, 96	oveq12d 7434	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
98	60, 65, 97	3eqtr3d 2805	. . . . . . . 8 ⊢ (𝜑 → (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
99	53, 98	oveq12d 7434	. . . . . . 7 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
100	5	sqcld 14210	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
101	80	negcld 11583	. . . . . . . 8 ⊢ (𝜑 → -(4 · (𝐴 · 𝐶)) ∈ ℂ)
102	3	sqcld 14210	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ∈ ℂ)
103	3, 3, 9, 9	mulne0d 11893	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝐴) · (2 · 𝐴)) ≠ 0)
104	95, 103	eqnetrd 3024	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ≠ 0)
105	100, 101, 102, 104	divdird 12056	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
106	100, 80	negsubd 11602	. . . . . . . 8 ⊢ (𝜑 → ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
107	106	oveq1d 7431	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
108	99, 105, 107	3eqtr2d 2803	. . . . . 6 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
109	48, 52, 108	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
110	109	oveq2d 7432	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))))
111	100, 80	subcld 11596	. . . . 5 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ)
112	111, 102, 104	divcan2d 12020	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
113	12, 110, 112	3eqtrd 2801	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
114	3, 11	mulcld 11256	. . . 4 ⊢ (𝜑 → ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ)
115		eqsqrtor 15456	. . . 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 15529	. . . . 5 ⊢ (𝜑 → (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
119	3, 11, 118, 9	rdiv 12077	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
120	118, 3, 9	divcld 12018	. . . . 5 ⊢ (𝜑 → ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
121	4, 10, 120	addlsub 11657	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
122	5, 3, 9	divnegd 12031	. . . . . . . 8 ⊢ (𝜑 → -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)))
123	122	oveq2d 7432	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
124	120, 10	negsubd 11602	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
125	5	negcld 11583	. . . . . . . . 9 ⊢ (𝜑 → -𝐵 ∈ ℂ)
126	125, 3, 9	divcld 12018	. . . . . . . 8 ⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ)
127	120, 126	addcomd 11439	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
128	123, 124, 127	3eqtr3d 2805	. . . . . 6 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
129	125, 118, 3, 9	divdird 12056	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
130	128, 129	eqtr4d 2800	. . . . 5 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
131	130	eqeq2d 2773	. . . 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 11583	. . . . 5 ⊢ (𝜑 → -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
134	3, 11, 133, 9	rdiv 12077	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
135	133, 3, 9	divcld 12018	. . . . 5 ⊢ (𝜑 → (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
136	4, 10, 135	addlsub 11657	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
137	122	oveq2d 7432	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
138	135, 10	negsubd 11602	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
139	135, 126	addcomd 11439	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
140	137, 138, 139	3eqtr3d 2805	. . . . . 6 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
141	125, 133, 3, 9	divdird 12056	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
142	125, 118	negsubd 11602	. . . . . . 7 ⊢ (𝜑 → (-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
143	142	oveq1d 7431	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
144	140, 141, 143	3eqtr2d 2803	. . . . 5 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
145	144	eqeq2d 2773	. . . 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 2957 ‘cfv 6537 (class class class)co 7416 ℂcc 11125 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 − cmin 11468 -cneg 11469 / cdiv 11898 2c2 12322 4c4 12324 ↑cexp 14127 √csqrt 15322

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8699 df-en 8956 df-dom 8957 df-sdom 8958 df-sup 9415 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-n0 12532 df-z 12619 df-uz 12891 df-rp 13045 df-seq 14068 df-exp 14128 df-cj 15188 df-re 15189 df-im 15190 df-sqrt 15324 df-abs 15325

This theorem is used by: constrfin 34258

W3C validator