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 26892

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 12287	. . . . . . . 8 ⊢ 2 ∈ ℂ
2		quad.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		mulcl 11151	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · 𝐴) ∈ ℂ)
4	1, 2, 3	sylancr 596	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
5		quad.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
6	4, 5	mulcld 11196	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ)
7		quad.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	6, 7	addcld 11195	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ)
9	8	sqcld 14151	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ)
10		quad2.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ)
11	10	sqcld 14151	. . . 4 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
12	9, 11	subeq0ad 11546	. . 3 ⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
13	5	sqcld 14151	. . . . . . 7 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
14	2, 13	mulcld 11196	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
15	7, 5	mulcld 11196	. . . . . . 7 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
16		quad.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17	15, 16	addcld 11195	. . . . . 6 ⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ)
18	14, 17	addcld 11195	. . . . 5 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ)
19		0cnd 11166	. . . . 5 ⊢ (𝜑 → 0 ∈ ℂ)
20		4cn 12297	. . . . . 6 ⊢ 4 ∈ ℂ
21		mulcl 11151	. . . . . 6 ⊢ ((4 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (4 · 𝐴) ∈ ℂ)
22	20, 2, 21	sylancr 596	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
23	20	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ∈ ℂ)
24		4ne0 12323	. . . . . . 7 ⊢ 4 ≠ 0
25	24	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ≠ 0)
26		quad.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
27	23, 2, 25, 26	mulne0d 11833	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
28	18, 19, 22, 27	mulcand 11814	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0))
29	6	sqcld 14151	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ)
30	6, 7	mulcld 11196	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ)
31		mulcl 11151	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
32	1, 30, 31	sylancr 596	. . . . . . . 8 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
33	2, 16	mulcld 11196	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
34		mulcl 11151	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (4 · (𝐴 · 𝐶)) ∈ ℂ)
35	20, 33, 34	sylancr 596	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
36	29, 32, 35	addassd 11198	. . . . . . 7 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
37	7	sqcld 14151	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
38	29, 32	addcld 11195	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ)
39	37, 38, 35	pnncand 11575	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))))
40	4, 5	sqmuld 14165	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2)))
41		sq2 14204	. . . . . . . . . . . . 13 ⊢ (2↑2) = 4
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑2) = 4)
43	2	sqvald 14150	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7409	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑2) · (𝐴↑2)) = (4 · (𝐴 · 𝐴)))
45		sqmul 14126	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
46	1, 2, 45	sylancr 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
47	23, 2, 2	mulassd 11199	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴)))
48	44, 46, 47	3eqtr4d 2806	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴))
49	48	oveq1d 7406	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2)))
50	22, 2, 13	mulassd 11199	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2))))
51	40, 49, 50	3eqtrrd 2801	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2))
52	22, 15, 16	adddid 11200	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)))
53		2t2e4 12375	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
54	53	oveq1i 7401	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 2) · 𝐴) = (4 · 𝐴)
55	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
56	55, 55, 2	mulassd 11199	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
57	54, 56	eqtr3id 2810	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · 𝐴) = (2 · (2 · 𝐴)))
58	57	oveq1d 7406	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵))
59	55, 4, 7	mulassd 11199	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
60	58, 59	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
61	60	oveq1d 7406	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋))
62	4, 7	mulcld 11196	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ)
63	55, 62, 5	mulassd 11199	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
64	61, 63	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
65	22, 7, 5	mulassd 11199	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋)))
66	4, 7, 5	mul32d 11387	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵))
67	66	oveq2d 7407	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
68	64, 65, 67	3eqtr3d 2804	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
69	23, 2, 16	mulassd 11199	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
70	68, 69	oveq12d 7409	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
71	52, 70	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
72	51, 71	oveq12d 7409	. . . . . . 7 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
73	36, 39, 72	3eqtr4rd 2807	. . . . . 6 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
74	22, 14, 17	adddid 11200	. . . . . 6 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))))
75		binom2 14224	. . . . . . . . 9 ⊢ ((((2 · 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
76	6, 7, 75	syl2anc 593	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
77	38, 37, 76	comraddd 11391	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))))
78		quad2.2	. . . . . . 7 ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
79	77, 78	oveq12d 7409	. . . . . 6 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
80	73, 74, 79	3eqtr4d 2806	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)))
81	22	mul01d 11376	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · 0) = 0)
82	80, 81	eqeq12d 2777	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
83	28, 82	bitr3d 283	. . 3 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0))
84	6, 7	subnegd 11543	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵))
85	84	oveq1d 7406	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2))
86	85	eqeq1d 2763	. . 3 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
87	12, 83, 86	3bitr4d 313	. 2 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2)))
88	7	negcld 11523	. . . 4 ⊢ (𝜑 → -𝐵 ∈ ℂ)
89	6, 88	subcld 11536	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ)
90		sqeqor 14223	. . 3 ⊢ (((((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
91	89, 10, 90	syl2anc 593	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
92	6, 88, 10	subaddd 11554	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
93	88, 10	addcld 11195	. . . . . 6 ⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ)
94		2ne0 12318	. . . . . . . 8 ⊢ 2 ≠ 0
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
96	55, 2, 95, 26	mulne0d 11833	. . . . . 6 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
97	93, 4, 5, 96	divmuld 11983	. . . . 5 ⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)))
98		eqcom 2768	. . . . 5 ⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋)
99		eqcom 2768	. . . . 5 ⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))
100	97, 98, 99	3bitr4g 316	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
101	92, 100	bitr4d 284	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴))))
102	88, 10	negsubd 11542	. . . . 5 ⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷))
103	102	eqeq1d 2763	. . . 4 ⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
104	10	negcld 11523	. . . . 5 ⊢ (𝜑 → -𝐷 ∈ ℂ)
105	6, 88, 104	subaddd 11554	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋)))
106	88, 10	subcld 11536	. . . . . 6 ⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ)
107	106, 4, 5, 96	divmuld 11983	. . . . 5 ⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)))
108		eqcom 2768	. . . . 5 ⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋)
109		eqcom 2768	. . . . 5 ⊢ ((-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷))
110	107, 108, 109	3bitr4g 316	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
111	103, 105, 110	3bitr4d 313	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴))))
112	101, 111	orbi12d 929	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷) ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))
113	87, 91, 112	3bitrd 307	1 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 (class class class)co 7391 ℂcc 11065 0cc0 11067 + caddc 11070 · cmul 11072 − cmin 11408 -cneg 11409 / cdiv 11838 2c2 12266 4c4 12268 ↑cexp 14068

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 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 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-n0 12476 df-z 12563 df-uz 12834 df-seq 14009 df-exp 14069

This theorem is referenced by: quad 26893 dcubic2 26897 dquartlem1 26904

W3C validator