quad2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > quad2		Structured version Visualization version GIF version

Theorem quad2 26805

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 12220	. . . . . . . 8 ⊢ 2 ∈ ℂ
2		quad.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		mulcl 11110	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · 𝐴) ∈ ℂ)
4	1, 2, 3	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
5		quad.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
6	4, 5	mulcld 11152	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ)
7		quad.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	6, 7	addcld 11151	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ)
9	8	sqcld 14067	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ)
10		quad2.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ)
11	10	sqcld 14067	. . . 4 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
12	9, 11	subeq0ad 11502	. . 3 ⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
13	5	sqcld 14067	. . . . . . 7 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
14	2, 13	mulcld 11152	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
15	7, 5	mulcld 11152	. . . . . . 7 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
16		quad.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17	15, 16	addcld 11151	. . . . . 6 ⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ)
18	14, 17	addcld 11151	. . . . 5 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ)
19		0cnd 11125	. . . . 5 ⊢ (𝜑 → 0 ∈ ℂ)
20		4cn 12230	. . . . . 6 ⊢ 4 ∈ ℂ
21		mulcl 11110	. . . . . 6 ⊢ ((4 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (4 · 𝐴) ∈ ℂ)
22	20, 2, 21	sylancr 587	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
23	20	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ∈ ℂ)
24		4ne0 12253	. . . . . . 7 ⊢ 4 ≠ 0
25	24	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ≠ 0)
26		quad.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
27	23, 2, 25, 26	mulne0d 11789	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
28	18, 19, 22, 27	mulcand 11770	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0))
29	6	sqcld 14067	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ)
30	6, 7	mulcld 11152	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ)
31		mulcl 11110	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
32	1, 30, 31	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
33	2, 16	mulcld 11152	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
34		mulcl 11110	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (4 · (𝐴 · 𝐶)) ∈ ℂ)
35	20, 33, 34	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
36	29, 32, 35	addassd 11154	. . . . . . 7 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
37	7	sqcld 14067	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
38	29, 32	addcld 11151	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ)
39	37, 38, 35	pnncand 11531	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))))
40	4, 5	sqmuld 14081	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2)))
41		sq2 14120	. . . . . . . . . . . . 13 ⊢ (2↑2) = 4
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑2) = 4)
43	2	sqvald 14066	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7376	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑2) · (𝐴↑2)) = (4 · (𝐴 · 𝐴)))
45		sqmul 14042	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
46	1, 2, 45	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
47	23, 2, 2	mulassd 11155	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴)))
48	44, 46, 47	3eqtr4d 2781	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴))
49	48	oveq1d 7373	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2)))
50	22, 2, 13	mulassd 11155	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2))))
51	40, 49, 50	3eqtrrd 2776	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2))
52	22, 15, 16	adddid 11156	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)))
53		2t2e4 12304	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
54	53	oveq1i 7368	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 2) · 𝐴) = (4 · 𝐴)
55	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
56	55, 55, 2	mulassd 11155	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
57	54, 56	eqtr3id 2785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · 𝐴) = (2 · (2 · 𝐴)))
58	57	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵))
59	55, 4, 7	mulassd 11155	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
60	58, 59	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
61	60	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋))
62	4, 7	mulcld 11152	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ)
63	55, 62, 5	mulassd 11155	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
64	61, 63	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
65	22, 7, 5	mulassd 11155	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋)))
66	4, 7, 5	mul32d 11343	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵))
67	66	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
68	64, 65, 67	3eqtr3d 2779	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
69	23, 2, 16	mulassd 11155	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
70	68, 69	oveq12d 7376	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
71	52, 70	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
72	51, 71	oveq12d 7376	. . . . . . 7 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
73	36, 39, 72	3eqtr4rd 2782	. . . . . 6 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
74	22, 14, 17	adddid 11156	. . . . . 6 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))))
75		binom2 14140	. . . . . . . . 9 ⊢ ((((2 · 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
76	6, 7, 75	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
77	38, 37, 76	comraddd 11347	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))))
78		quad2.2	. . . . . . 7 ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
79	77, 78	oveq12d 7376	. . . . . 6 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
80	73, 74, 79	3eqtr4d 2781	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)))
81	22	mul01d 11332	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · 0) = 0)
82	80, 81	eqeq12d 2752	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
83	28, 82	bitr3d 281	. . 3 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
84	6, 7	subnegd 11499	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵))
85	84	oveq1d 7373	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2))
86	85	eqeq1d 2738	. . 3 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
87	12, 83, 86	3bitr4d 311	. 2 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2)))
88	7	negcld 11479	. . . 4 ⊢ (𝜑 → -𝐵 ∈ ℂ)
89	6, 88	subcld 11492	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ)
90		sqeqor 14139	. . 3 ⊢ (((((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
91	89, 10, 90	syl2anc 584	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
92	6, 88, 10	subaddd 11510	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
93	88, 10	addcld 11151	. . . . . 6 ⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ)
94		2ne0 12249	. . . . . . . 8 ⊢ 2 ≠ 0
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
96	55, 2, 95, 26	mulne0d 11789	. . . . . 6 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
97	93, 4, 5, 96	divmuld 11939	. . . . 5 ⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)))
98		eqcom 2743	. . . . 5 ⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋)
99		eqcom 2743	. . . . 5 ⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))
100	97, 98, 99	3bitr4g 314	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
101	92, 100	bitr4d 282	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴))))
102	88, 10	negsubd 11498	. . . . 5 ⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷))
103	102	eqeq1d 2738	. . . 4 ⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
104	10	negcld 11479	. . . . 5 ⊢ (𝜑 → -𝐷 ∈ ℂ)
105	6, 88, 104	subaddd 11510	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋)))
106	88, 10	subcld 11492	. . . . . 6 ⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ)
107	106, 4, 5, 96	divmuld 11939	. . . . 5 ⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)))
108		eqcom 2743	. . . . 5 ⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋)
109		eqcom 2743	. . . . 5 ⊢ ((-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷))
110	107, 108, 109	3bitr4g 314	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
111	103, 105, 110	3bitr4d 311	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))
112	101, 111	orbi12d 918	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷) ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))
113	87, 91, 112	3bitrd 305	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 (class class class)co 7358 ℂcc 11024 0cc0 11026 + caddc 11029 · cmul 11031 − cmin 11364 -cneg 11365 / cdiv 11794 2c2 12200 4c4 12202 ↑cexp 13984

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

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 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-n0 12402 df-z 12489 df-uz 12752 df-seq 13925 df-exp 13985

This theorem is referenced by: quad 26806 dcubic2 26810 dquartlem1 26817

W3C validator