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 25419

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 11715	. . . . . . . 8 ⊢ 2 ∈ ℂ
2		quad.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		mulcl 10623	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (2 · 𝐴) ∈ ℂ)
4	1, 2, 3	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐴) ∈ ℂ)
5		quad.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℂ)
6	4, 5	mulcld 10663	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐴) · 𝑋) ∈ ℂ)
7		quad.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℂ)
8	6, 7	addcld 10662	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) + 𝐵) ∈ ℂ)
9	8	sqcld 13511	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) ∈ ℂ)
10		quad2.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ)
11	10	sqcld 13511	. . . 4 ⊢ (𝜑 → (𝐷↑2) ∈ ℂ)
12	9, 11	subeq0ad 11009	. . 3 ⊢ (𝜑 → ((((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = 0 ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
13	5	sqcld 13511	. . . . . . 7 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
14	2, 13	mulcld 10663	. . . . . 6 ⊢ (𝜑 → (𝐴 · (𝑋↑2)) ∈ ℂ)
15	7, 5	mulcld 10663	. . . . . . 7 ⊢ (𝜑 → (𝐵 · 𝑋) ∈ ℂ)
16		quad.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17	15, 16	addcld 10662	. . . . . 6 ⊢ (𝜑 → ((𝐵 · 𝑋) + 𝐶) ∈ ℂ)
18	14, 17	addcld 10662	. . . . 5 ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) ∈ ℂ)
19		0cnd 10636	. . . . 5 ⊢ (𝜑 → 0 ∈ ℂ)
20		4cn 11725	. . . . . 6 ⊢ 4 ∈ ℂ
21		mulcl 10623	. . . . . 6 ⊢ ((4 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (4 · 𝐴) ∈ ℂ)
22	20, 2, 21	sylancr 589	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ∈ ℂ)
23	20	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ∈ ℂ)
24		4ne0 11748	. . . . . . 7 ⊢ 4 ≠ 0
25	24	a1i 11	. . . . . 6 ⊢ (𝜑 → 4 ≠ 0)
26		quad.z	. . . . . 6 ⊢ (𝜑 → 𝐴 ≠ 0)
27	23, 2, 25, 26	mulne0d 11294	. . . . 5 ⊢ (𝜑 → (4 · 𝐴) ≠ 0)
28	18, 19, 22, 27	mulcand 11275	. . . 4 ⊢ (𝜑 → (((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = ((4 · 𝐴) · 0) ↔ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0))
29	6	sqcld 13511	. . . . . . . 8 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) ∈ ℂ)
30	6, 7	mulcld 10663	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ)
31		mulcl 10623	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ (((2 · 𝐴) · 𝑋) · 𝐵) ∈ ℂ) → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
32	1, 30, 31	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝑋) · 𝐵)) ∈ ℂ)
33	2, 16	mulcld 10663	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
34		mulcl 10623	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝐴 · 𝐶) ∈ ℂ) → (4 · (𝐴 · 𝐶)) ∈ ℂ)
35	20, 33, 34	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝐴 · 𝐶)) ∈ ℂ)
36	29, 32, 35	addassd 10665	. . . . . . 7 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
37	7	sqcld 13511	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
38	29, 32	addcld 10662	. . . . . . . 8 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) ∈ ℂ)
39	37, 38, 35	pnncand 11038	. . . . . . 7 ⊢ (𝜑 → (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) = (((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵))) + (4 · (𝐴 · 𝐶))))
40	4, 5	sqmuld 13525	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋)↑2) = (((2 · 𝐴)↑2) · (𝑋↑2)))
41		sq2 13563	. . . . . . . . . . . . 13 ⊢ (2↑2) = 4
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (2↑2) = 4)
43	2	sqvald 13510	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
44	42, 43	oveq12d 7176	. . . . . . . . . . 11 ⊢ (𝜑 → ((2↑2) · (𝐴↑2)) = (4 · (𝐴 · 𝐴)))
45		sqmul 13488	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
46	1, 2, 45	sylancr 589	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((2↑2) · (𝐴↑2)))
47	23, 2, 2	mulassd 10666	. . . . . . . . . . 11 ⊢ (𝜑 → ((4 · 𝐴) · 𝐴) = (4 · (𝐴 · 𝐴)))
48	44, 46, 47	3eqtr4d 2868	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐴)↑2) = ((4 · 𝐴) · 𝐴))
49	48	oveq1d 7173	. . . . . . . . 9 ⊢ (𝜑 → (((2 · 𝐴)↑2) · (𝑋↑2)) = (((4 · 𝐴) · 𝐴) · (𝑋↑2)))
50	22, 2, 13	mulassd 10666	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · 𝐴) · (𝑋↑2)) = ((4 · 𝐴) · (𝐴 · (𝑋↑2))))
51	40, 49, 50	3eqtrrd 2863	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · (𝐴 · (𝑋↑2))) = (((2 · 𝐴) · 𝑋)↑2))
52	22, 15, 16	adddid 10667	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)))
53		2t2e4 11804	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 2) = 4
54	53	oveq1i 7168	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 2) · 𝐴) = (4 · 𝐴)
55	1	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
56	55, 55, 2	mulassd 10666	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 2) · 𝐴) = (2 · (2 · 𝐴)))
57	54, 56	syl5eqr 2872	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (4 · 𝐴) = (2 · (2 · 𝐴)))
58	57	oveq1d 7173	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = ((2 · (2 · 𝐴)) · 𝐵))
59	55, 4, 7	mulassd 10666	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (2 · 𝐴)) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
60	58, 59	eqtrd 2858	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((4 · 𝐴) · 𝐵) = (2 · ((2 · 𝐴) · 𝐵)))
61	60	oveq1d 7173	. . . . . . . . . . . 12 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋))
62	4, 7	mulcld 10663	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐴) · 𝐵) ∈ ℂ)
63	55, 62, 5	mulassd 10666	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · ((2 · 𝐴) · 𝐵)) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
64	61, 63	eqtrd 2858	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = (2 · (((2 · 𝐴) · 𝐵) · 𝑋)))
65	22, 7, 5	mulassd 10666	. . . . . . . . . . 11 ⊢ (𝜑 → (((4 · 𝐴) · 𝐵) · 𝑋) = ((4 · 𝐴) · (𝐵 · 𝑋)))
66	4, 7, 5	mul32d 10852	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐴) · 𝐵) · 𝑋) = (((2 · 𝐴) · 𝑋) · 𝐵))
67	66	oveq2d 7174	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (((2 · 𝐴) · 𝐵) · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
68	64, 65, 67	3eqtr3d 2866	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · (𝐵 · 𝑋)) = (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))
69	23, 2, 16	mulassd 10666	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · 𝐴) · 𝐶) = (4 · (𝐴 · 𝐶)))
70	68, 69	oveq12d 7176	. . . . . . . . 9 ⊢ (𝜑 → (((4 · 𝐴) · (𝐵 · 𝑋)) + ((4 · 𝐴) · 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
71	52, 70	eqtrd 2858	. . . . . . . 8 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶)) = ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶))))
72	51, 71	oveq12d 7176	. . . . . . 7 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = ((((2 · 𝐴) · 𝑋)↑2) + ((2 · (((2 · 𝐴) · 𝑋) · 𝐵)) + (4 · (𝐴 · 𝐶)))))
73	36, 39, 72	3eqtr4rd 2869	. . . . . 6 ⊢ (𝜑 → (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
74	22, 14, 17	adddid 10667	. . . . . 6 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((4 · 𝐴) · (𝐴 · (𝑋↑2))) + ((4 · 𝐴) · ((𝐵 · 𝑋) + 𝐶))))
75		binom2 13582	. . . . . . . . 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 10856	. . . . . . 7 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = ((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))))
78		quad2.2	. . . . . . 7 ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))
79	77, 78	oveq12d 7176	. . . . . 6 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)) = (((𝐵↑2) + ((((2 · 𝐴) · 𝑋)↑2) + (2 · (((2 · 𝐴) · 𝑋) · 𝐵)))) − ((𝐵↑2) − (4 · (𝐴 · 𝐶)))))
80	73, 74, 79	3eqtr4d 2868	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶))) = (((((2 · 𝐴) · 𝑋) + 𝐵)↑2) − (𝐷↑2)))
81	22	mul01d 10841	. . . . 5 ⊢ (𝜑 → ((4 · 𝐴) · 0) = 0)
82	80, 81	eqeq12d 2839	. . . 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 11006	. . . . 5 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) = (((2 · 𝐴) · 𝑋) + 𝐵))
85	84	oveq1d 7173	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = ((((2 · 𝐴) · 𝑋) + 𝐵)↑2))
86	85	eqeq1d 2825	. . 3 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) + 𝐵)↑2) = (𝐷↑2)))
87	12, 83, 86	3bitr4d 313	. 2 ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ ((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2)))
88	7	negcld 10986	. . . 4 ⊢ (𝜑 → -𝐵 ∈ ℂ)
89	6, 88	subcld 10999	. . 3 ⊢ (𝜑 → (((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ)
90		sqeqor 13581	. . 3 ⊢ (((((2 · 𝐴) · 𝑋) − -𝐵) ∈ ℂ ∧ 𝐷 ∈ ℂ) → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
91	89, 10, 90	syl2anc 586	. 2 ⊢ (𝜑 → (((((2 · 𝐴) · 𝑋) − -𝐵)↑2) = (𝐷↑2) ↔ ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ∨ (((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷)))
92	6, 88, 10	subaddd 11017	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
93	88, 10	addcld 10662	. . . . . 6 ⊢ (𝜑 → (-𝐵 + 𝐷) ∈ ℂ)
94		2ne0 11744	. . . . . . . 8 ⊢ 2 ≠ 0
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ≠ 0)
96	55, 2, 95, 26	mulne0d 11294	. . . . . 6 ⊢ (𝜑 → (2 · 𝐴) ≠ 0)
97	93, 4, 5, 96	divmuld 11440	. . . . 5 ⊢ (𝜑 → (((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷)))
98		eqcom 2830	. . . . 5 ⊢ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 + 𝐷) / (2 · 𝐴)) = 𝑋)
99		eqcom 2830	. . . . 5 ⊢ ((-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋) ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 + 𝐷))
100	97, 98, 99	3bitr4g 316	. . . 4 ⊢ (𝜑 → (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ↔ (-𝐵 + 𝐷) = ((2 · 𝐴) · 𝑋)))
101	92, 100	bitr4d 284	. . 3 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = 𝐷 ↔ 𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴))))
102	88, 10	negsubd 11005	. . . . 5 ⊢ (𝜑 → (-𝐵 + -𝐷) = (-𝐵 − 𝐷))
103	102	eqeq1d 2825	. . . 4 ⊢ (𝜑 → ((-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋) ↔ (-𝐵 − 𝐷) = ((2 · 𝐴) · 𝑋)))
104	10	negcld 10986	. . . . 5 ⊢ (𝜑 → -𝐷 ∈ ℂ)
105	6, 88, 104	subaddd 11017	. . . 4 ⊢ (𝜑 → ((((2 · 𝐴) · 𝑋) − -𝐵) = -𝐷 ↔ (-𝐵 + -𝐷) = ((2 · 𝐴) · 𝑋)))
106	88, 10	subcld 10999	. . . . . 6 ⊢ (𝜑 → (-𝐵 − 𝐷) ∈ ℂ)
107	106, 4, 5, 96	divmuld 11440	. . . . 5 ⊢ (𝜑 → (((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋 ↔ ((2 · 𝐴) · 𝑋) = (-𝐵 − 𝐷)))
108		eqcom 2830	. . . . 5 ⊢ (𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)) ↔ ((-𝐵 − 𝐷) / (2 · 𝐴)) = 𝑋)
109		eqcom 2830	. . . . 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 1537 ∈ wcel 2114 ≠ wne 3018 (class class class)co 7158 ℂcc 10537 0cc0 10539 + caddc 10542 · cmul 10544 − cmin 10872 -cneg 10873 / cdiv 11299 2c2 11695 4c4 11697 ↑cexp 13432

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-n0 11901 df-z 11985 df-uz 12247 df-seq 13373 df-exp 13433

This theorem is referenced by: quad 25420 dcubic2 25424 dquartlem1 25431

W3C validator