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 33105

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 12325	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
2		quad3d.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1, 2	mulcld 11235	. . . . 5 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
4		quad3d.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
5		quad3d.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
6		2ne0 12353	. . . . . . . . 9 ⊢ 2 ≠ 0
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
8		quad3d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ 0)
9	1, 2, 7, 8	mulne0d 11872	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
10	5, 3, 9	divcld 11997	. . . . . 6 ⊢ (𝜑 → (𝐵 / (2 · 𝐴)) ∈ ℂ)
11	4, 10	addcld 11234	. . . . 5 ⊢ (𝜑 → (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ)
12	3, 11	sqmuld 14201	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)))
13	4, 10	binom2d 14261	. . . . . . 7 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)))
14	4	sqcld 14187	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
15	2, 14	mulcld 11235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
16	5, 4	mulcld 11235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
17	15, 16, 2, 8	divdird 12035	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)))
18	14, 2, 8	divcan3d 12002	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2))
19	5, 4, 2, 8	div23d 12034	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋))
20	18, 19	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)))
21	17, 20	eqtr2d 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴))
22	5, 2, 8	divcld 11997	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ)
23	22, 4	mulcomd 11236	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)))
24	4, 22	mulcld 11235	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐵 / 𝐴)) ∈ ℂ)
25	24, 1, 7	divcan2d 11999	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)))
26	4, 22, 1, 7	divassd 12032	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)))
27	5, 2, 1, 8, 7	divdiv1d 12028	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)))
28	2, 1	mulcomd 11236	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 2) = (2 · 𝐴))
29	28	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)))
30	27, 29	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)))
31	30	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))))
32	26, 31	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))))
33	32	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
34	23, 25, 33	3eqtr2d 2803	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
35	34	oveq2d 7428	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))))
36	15, 16	addcld 11234	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ)
37		quad3d.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
38	15, 16, 37	addassd 11237	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)))
39	36, 37, 38	mvlraddd 11630	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶))
40		quad3d.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)
41	40	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶))
42		df-neg 11450	. . . . . . . . . . . 12 ⊢ -𝐶 = (0 − 𝐶)
43	41, 42	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶)
44	39, 43	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶)
45	44	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴))
46	21, 35, 45	3eqtr3d 2805	. . . . . . . 8 ⊢ (𝜑 → ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴))
47	46	oveq1d 7427	. . . . . . 7 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
48	13, 47	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
49	37	negcld 11562	. . . . . . . 8 ⊢ (𝜑 → -𝐶 ∈ ℂ)
50	49, 2, 8	divcld 11997	. . . . . . 7 ⊢ (𝜑 → (-𝐶 / 𝐴) ∈ ℂ)
51	10	sqcld 14187	. . . . . . 7 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ)
52	50, 51	addcomd 11418	. . . . . 6 ⊢ (𝜑 → ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)))
53	5, 3, 9	sqdivd 14202	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)))
54		4cn 12332	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
56	55, 2	mulcld 11235	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
57		4ne0 12358	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ≠ 0)
59	55, 2, 58, 8	mulne0d 11872	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
60	56, 56, 49, 2, 59, 8	divmuldivd 12038	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)))
61	56, 59	dividd 11995	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) / (4 · 𝐴)) = 1)
62	61	eqcomd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = ((4 · 𝐴) / (4 · 𝐴)))
63	62	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)))
64	50	mullidd 11233	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
65	63, 64	eqtr3d 2799	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
66	37	mulm1d 11672	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 · 𝐶) = -𝐶)
67	66	eqcomd 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝐶 = (-1 · 𝐶))
68	67	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
69		neg1cn 12209	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -1 ∈ ℂ)
71	56, 70, 37	mulassd 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
72	68, 71	eqtr4d 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶))
73	56, 70	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -1) = (-1 · (4 · 𝐴)))
74	73	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((-1 · (4 · 𝐴)) · 𝐶))
75	70, 56, 37	mulassd 11238	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-1 · (4 · 𝐴)) · 𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
76	72, 74, 75	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
77	55, 2, 37	mulassd 11238	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
78	77	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · ((4 · 𝐴) · 𝐶)) = (-1 · (4 · (𝐴 · 𝐶))))
79	2, 37	mulcld 11235	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
80	55, 79	mulcld 11235	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
81	80	mulm1d 11672	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · (4 · (𝐴 · 𝐶))) = -(4 · (𝐴 · 𝐶)))
82	76, 78, 81	3eqtrd 2801	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)))
83		2t2e4 12410	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 2) = 4)
85	84	eqcomd 2768	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 4 = (2 · 2))
86	85	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (4 · 𝐴) = ((2 · 2) · 𝐴))
87	86	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (((2 · 2) · 𝐴) · 𝐴))
88	1, 1, 2	mulassd 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
89	88	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 2) · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
90	87, 89	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
91	1, 3	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (2 · 𝐴)) = ((2 · 𝐴) · 2))
92	91	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐴) = (((2 · 𝐴) · 2) · 𝐴))
93	3, 1, 2	mulassd 11238	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
94	90, 92, 93	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
95	3	sqvald 14186	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴)))
96	94, 95	eqtr4d 2800	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴)↑2))
97	82, 96	oveq12d 7430	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
98	60, 65, 97	3eqtr3d 2805	. . . . . . . 8 ⊢ (𝜑 → (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
99	53, 98	oveq12d 7430	. . . . . . 7 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
100	5	sqcld 14187	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
101	80	negcld 11562	. . . . . . . 8 ⊢ (𝜑 → -(4 · (𝐴 · 𝐶)) ∈ ℂ)
102	3	sqcld 14187	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ∈ ℂ)
103	3, 3, 9, 9	mulne0d 11872	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝐴) · (2 · 𝐴)) ≠ 0)
104	95, 103	eqnetrd 3024	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ≠ 0)
105	100, 101, 102, 104	divdird 12035	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
106	100, 80	negsubd 11581	. . . . . . . 8 ⊢ (𝜑 → ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
107	106	oveq1d 7427	. . . . . . 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 7428	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))))
111	100, 80	subcld 11575	. . . . 5 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ)
112	111, 102, 104	divcan2d 11999	. . . 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 11235	. . . 4 ⊢ (𝜑 → ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ)
115		eqsqrtor 15425	. . . 4 ⊢ ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ) → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
116	114, 111, 115	syl2anc 595	. . 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 15498	. . . . 5 ⊢ (𝜑 → (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
119	3, 11, 118, 9	rdiv 12056	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
120	118, 3, 9	divcld 11997	. . . . 5 ⊢ (𝜑 → ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
121	4, 10, 120	addlsub 11636	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
122	5, 3, 9	divnegd 12010	. . . . . . . 8 ⊢ (𝜑 → -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)))
123	122	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
124	120, 10	negsubd 11581	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
125	5	negcld 11562	. . . . . . . . 9 ⊢ (𝜑 → -𝐵 ∈ ℂ)
126	125, 3, 9	divcld 11997	. . . . . . . 8 ⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ)
127	120, 126	addcomd 11418	. . . . . . 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 12035	. . . . . 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 11562	. . . . 5 ⊢ (𝜑 → -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
134	3, 11, 133, 9	rdiv 12056	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
135	133, 3, 9	divcld 11997	. . . . 5 ⊢ (𝜑 → (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
136	4, 10, 135	addlsub 11636	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
137	122	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
138	135, 10	negsubd 11581	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
139	135, 126	addcomd 11418	. . . . . . 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 12035	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
142	125, 118	negsubd 11581	. . . . . . 7 ⊢ (𝜑 → (-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
143	142	oveq1d 7427	. . . . . 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 931	. 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 860 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 − cmin 11447 -cneg 11448 / cdiv 11877 2c2 12301 4c4 12303 ↑cexp 14104 √csqrt 15291

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 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 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-sup 9400 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-n0 12511 df-z 12598 df-uz 12869 df-rp 13023 df-seq 14045 df-exp 14105 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294

This theorem is used by: constrfin 34145

W3C validator