quad3d

Description: Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019) Deduction version. (Revised by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	quad3d.1	$⊢ φ \to X \in ℂ$
	quad3d.2	$⊢ φ \to A \in ℂ$
	quad3d.3	$⊢ φ \to A \neq 0$
	quad3d.4	$⊢ φ \to B \in ℂ$
	quad3d.5	$⊢ φ \to C \in ℂ$
	quad3d.6	$⊢ φ \to A X^{2} + B X + C = 0$
Assertion	quad3d	$⊢ φ \to (X = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A} \lor X = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A})$

Proof

Step	Hyp	Ref	Expression
1		quad3d.1	$⊢ φ \to X \in ℂ$
2		quad3d.2	$⊢ φ \to A \in ℂ$
3		quad3d.3	$⊢ φ \to A \neq 0$
4		quad3d.4	$⊢ φ \to B \in ℂ$
5		quad3d.5	$⊢ φ \to C \in ℂ$
6		quad3d.6	$⊢ φ \to A X^{2} + B X + C = 0$
7		2cnd	$⊢ φ \to 2 \in ℂ$
8	7 2	mulcld	$⊢ φ \to 2 A \in ℂ$
9		2ne0	$⊢ 2 \neq 0$
10	9	a1i	$⊢ φ \to 2 \neq 0$
11	7 2 10 3	mulne0d	$⊢ φ \to 2 A \neq 0$
12	4 8 11	divcld	$⊢ φ \to \frac{B}{2 A} \in ℂ$
13	1 12	addcld	$⊢ φ \to X + (\frac{B}{2 A}) \in ℂ$
14	8 13	sqmuld	$⊢ φ \to {2 A (X + (\frac{B}{2 A}))}^{2} = {2 A}^{2} {(X + (\frac{B}{2 A}))}^{2}$
15	1 12	binom2d	$⊢ φ \to {(X + (\frac{B}{2 A}))}^{2} = X^{2} + 2 X (\frac{B}{2 A}) + {(\frac{B}{2 A})}^{2}$
16	1	sqcld	$⊢ φ \to X^{2} \in ℂ$
17	2 16	mulcld	$⊢ φ \to A X^{2} \in ℂ$
18	4 1	mulcld	$⊢ φ \to B X \in ℂ$
19	17 18 2 3	divdird	$⊢ φ \to \frac{A X^{2} + B X}{A} = (\frac{A X^{2}}{A}) + (\frac{B X}{A})$
20	16 2 3	divcan3d	$⊢ φ \to \frac{A X^{2}}{A} = X^{2}$
21	4 1 2 3	div23d	$⊢ φ \to \frac{B X}{A} = (\frac{B}{A}) X$
22	20 21	oveq12d	$⊢ φ \to (\frac{A X^{2}}{A}) + (\frac{B X}{A}) = X^{2} + (\frac{B}{A}) X$
23	19 22	eqtr2d	$⊢ φ \to X^{2} + (\frac{B}{A}) X = \frac{A X^{2} + B X}{A}$
24	4 2 3	divcld	$⊢ φ \to \frac{B}{A} \in ℂ$
25	24 1	mulcomd	$⊢ φ \to (\frac{B}{A}) X = X (\frac{B}{A})$
26	1 24	mulcld	$⊢ φ \to X (\frac{B}{A}) \in ℂ$
27	26 7 10	divcan2d	$⊢ φ \to 2 (\frac{X (\frac{B}{A})}{2}) = X (\frac{B}{A})$
28	1 24 7 10	divassd	$⊢ φ \to \frac{X (\frac{B}{A})}{2} = X (\frac{\frac{B}{A}}{2})$
29	4 2 7 3 10	divdiv1d	$⊢ φ \to \frac{\frac{B}{A}}{2} = \frac{B}{A \cdot 2}$
30	2 7	mulcomd	$⊢ φ \to A \cdot 2 = 2 A$
31	30	oveq2d	$⊢ φ \to \frac{B}{A \cdot 2} = \frac{B}{2 A}$
32	29 31	eqtrd	$⊢ φ \to \frac{\frac{B}{A}}{2} = \frac{B}{2 A}$
33	32	oveq2d	$⊢ φ \to X (\frac{\frac{B}{A}}{2}) = X (\frac{B}{2 A})$
34	28 33	eqtrd	$⊢ φ \to \frac{X (\frac{B}{A})}{2} = X (\frac{B}{2 A})$
35	34	oveq2d	$⊢ φ \to 2 (\frac{X (\frac{B}{A})}{2}) = 2 X (\frac{B}{2 A})$
36	25 27 35	3eqtr2d	$⊢ φ \to (\frac{B}{A}) X = 2 X (\frac{B}{2 A})$
37	36	oveq2d	$⊢ φ \to X^{2} + (\frac{B}{A}) X = X^{2} + 2 X (\frac{B}{2 A})$
38	17 18	addcld	$⊢ φ \to A X^{2} + B X \in ℂ$
39	17 18 5	addassd	$⊢ φ \to A X^{2} + B X + C = A X^{2} + B X + C$
40	38 5 39	mvlraddd	$⊢ φ \to A X^{2} + B X = A X^{2} + (B X + C) - C$
41	6	oveq1d	$⊢ φ \to A X^{2} + (B X + C) - C = 0 - C$
42		df-neg	$⊢ - C = 0 - C$
43	41 42	eqtr4di	$⊢ φ \to A X^{2} + (B X + C) - C = - C$
44	40 43	eqtrd	$⊢ φ \to A X^{2} + B X = - C$
45	44	oveq1d	$⊢ φ \to \frac{A X^{2} + B X}{A} = \frac{- C}{A}$
46	23 37 45	3eqtr3d	$⊢ φ \to X^{2} + 2 X (\frac{B}{2 A}) = \frac{- C}{A}$
47	46	oveq1d	$⊢ φ \to X^{2} + 2 X (\frac{B}{2 A}) + {(\frac{B}{2 A})}^{2} = (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2}$
48	15 47	eqtrd	$⊢ φ \to {(X + (\frac{B}{2 A}))}^{2} = (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2}$
49	5	negcld	$⊢ φ \to - C \in ℂ$
50	49 2 3	divcld	$⊢ φ \to \frac{- C}{A} \in ℂ$
51	12	sqcld	$⊢ φ \to {(\frac{B}{2 A})}^{2} \in ℂ$
52	50 51	addcomd	$⊢ φ \to (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2} = {(\frac{B}{2 A})}^{2} + (\frac{- C}{A})$
53	4 8 11	sqdivd	$⊢ φ \to {(\frac{B}{2 A})}^{2} = \frac{B^{2}}{{2 A}^{2}}$
54		4cn	$⊢ 4 \in ℂ$
55	54	a1i	$⊢ φ \to 4 \in ℂ$
56	55 2	mulcld	$⊢ φ \to 4 A \in ℂ$
57		4ne0	$⊢ 4 \neq 0$
58	57	a1i	$⊢ φ \to 4 \neq 0$
59	55 2 58 3	mulne0d	$⊢ φ \to 4 A \neq 0$
60	56 56 49 2 59 3	divmuldivd	$⊢ φ \to (\frac{4 A}{4 A}) (\frac{- C}{A}) = \frac{4 A (- C)}{4 A A}$
61	56 59	dividd	$⊢ φ \to \frac{4 A}{4 A} = 1$
62	61	eqcomd	$⊢ φ \to 1 = \frac{4 A}{4 A}$
63	62	oveq1d	$⊢ φ \to 1 (\frac{- C}{A}) = (\frac{4 A}{4 A}) (\frac{- C}{A})$
64	50	mullidd	$⊢ φ \to 1 (\frac{- C}{A}) = \frac{- C}{A}$
65	63 64	eqtr3d	$⊢ φ \to (\frac{4 A}{4 A}) (\frac{- C}{A}) = \frac{- C}{A}$
66	5	mulm1d	$⊢ φ \to -1 C = - C$
67	66	eqcomd	$⊢ φ \to - C = -1 C$
68	67	oveq2d	$⊢ φ \to 4 A (- C) = 4 A -1 C$
69		neg1cn	$⊢ - 1 \in ℂ$
70	69	a1i	$⊢ φ \to - 1 \in ℂ$
71	56 70 5	mulassd	$⊢ φ \to 4 A -1 C = 4 A -1 C$
72	68 71	eqtr4d	$⊢ φ \to 4 A (- C) = 4 A -1 C$
73	56 70	mulcomd	$⊢ φ \to 4 A -1 = -1 4 A$
74	73	oveq1d	$⊢ φ \to 4 A -1 C = -1 4 A C$
75	70 56 5	mulassd	$⊢ φ \to -1 4 A C = -1 4 A C$
76	72 74 75	3eqtrd	$⊢ φ \to 4 A (- C) = -1 4 A C$
77	55 2 5	mulassd	$⊢ φ \to 4 A C = 4 A C$
78	77	oveq2d	$⊢ φ \to -1 4 A C = -1 4 A C$
79	2 5	mulcld	$⊢ φ \to A C \in ℂ$
80	55 79	mulcld	$⊢ φ \to 4 A C \in ℂ$
81	80	mulm1d	$⊢ φ \to -1 4 A C = - 4 A C$
82	76 78 81	3eqtrd	$⊢ φ \to 4 A (- C) = - 4 A C$
83		2t2e4	$⊢ 2 \cdot 2 = 4$
84	83	a1i	$⊢ φ \to 2 \cdot 2 = 4$
85	84	eqcomd	$⊢ φ \to 4 = 2 \cdot 2$
86	85	oveq1d	$⊢ φ \to 4 A = 2 \cdot 2 A$
87	86	oveq1d	$⊢ φ \to 4 A A = 2 \cdot 2 A A$
88	7 7 2	mulassd	$⊢ φ \to 2 \cdot 2 A = 2 2 A$
89	88	oveq1d	$⊢ φ \to 2 \cdot 2 A A = 2 2 A A$
90	87 89	eqtrd	$⊢ φ \to 4 A A = 2 2 A A$
91	7 8	mulcomd	$⊢ φ \to 2 2 A = 2 A \cdot 2$
92	91	oveq1d	$⊢ φ \to 2 2 A A = 2 A \cdot 2 A$
93	8 7 2	mulassd	$⊢ φ \to 2 A \cdot 2 A = 2 A 2 A$
94	90 92 93	3eqtrd	$⊢ φ \to 4 A A = 2 A 2 A$
95	8	sqvald	$⊢ φ \to {2 A}^{2} = 2 A 2 A$
96	94 95	eqtr4d	$⊢ φ \to 4 A A = {2 A}^{2}$
97	82 96	oveq12d	$⊢ φ \to \frac{4 A (- C)}{4 A A} = \frac{- 4 A C}{{2 A}^{2}}$
98	60 65 97	3eqtr3d	$⊢ φ \to \frac{- C}{A} = \frac{- 4 A C}{{2 A}^{2}}$
99	53 98	oveq12d	$⊢ φ \to {(\frac{B}{2 A})}^{2} + (\frac{- C}{A}) = (\frac{B^{2}}{{2 A}^{2}}) + (\frac{- 4 A C}{{2 A}^{2}})$
100	4	sqcld	$⊢ φ \to B^{2} \in ℂ$
101	80	negcld	$⊢ φ \to - 4 A C \in ℂ$
102	8	sqcld	$⊢ φ \to {2 A}^{2} \in ℂ$
103	8 8 11 11	mulne0d	$⊢ φ \to 2 A 2 A \neq 0$
104	95 103	eqnetrd	$⊢ φ \to {2 A}^{2} \neq 0$
105	100 101 102 104	divdird	$⊢ φ \to \frac{B^{2} + (- 4 A C)}{{2 A}^{2}} = (\frac{B^{2}}{{2 A}^{2}}) + (\frac{- 4 A C}{{2 A}^{2}})$
106	100 80	negsubd	$⊢ φ \to B^{2} + (- 4 A C) = B^{2} - 4 A C$
107	106	oveq1d	$⊢ φ \to \frac{B^{2} + (- 4 A C)}{{2 A}^{2}} = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
108	99 105 107	3eqtr2d	$⊢ φ \to {(\frac{B}{2 A})}^{2} + (\frac{- C}{A}) = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
109	48 52 108	3eqtrd	$⊢ φ \to {(X + (\frac{B}{2 A}))}^{2} = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
110	109	oveq2d	$⊢ φ \to {2 A}^{2} {(X + (\frac{B}{2 A}))}^{2} = {2 A}^{2} (\frac{B^{2} - 4 A C}{{2 A}^{2}})$
111	100 80	subcld	$⊢ φ \to B^{2} - 4 A C \in ℂ$
112	111 102 104	divcan2d	$⊢ φ \to {2 A}^{2} (\frac{B^{2} - 4 A C}{{2 A}^{2}}) = B^{2} - 4 A C$
113	14 110 112	3eqtrd	$⊢ φ \to {2 A (X + (\frac{B}{2 A}))}^{2} = B^{2} - 4 A C$
114	8 13	mulcld	$⊢ φ \to 2 A (X + (\frac{B}{2 A})) \in ℂ$
115		eqsqrtor	$⊢ (2 A (X + (\frac{B}{2 A})) \in ℂ \land B^{2} - 4 A C \in ℂ) \to ({2 A (X + (\frac{B}{2 A}))}^{2} = B^{2} - 4 A C \leftrightarrow (2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \lor 2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C}))$
116	114 111 115	syl2anc	$⊢ φ \to ({2 A (X + (\frac{B}{2 A}))}^{2} = B^{2} - 4 A C \leftrightarrow (2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \lor 2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C}))$
117	113 116	mpbid	$⊢ φ \to (2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \lor 2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C})$
118	111	sqrtcld	$⊢ φ \to \sqrt{B^{2} - 4 A C} \in ℂ$
119	8 13 118 11	rdiv	$⊢ φ \to (2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \leftrightarrow X + (\frac{B}{2 A}) = \frac{\sqrt{B^{2} - 4 A C}}{2 A})$
120	118 8 11	divcld	$⊢ φ \to \frac{\sqrt{B^{2} - 4 A C}}{2 A} \in ℂ$
121	1 12 120	addlsub	$⊢ φ \to (X + (\frac{B}{2 A}) = \frac{\sqrt{B^{2} - 4 A C}}{2 A} \leftrightarrow X = (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}))$
122	4 8 11	divnegd	$⊢ φ \to - \frac{B}{2 A} = \frac{- B}{2 A}$
123	122	oveq2d	$⊢ φ \to (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) + (- \frac{B}{2 A}) = (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) + (\frac{- B}{2 A})$
124	120 12	negsubd	$⊢ φ \to (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) + (- \frac{B}{2 A}) = (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A})$
125	4	negcld	$⊢ φ \to - B \in ℂ$
126	125 8 11	divcld	$⊢ φ \to \frac{- B}{2 A} \in ℂ$
127	120 126	addcomd	$⊢ φ \to (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) + (\frac{- B}{2 A}) = (\frac{- B}{2 A}) + (\frac{\sqrt{B^{2} - 4 A C}}{2 A})$
128	123 124 127	3eqtr3d	$⊢ φ \to (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = (\frac{- B}{2 A}) + (\frac{\sqrt{B^{2} - 4 A C}}{2 A})$
129	125 118 8 11	divdird	$⊢ φ \to \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A} = (\frac{- B}{2 A}) + (\frac{\sqrt{B^{2} - 4 A C}}{2 A})$
130	128 129	eqtr4d	$⊢ φ \to (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A}$
131	130	eqeq2d	$⊢ φ \to (X = (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) \leftrightarrow X = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A})$
132	119 121 131	3bitrd	$⊢ φ \to (2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \leftrightarrow X = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A})$
133	118	negcld	$⊢ φ \to - \sqrt{B^{2} - 4 A C} \in ℂ$
134	8 13 133 11	rdiv	$⊢ φ \to (2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C} \leftrightarrow X + (\frac{B}{2 A}) = \frac{- \sqrt{B^{2} - 4 A C}}{2 A})$
135	133 8 11	divcld	$⊢ φ \to \frac{- \sqrt{B^{2} - 4 A C}}{2 A} \in ℂ$
136	1 12 135	addlsub	$⊢ φ \to (X + (\frac{B}{2 A}) = \frac{- \sqrt{B^{2} - 4 A C}}{2 A} \leftrightarrow X = (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}))$
137	122	oveq2d	$⊢ φ \to (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) + (- \frac{B}{2 A}) = (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) + (\frac{- B}{2 A})$
138	135 12	negsubd	$⊢ φ \to (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) + (- \frac{B}{2 A}) = (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A})$
139	135 126	addcomd	$⊢ φ \to (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) + (\frac{- B}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{B^{2} - 4 A C}}{2 A})$
140	137 138 139	3eqtr3d	$⊢ φ \to (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = (\frac{- B}{2 A}) + (\frac{- \sqrt{B^{2} - 4 A C}}{2 A})$
141	125 133 8 11	divdird	$⊢ φ \to \frac{- B + (- \sqrt{B^{2} - 4 A C})}{2 A} = (\frac{- B}{2 A}) + (\frac{- \sqrt{B^{2} - 4 A C}}{2 A})$
142	125 118	negsubd	$⊢ φ \to - B + (- \sqrt{B^{2} - 4 A C}) = - B - \sqrt{B^{2} - 4 A C}$
143	142	oveq1d	$⊢ φ \to \frac{- B + (- \sqrt{B^{2} - 4 A C})}{2 A} = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A}$
144	140 141 143	3eqtr2d	$⊢ φ \to (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A}$
145	144	eqeq2d	$⊢ φ \to (X = (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) \leftrightarrow X = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A})$
146	134 136 145	3bitrd	$⊢ φ \to (2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C} \leftrightarrow X = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A})$
147	132 146	orbi12d	$⊢ φ \to ((2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C} \lor 2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C}) \leftrightarrow (X = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A} \lor X = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A}))$
148	117 147	mpbid	$⊢ φ \to (X = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A} \lor X = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A})$

Metamath Proof Explorer

Theorem quad3d

Proof