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 25415

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 11710	. . . . . . . 8 ⊢ 2 ∈ ℂ
2		quad.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		mulcl 10618	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · 𝐴) ∈ ℂ)
4	1, 2, 3	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
5		quad.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
6	4, 5	mulcld 10658	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ)
7		quad.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	6, 7	addcld 10657	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ)
9	8	sqcld 13506	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ)
10		quad2.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ)
11	10	sqcld 13506	. . . 4 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
12	9, 11	subeq0ad 11004	. . 3 ⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
13	5	sqcld 13506	. . . . . . 7 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
14	2, 13	mulcld 10658	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
15	7, 5	mulcld 10658	. . . . . . 7 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
16		quad.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17	15, 16	addcld 10657	. . . . . 6 ⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ)
18	14, 17	addcld 10657	. . . . 5 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ)
19		0cnd 10631	. . . . 5 ⊢ (𝜑 → 0 ∈ ℂ)
20		4cn 11720	. . . . . 6 ⊢ 4 ∈ ℂ
21		mulcl 10618	. . . . . 6 ⊢ ((4 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (4 · 𝐴) ∈ ℂ)
22	20, 2, 21	sylancr 589	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
23	20	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ∈ ℂ)
24		4ne0 11743	. . . . . . 7 ⊢ 4 ≠ 0
25	24	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ≠ 0)
26		quad.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
27	23, 2, 25, 26	mulne0d 11289	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
28	18, 19, 22, 27	mulcand 11270	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0))
29	6	sqcld 13506	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ)
30	6, 7	mulcld 10658	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ)
31		mulcl 10618	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
32	1, 30, 31	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
33	2, 16	mulcld 10658	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
34		mulcl 10618	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (4 · (𝐴 · 𝐶)) ∈ ℂ)
35	20, 33, 34	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
36	29, 32, 35	addassd 10660	. . . . . . 7 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
37	7	sqcld 13506	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
38	29, 32	addcld 10657	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ)
39	37, 38, 35	pnncand 11033	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))))
40	4, 5	sqmuld 13520	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2)))
41		sq2 13558	. . . . . . . . . . . . 13 ⊢ (2↑2) = 4
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑2) = 4)
43	2	sqvald 13505	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7171	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑2) · (𝐴↑2)) = (4 · (𝐴 · 𝐴)))
45		sqmul 13483	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
46	1, 2, 45	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
47	23, 2, 2	mulassd 10661	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴)))
48	44, 46, 47	3eqtr4d 2865	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴))
49	48	oveq1d 7168	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2)))
50	22, 2, 13	mulassd 10661	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2))))
51	40, 49, 50	3eqtrrd 2860	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2))
52	22, 15, 16	adddid 10662	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)))
53		2t2e4 11799	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
54	53	oveq1i 7163	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 2) · 𝐴) = (4 · 𝐴)
55	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
56	55, 55, 2	mulassd 10661	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
57	54, 56	syl5eqr 2869	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · 𝐴) = (2 · (2 · 𝐴)))
58	57	oveq1d 7168	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵))
59	55, 4, 7	mulassd 10661	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
60	58, 59	eqtrd 2855	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
61	60	oveq1d 7168	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋))
62	4, 7	mulcld 10658	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ)
63	55, 62, 5	mulassd 10661	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
64	61, 63	eqtrd 2855	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
65	22, 7, 5	mulassd 10661	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋)))
66	4, 7, 5	mul32d 10847	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵))
67	66	oveq2d 7169	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
68	64, 65, 67	3eqtr3d 2863	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
69	23, 2, 16	mulassd 10661	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
70	68, 69	oveq12d 7171	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
71	52, 70	eqtrd 2855	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
72	51, 71	oveq12d 7171	. . . . . . 7 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
73	36, 39, 72	3eqtr4rd 2866	. . . . . 6 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
74	22, 14, 17	adddid 10662	. . . . . 6 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))))
75		binom2 13577	. . . . . . . . 9 ⊢ ((((2 · 𝐴) · 𝑋) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
76	6, 7, 75	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (𝐵↑2)))
77	38, 37, 76	comraddd 10851	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))))
78		quad2.2	. . . . . . 7 ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
79	77, 78	oveq12d 7171	. . . . . 6 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
80	73, 74, 79	3eqtr4d 2865	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)))
81	22	mul01d 10836	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · 0) = 0)
82	80, 81	eqeq12d 2836	. . . 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 11001	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵))
85	84	oveq1d 7168	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2))
86	85	eqeq1d 2822	. . 3 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
87	12, 83, 86	3bitr4d 313	. 2 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2)))
88	7	negcld 10981	. . . 4 ⊢ (𝜑 → -𝐵 ∈ ℂ)
89	6, 88	subcld 10994	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ)
90		sqeqor 13576	. . 3 ⊢ (((((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
91	89, 10, 90	syl2anc 586	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
92	6, 88, 10	subaddd 11012	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
93	88, 10	addcld 10657	. . . . . 6 ⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ)
94		2ne0 11739	. . . . . . . 8 ⊢ 2 ≠ 0
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
96	55, 2, 95, 26	mulne0d 11289	. . . . . 6 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
97	93, 4, 5, 96	divmuld 11435	. . . . 5 ⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)))
98		eqcom 2827	. . . . 5 ⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋)
99		eqcom 2827	. . . . 5 ⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))
100	97, 98, 99	3bitr4g 316	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
101	92, 100	bitr4d 284	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴))))
102	88, 10	negsubd 11000	. . . . 5 ⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷))
103	102	eqeq1d 2822	. . . 4 ⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
104	10	negcld 10981	. . . . 5 ⊢ (𝜑 → -𝐷 ∈ ℂ)
105	6, 88, 104	subaddd 11012	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋)))
106	88, 10	subcld 10994	. . . . . 6 ⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ)
107	106, 4, 5, 96	divmuld 11435	. . . . 5 ⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)))
108		eqcom 2827	. . . . 5 ⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋)
109		eqcom 2827	. . . . 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 915	. 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 843 = wceq 1536 ∈ wcel 2113 ≠ wne 3015 (class class class)co 7153 ℂcc 10532 0cc0 10534 + caddc 10537 · cmul 10539 − cmin 10867 -cneg 10868 / cdiv 11294 2c2 11690 4c4 11692 ↑cexp 13427

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2792 ax-sep 5200 ax-nul 5207 ax-pow 5263 ax-pr 5327 ax-un 7458 ax-cnex 10590 ax-resscn 10591 ax-1cn 10592 ax-icn 10593 ax-addcl 10594 ax-addrcl 10595 ax-mulcl 10596 ax-mulrcl 10597 ax-mulcom 10598 ax-addass 10599 ax-mulass 10600 ax-distr 10601 ax-i2m1 10602 ax-1ne0 10603 ax-1rid 10604 ax-rnegex 10605 ax-rrecex 10606 ax-cnre 10607 ax-pre-lttri 10608 ax-pre-lttrn 10609 ax-pre-ltadd 10610 ax-pre-mulgt0 10611

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2892 df-nfc 2962 df-ne 3016 df-nel 3123 df-ral 3142 df-rex 3143 df-reu 3144 df-rmo 3145 df-rab 3146 df-v 3495 df-sbc 3771 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4465 df-pw 4538 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-uni 4836 df-iun 4918 df-br 5064 df-opab 5126 df-mpt 5144 df-tr 5170 df-id 5457 df-eprel 5462 df-po 5471 df-so 5472 df-fr 5511 df-we 5513 df-xp 5558 df-rel 5559 df-cnv 5560 df-co 5561 df-dm 5562 df-rn 5563 df-res 5564 df-ima 5565 df-pred 6145 df-ord 6191 df-on 6192 df-lim 6193 df-suc 6194 df-iota 6311 df-fun 6354 df-fn 6355 df-f 6356 df-f1 6357 df-fo 6358 df-f1o 6359 df-fv 6360 df-riota 7111 df-ov 7156 df-oprab 7157 df-mpo 7158 df-om 7578 df-2nd 7687 df-wrecs 7944 df-recs 8005 df-rdg 8043 df-er 8286 df-en 8507 df-dom 8508 df-sdom 8509 df-pnf 10674 df-mnf 10675 df-xr 10676 df-ltxr 10677 df-le 10678 df-sub 10869 df-neg 10870 df-div 11295 df-nn 11636 df-2 11698 df-3 11699 df-4 11700 df-n0 11896 df-z 11980 df-uz 12242 df-seq 13368 df-exp 13428

This theorem is referenced by: quad 25416 dcubic2 25420 dquartlem1 25427

W3C validator