Theorem quad2 26816

Description: The quadratic equation, without specifying the particular branch 𝐷 to the square root. (Contributed by Mario Carneiro, 23-Apr-2015.)

Hypotheses

Ref	Expression
quad.a	⊢ (𝜑 → 𝐴 ∈ ℂ)
quad.z	⊢ (𝜑 → 𝐴 ≠ 0)
quad.b	⊢ (𝜑 → 𝐵 ∈ ℂ)
quad.c	⊢ (𝜑 → 𝐶 ∈ ℂ)
quad.x	⊢ (𝜑 → 𝑋 ∈ ℂ)
quad2.d	⊢ (𝜑 → 𝐷 ∈ ℂ)
quad2.2	⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))

Assertion

Ref	Expression
quad2	⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))

Proof of Theorem quad2

Step	Hyp	Ref	Expression
1		2cn 12320	. . . . . . . 8 ⊢ 2 ∈ ℂ
2		quad.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		mulcl 11224	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · 𝐴) ∈ ℂ)
4	1, 2, 3	sylancr 585	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
5		quad.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
6	4, 5	mulcld 11266	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ)
7		quad.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	6, 7	addcld 11265	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ)
9	8	sqcld 14144	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ)
10		quad2.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ)
11	10	sqcld 14144	. . . 4 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
12	9, 11	subeq0ad 11613	. . 3 ⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
13	5	sqcld 14144	. . . . . . 7 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
14	2, 13	mulcld 11266	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
15	7, 5	mulcld 11266	. . . . . . 7 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
16		quad.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17	15, 16	addcld 11265	. . . . . 6 ⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ)
18	14, 17	addcld 11265	. . . . 5 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ)
19		0cnd 11239	. . . . 5 ⊢ (𝜑 → 0 ∈ ℂ)
20		4cn 12330	. . . . . 6 ⊢ 4 ∈ ℂ
21		mulcl 11224	. . . . . 6 ⊢ ((4 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (4 · 𝐴) ∈ ℂ)
22	20, 2, 21	sylancr 585	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
23	20	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ∈ ℂ)
24		4ne0 12353	. . . . . . 7 ⊢ 4 ≠ 0
25	24	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ≠ 0)
26		quad.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
27	23, 2, 25, 26	mulne0d 11898	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
28	18, 19, 22, 27	mulcand 11879	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0))
29	6	sqcld 14144	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ)
30	6, 7	mulcld 11266	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ)
31		mulcl 11224	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
32	1, 30, 31	sylancr 585	. . . . . . . 8 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
33	2, 16	mulcld 11266	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
34		mulcl 11224	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (4 · (𝐴 · 𝐶)) ∈ ℂ)
35	20, 33, 34	sylancr 585	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
36	29, 32, 35	addassd 11268	. . . . . . 7 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
37	7	sqcld 14144	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
38	29, 32	addcld 11265	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ)
39	37, 38, 35	pnncand 11642	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))))
40	4, 5	sqmuld 14158	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2)))
41		sq2 14196	. . . . . . . . . . . . 13 ⊢ (2↑2) = 4
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑2) = 4)
43	2	sqvald 14143	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7437	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑2) · (𝐴↑2)) = (4 · (𝐴 · 𝐴)))
45		sqmul 14119	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
46	1, 2, 45	sylancr 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
47	23, 2, 2	mulassd 11269	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴)))
48	44, 46, 47	3eqtr4d 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴))
49	48	oveq1d 7434	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2)))
50	22, 2, 13	mulassd 11269	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2))))
51	40, 49, 50	3eqtrrd 2770	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2))
52	22, 15, 16	adddid 11270	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)))
53		2t2e4 12409	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
54	53	oveq1i 7429	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 2) · 𝐴) = (4 · 𝐴)
55	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
56	55, 55, 2	mulassd 11269	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
57	54, 56	eqtr3id 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · 𝐴) = (2 · (2 · 𝐴)))
58	57	oveq1d 7434	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵))
59	55, 4, 7	mulassd 11269	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
60	58, 59	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
61	60	oveq1d 7434	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋))
62	4, 7	mulcld 11266	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ)
63	55, 62, 5	mulassd 11269	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
64	61, 63	eqtrd 2765	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
65	22, 7, 5	mulassd 11269	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋)))
66	4, 7, 5	mul32d 11456	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵))
67	66	oveq2d 7435	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
68	64, 65, 67	3eqtr3d 2773	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
69	23, 2, 16	mulassd 11269	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
70	68, 69	oveq12d 7437	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
71	52, 70	eqtrd 2765	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
72	51, 71	oveq12d 7437	. . . . . . 7 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
73	36, 39, 72	3eqtr4rd 2776	. . . . . 6 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
74	22, 14, 17	adddid 11270	. . . . . 6 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))))
75		binom2 14216	. . . . . . . . 9 ⊢ ((((2 · 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
76	6, 7, 75	syl2anc 582	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
77	38, 37, 76	comraddd 11460	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))))
78		quad2.2	. . . . . . 7 ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
79	77, 78	oveq12d 7437	. . . . . 6 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
80	73, 74, 79	3eqtr4d 2775	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)))
81	22	mul01d 11445	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · 0) = 0)
82	80, 81	eqeq12d 2741	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
83	28, 82	bitr3d 280	. . 3 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
84	6, 7	subnegd 11610	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵))
85	84	oveq1d 7434	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2))
86	85	eqeq1d 2727	. . 3 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
87	12, 83, 86	3bitr4d 310	. 2 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2)))
88	7	negcld 11590	. . . 4 ⊢ (𝜑 → -𝐵 ∈ ℂ)
89	6, 88	subcld 11603	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ)
90		sqeqor 14215	. . 3 ⊢ (((((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
91	89, 10, 90	syl2anc 582	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
92	6, 88, 10	subaddd 11621	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
93	88, 10	addcld 11265	. . . . . 6 ⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ)
94		2ne0 12349	. . . . . . . 8 ⊢ 2 ≠ 0
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
96	55, 2, 95, 26	mulne0d 11898	. . . . . 6 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
97	93, 4, 5, 96	divmuld 12045	. . . . 5 ⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)))
98		eqcom 2732	. . . . 5 ⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋)
99		eqcom 2732	. . . . 5 ⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))
100	97, 98, 99	3bitr4g 313	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
101	92, 100	bitr4d 281	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴))))
102	88, 10	negsubd 11609	. . . . 5 ⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷))
103	102	eqeq1d 2727	. . . 4 ⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
104	10	negcld 11590	. . . . 5 ⊢ (𝜑 → -𝐷 ∈ ℂ)
105	6, 88, 104	subaddd 11621	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋)))
106	88, 10	subcld 11603	. . . . . 6 ⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ)
107	106, 4, 5, 96	divmuld 12045	. . . . 5 ⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)))
108		eqcom 2732	. . . . 5 ⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋)
109		eqcom 2732	. . . . 5 ⊢ ((-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷))
110	107, 108, 109	3bitr4g 313	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
111	103, 105, 110	3bitr4d 310	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))
112	101, 111	orbi12d 916	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷) ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))
113	87, 91, 112	3bitrd 304	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 845   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  (class class class)co 7419  ℂcc 11138  0cc0 11140   + caddc 11143   · cmul 11145   − cmin 11476  -cneg 11477   / cdiv 11903  2c2 12300  4c4 12302  ↑cexp 14062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-n0 12506  df-z 12592  df-uz 12856  df-seq 14003  df-exp 14063

This theorem is referenced by:  quad  26817  dcubic2  26821  dquartlem1  26828