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 32723

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 12195	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℂ)
2		quad3d.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3	1, 2	mulcld 11124	. . . . 5 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
4		quad3d.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
5		quad3d.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
6		2ne0 12221	. . . . . . . . 9 ⊢ 2 ≠ 0
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
8		quad3d.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ 0)
9	1, 2, 7, 8	mulne0d 11761	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
10	5, 3, 9	divcld 11889	. . . . . 6 ⊢ (𝜑 → (𝐵 / (2 · 𝐴)) ∈ ℂ)
11	4, 10	addcld 11123	. . . . 5 ⊢ (𝜑 → (𝑋 + (𝐵 / (2 · 𝐴))) ∈ ℂ)
12	3, 11	sqmuld 14057	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)))
13	4, 10	binom2d 14117	. . . . . . 7 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)))
14	4	sqcld 14043	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
15	2, 14	mulcld 11124	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
16	5, 4	mulcld 11124	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
17	15, 16, 2, 8	divdird 11927	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)))
18	14, 2, 8	divcan3d 11894	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) / 𝐴) = (𝑋↑2))
19	5, 4, 2, 8	div23d 11926	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝑋) / 𝐴) = ((𝐵 / 𝐴) · 𝑋))
20	18, 19	oveq12d 7359	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) / 𝐴) + ((𝐵 · 𝑋) / 𝐴)) = ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)))
21	17, 20	eqtr2d 2766	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴))
22	5, 2, 8	divcld 11889	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 𝐴) ∈ ℂ)
23	22, 4	mulcomd 11125	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (𝑋 · (𝐵 / 𝐴)))
24	4, 22	mulcld 11124	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · (𝐵 / 𝐴)) ∈ ℂ)
25	24, 1, 7	divcan2d 11891	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (𝑋 · (𝐵 / 𝐴)))
26	4, 22, 1, 7	divassd 11924	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · ((𝐵 / 𝐴) / 2)))
27	5, 2, 1, 8, 7	divdiv1d 11920	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (𝐴 · 2)))
28	2, 1	mulcomd 11125	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 2) = (2 · 𝐴))
29	28	oveq2d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 / (𝐴 · 2)) = (𝐵 / (2 · 𝐴)))
30	27, 29	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵 / 𝐴) / 2) = (𝐵 / (2 · 𝐴)))
31	30	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · ((𝐵 / 𝐴) / 2)) = (𝑋 · (𝐵 / (2 · 𝐴))))
32	26, 31	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 · (𝐵 / 𝐴)) / 2) = (𝑋 · (𝐵 / (2 · 𝐴))))
33	32	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑋 · (𝐵 / 𝐴)) / 2)) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
34	23, 25, 33	3eqtr2d 2771	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 𝐴) · 𝑋) = (2 · (𝑋 · (𝐵 / (2 · 𝐴)))))
35	34	oveq2d 7357	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) + ((𝐵 / 𝐴) · 𝑋)) = ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))))
36	15, 16	addcld 11123	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) ∈ ℂ)
37		quad3d.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ℂ)
38	15, 16, 37	addassd 11126	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) + 𝐶) = ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)))
39	36, 37, 38	mvlraddd 11519	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶))
40		quad3d.6	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)
41	40	oveq1d 7356	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = (0 − 𝐶))
42		df-neg 11339	. . . . . . . . . . . 12 ⊢ -𝐶 = (0 − 𝐶)
43	41, 42	eqtr4di 2783	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) − 𝐶) = -𝐶)
44	39, 43	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) = -𝐶)
45	44	oveq1d 7356	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + (𝐵 · 𝑋)) / 𝐴) = (-𝐶 / 𝐴))
46	21, 35, 45	3eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → ((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) = (-𝐶 / 𝐴))
47	46	oveq1d 7356	. . . . . . 7 ⊢ (𝜑 → (((𝑋↑2) + (2 · (𝑋 · (𝐵 / (2 · 𝐴))))) + ((𝐵 / (2 · 𝐴))↑2)) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
48	13, 47	eqtrd 2765	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)))
49	37	negcld 11451	. . . . . . . 8 ⊢ (𝜑 → -𝐶 ∈ ℂ)
50	49, 2, 8	divcld 11889	. . . . . . 7 ⊢ (𝜑 → (-𝐶 / 𝐴) ∈ ℂ)
51	10	sqcld 14043	. . . . . . 7 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) ∈ ℂ)
52	50, 51	addcomd 11307	. . . . . 6 ⊢ (𝜑 → ((-𝐶 / 𝐴) + ((𝐵 / (2 · 𝐴))↑2)) = (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)))
53	5, 3, 9	sqdivd 14058	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / (2 · 𝐴))↑2) = ((𝐵↑2) / ((2 · 𝐴)↑2)))
54		4cn 12202	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
55	54	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
56	55, 2	mulcld 11124	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
57		4ne0 12225	. . . . . . . . . . . 12 ⊢ 4 ≠ 0
58	57	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ≠ 0)
59	55, 2, 58, 8	mulne0d 11761	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
60	56, 56, 49, 2, 59, 8	divmuldivd 11930	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)))
61	56, 59	dividd 11887	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) / (4 · 𝐴)) = 1)
62	61	eqcomd 2736	. . . . . . . . . . 11 ⊢ (𝜑 → 1 = ((4 · 𝐴) / (4 · 𝐴)))
63	62	oveq1d 7356	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)))
64	50	mullidd 11122	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
65	63, 64	eqtr3d 2767	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) / (4 · 𝐴)) · (-𝐶 / 𝐴)) = (-𝐶 / 𝐴))
66	37	mulm1d 11561	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (-1 · 𝐶) = -𝐶)
67	66	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝐶 = (-1 · 𝐶))
68	67	oveq2d 7357	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
69		neg1cn 12102	. . . . . . . . . . . . . . 15 ⊢ -1 ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -1 ∈ ℂ)
71	56, 70, 37	mulassd 11127	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((4 · 𝐴) · (-1 · 𝐶)))
72	68, 71	eqtr4d 2768	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (((4 · 𝐴) · -1) · 𝐶))
73	56, 70	mulcomd 11125	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · -1) = (-1 · (4 · 𝐴)))
74	73	oveq1d 7356	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · -1) · 𝐶) = ((-1 · (4 · 𝐴)) · 𝐶))
75	70, 56, 37	mulassd 11127	. . . . . . . . . . . 12 ⊢ (𝜑 → ((-1 · (4 · 𝐴)) · 𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
76	72, 74, 75	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = (-1 · ((4 · 𝐴) · 𝐶)))
77	55, 2, 37	mulassd 11127	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
78	77	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · ((4 · 𝐴) · 𝐶)) = (-1 · (4 · (𝐴 · 𝐶))))
79	2, 37	mulcld 11124	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
80	55, 79	mulcld 11124	. . . . . . . . . . . 12 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
81	80	mulm1d 11561	. . . . . . . . . . 11 ⊢ (𝜑 → (-1 · (4 · (𝐴 · 𝐶))) = -(4 · (𝐴 · 𝐶)))
82	76, 78, 81	3eqtrd 2769	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · -𝐶) = -(4 · (𝐴 · 𝐶)))
83		2t2e4 12276	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · 2) = 4)
85	84	eqcomd 2736	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 4 = (2 · 2))
86	85	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (4 · 𝐴) = ((2 · 2) · 𝐴))
87	86	oveq1d 7356	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (((2 · 2) · 𝐴) · 𝐴))
88	1, 1, 2	mulassd 11127	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
89	88	oveq1d 7356	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 2) · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
90	87, 89	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · (2 · 𝐴)) · 𝐴))
91	1, 3	mulcomd 11125	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (2 · 𝐴)) = ((2 · 𝐴) · 2))
92	91	oveq1d 7356	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐴) = (((2 · 𝐴) · 2) · 𝐴))
93	3, 1, 2	mulassd 11127	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 2) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
94	90, 92, 93	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴) · (2 · 𝐴)))
95	3	sqvald 14042	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2 · 𝐴) · (2 · 𝐴)))
96	94, 95	eqtr4d 2768	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = ((2 · 𝐴)↑2))
97	82, 96	oveq12d 7359	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · -𝐶) / ((4 · 𝐴) · 𝐴)) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
98	60, 65, 97	3eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → (-𝐶 / 𝐴) = (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2)))
99	53, 98	oveq12d 7359	. . . . . . 7 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
100	5	sqcld 14043	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
101	80	negcld 11451	. . . . . . . 8 ⊢ (𝜑 → -(4 · (𝐴 · 𝐶)) ∈ ℂ)
102	3	sqcld 14043	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ∈ ℂ)
103	3, 3, 9, 9	mulne0d 11761	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝐴) · (2 · 𝐴)) ≠ 0)
104	95, 103	eqnetrd 2993	. . . . . . . 8 ⊢ (𝜑 → ((2 · 𝐴)↑2) ≠ 0)
105	100, 101, 102, 104	divdird 11927	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) / ((2 · 𝐴)↑2)) + (-(4 · (𝐴 · 𝐶)) / ((2 · 𝐴)↑2))))
106	100, 80	negsubd 11470	. . . . . . . 8 ⊢ (𝜑 → ((𝐵↑2) + -(4 · (𝐴 · 𝐶))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
107	106	oveq1d 7356	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + -(4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
108	99, 105, 107	3eqtr2d 2771	. . . . . 6 ⊢ (𝜑 → (((𝐵 / (2 · 𝐴))↑2) + (-𝐶 / 𝐴)) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
109	48, 52, 108	3eqtrd 2769	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴)))↑2) = (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2)))
110	109	oveq2d 7357	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · ((𝑋 + (𝐵 / (2 · 𝐴)))↑2)) = (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))))
111	100, 80	subcld 11464	. . . . 5 ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ)
112	111, 102, 104	divcan2d 11891	. . . 4 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (((𝐵↑2) − (4 · (𝐴 · 𝐶))) / ((2 · 𝐴)↑2))) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
113	12, 110, 112	3eqtrd 2769	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
114	3, 11	mulcld 11124	. . . 4 ⊢ (𝜑 → ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ)
115		eqsqrtor 15266	. . . 4 ⊢ ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) ∈ ℂ ∧ ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ∈ ℂ) → ((((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴))))↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ↔ (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∨ ((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))))))
116	114, 111, 115	syl2anc 584	. . 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 15339	. . . . 5 ⊢ (𝜑 → (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
119	3, 11, 118, 9	rdiv 11948	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
120	118, 3, 9	divcld 11889	. . . . 5 ⊢ (𝜑 → ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
121	4, 10, 120	addlsub 11525	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
122	5, 3, 9	divnegd 11902	. . . . . . . 8 ⊢ (𝜑 → -(𝐵 / (2 · 𝐴)) = (-𝐵 / (2 · 𝐴)))
123	122	oveq2d 7357	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
124	120, 10	negsubd 11470	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
125	5	negcld 11451	. . . . . . . . 9 ⊢ (𝜑 → -𝐵 ∈ ℂ)
126	125, 3, 9	divcld 11889	. . . . . . . 8 ⊢ (𝜑 → (-𝐵 / (2 · 𝐴)) ∈ ℂ)
127	120, 126	addcomd 11307	. . . . . . 7 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
128	123, 124, 127	3eqtr3d 2773	. . . . . 6 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
129	125, 118, 3, 9	divdird 11927	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + ((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
130	128, 129	eqtr4d 2768	. . . . 5 ⊢ (𝜑 → (((√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
131	130	eqeq2d 2741	. . . 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 11451	. . . . 5 ⊢ (𝜑 → -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ∈ ℂ)
134	3, 11, 133, 9	rdiv 11948	. . . 4 ⊢ (𝜑 → (((2 · 𝐴) · (𝑋 + (𝐵 / (2 · 𝐴)))) = -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ↔ (𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
135	133, 3, 9	divcld 11889	. . . . 5 ⊢ (𝜑 → (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ∈ ℂ)
136	4, 10, 135	addlsub 11525	. . . 4 ⊢ (𝜑 → ((𝑋 + (𝐵 / (2 · 𝐴))) = (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) ↔ 𝑋 = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴)))))
137	122	oveq2d 7357	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))))
138	135, 10	negsubd 11470	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + -(𝐵 / (2 · 𝐴))) = ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))))
139	135, 126	addcomd 11307	. . . . . . 7 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) + (-𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
140	137, 138, 139	3eqtr3d 2773	. . . . . 6 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
141	125, 133, 3, 9	divdird 11927	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 / (2 · 𝐴)) + (-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴))))
142	125, 118	negsubd 11470	. . . . . . 7 ⊢ (𝜑 → (-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) = (-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))))
143	142	oveq1d 7356	. . . . . 6 ⊢ (𝜑 → ((-𝐵 + -(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
144	140, 141, 143	3eqtr2d 2771	. . . . 5 ⊢ (𝜑 → ((-(√‘((𝐵↑2) − (4 · (𝐴 · 𝐶)))) / (2 · 𝐴)) − (𝐵 / (2 · 𝐴))) = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
145	144	eqeq2d 2741	. . . 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 918	. 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 847 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ‘cfv 6477 (class class class)co 7341 ℂcc 10996 0cc0 10998 1c1 10999 + caddc 11001 · cmul 11003 − cmin 11336 -cneg 11337 / cdiv 11766 2c2 12172 4c4 12174 ↑cexp 13960 √csqrt 15132

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075 ax-pre-sup 11076

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-sup 9321 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-div 11767 df-nn 12118 df-2 12180 df-3 12181 df-4 12182 df-n0 12374 df-z 12461 df-uz 12725 df-rp 12883 df-seq 13901 df-exp 13961 df-cj 14998 df-re 14999 df-im 15000 df-sqrt 15134 df-abs 15135

This theorem is referenced by: constrfin 33749

W3C validator