quad3

Description: Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019)

	Ref	Expression
Hypotheses	quad3.1	$⊢ X \in ℂ$
	quad3.2	$⊢ A \in ℂ$
	quad3.3	$⊢ A \neq 0$
	quad3.4	$⊢ B \in ℂ$
	quad3.5	$⊢ C \in ℂ$
	quad3.6	$⊢ A X^{2} + B X + C = 0$
Assertion	quad3	$⊢ (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		quad3.1	$⊢ X \in ℂ$
2		quad3.2	$⊢ A \in ℂ$
3		quad3.3	$⊢ A \neq 0$
4		quad3.4	$⊢ B \in ℂ$
5		quad3.5	$⊢ C \in ℂ$
6		quad3.6	$⊢ A X^{2} + B X + C = 0$
7		2cn	$⊢ 2 \in ℂ$
8	7 2	mulcli	$⊢ 2 A \in ℂ$
9		2ne0	$⊢ 2 \neq 0$
10	7 2 9 3	mulne0i	$⊢ 2 A \neq 0$
11	4 8 10	divcli	$⊢ \frac{B}{2 A} \in ℂ$
12	1 11	addcli	$⊢ X + (\frac{B}{2 A}) \in ℂ$
13	8 12	sqmuli	$⊢ {2 A (X + (\frac{B}{2 A}))}^{2} = {2 A}^{2} {(X + (\frac{B}{2 A}))}^{2}$
14	1 11	binom2i	$⊢ {(X + (\frac{B}{2 A}))}^{2} = X^{2} + 2 X (\frac{B}{2 A}) + {(\frac{B}{2 A})}^{2}$
15	1	sqcli	$⊢ X^{2} \in ℂ$
16	2 15	mulcli	$⊢ A X^{2} \in ℂ$
17	4 1	mulcli	$⊢ B X \in ℂ$
18	16 17 2 3	divdiri	$⊢ \frac{A X^{2} + B X}{A} = (\frac{A X^{2}}{A}) + (\frac{B X}{A})$
19	15 2 3	divcan3i	$⊢ \frac{A X^{2}}{A} = X^{2}$
20	4 1 2 3	div23i	$⊢ \frac{B X}{A} = (\frac{B}{A}) X$
21	19 20	oveq12i	$⊢ (\frac{A X^{2}}{A}) + (\frac{B X}{A}) = X^{2} + (\frac{B}{A}) X$
22	18 21	eqtr2i	$⊢ X^{2} + (\frac{B}{A}) X = \frac{A X^{2} + B X}{A}$
23	4 2 3	divcli	$⊢ \frac{B}{A} \in ℂ$
24	23 1	mulcomi	$⊢ (\frac{B}{A}) X = X (\frac{B}{A})$
25	1 23	mulcli	$⊢ X (\frac{B}{A}) \in ℂ$
26	25 7 9	divcan2i	$⊢ 2 (\frac{X (\frac{B}{A})}{2}) = X (\frac{B}{A})$
27	1 23 7 9	divassi	$⊢ \frac{X (\frac{B}{A})}{2} = X (\frac{\frac{B}{A}}{2})$
28	2 3	pm3.2i	$⊢ (A \in ℂ \land A \neq 0)$
29	7 9	pm3.2i	$⊢ (2 \in ℂ \land 2 \neq 0)$
30		divdiv1	$⊢ (B \in ℂ \land (A \in ℂ \land A \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{B}{A}}{2} = \frac{B}{A \cdot 2}$
31	4 28 29 30	mp3an	$⊢ \frac{\frac{B}{A}}{2} = \frac{B}{A \cdot 2}$
32	2 7	mulcomi	$⊢ A \cdot 2 = 2 A$
33	32	oveq2i	$⊢ \frac{B}{A \cdot 2} = \frac{B}{2 A}$
34	31 33	eqtri	$⊢ \frac{\frac{B}{A}}{2} = \frac{B}{2 A}$
35	34	oveq2i	$⊢ X (\frac{\frac{B}{A}}{2}) = X (\frac{B}{2 A})$
36	27 35	eqtri	$⊢ \frac{X (\frac{B}{A})}{2} = X (\frac{B}{2 A})$
37	36	oveq2i	$⊢ 2 (\frac{X (\frac{B}{A})}{2}) = 2 X (\frac{B}{2 A})$
38	24 26 37	3eqtr2i	$⊢ (\frac{B}{A}) X = 2 X (\frac{B}{2 A})$
39	38	oveq2i	$⊢ X^{2} + (\frac{B}{A}) X = X^{2} + 2 X (\frac{B}{2 A})$
40	16 17 5	addassi	$⊢ A X^{2} + B X + C = A X^{2} + B X + C$
41	40	eqcomi	$⊢ A X^{2} + B X + C = A X^{2} + B X + C$
42	41	oveq1i	$⊢ A X^{2} + (B X + C) - C = (A X^{2} + B X) + C - C$
43	16 17	addcli	$⊢ A X^{2} + B X \in ℂ$
44	43 5	pncan3oi	$⊢ (A X^{2} + B X) + C - C = A X^{2} + B X$
45	42 44	eqtr2i	$⊢ A X^{2} + B X = A X^{2} + (B X + C) - C$
46	6	oveq1i	$⊢ A X^{2} + (B X + C) - C = 0 - C$
47		df-neg	$⊢ - C = 0 - C$
48	46 47	eqtr4i	$⊢ A X^{2} + (B X + C) - C = - C$
49	45 48	eqtri	$⊢ A X^{2} + B X = - C$
50	49	oveq1i	$⊢ \frac{A X^{2} + B X}{A} = \frac{- C}{A}$
51	22 39 50	3eqtr3i	$⊢ X^{2} + 2 X (\frac{B}{2 A}) = \frac{- C}{A}$
52	51	oveq1i	$⊢ X^{2} + 2 X (\frac{B}{2 A}) + {(\frac{B}{2 A})}^{2} = (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2}$
53	14 52	eqtri	$⊢ {(X + (\frac{B}{2 A}))}^{2} = (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2}$
54	5	negcli	$⊢ - C \in ℂ$
55	54 2 3	divcli	$⊢ \frac{- C}{A} \in ℂ$
56	11	sqcli	$⊢ {(\frac{B}{2 A})}^{2} \in ℂ$
57	55 56	addcomi	$⊢ (\frac{- C}{A}) + {(\frac{B}{2 A})}^{2} = {(\frac{B}{2 A})}^{2} + (\frac{- C}{A})$
58	4 8 10	sqdivi	$⊢ {(\frac{B}{2 A})}^{2} = \frac{B^{2}}{{2 A}^{2}}$
59		4cn	$⊢ 4 \in ℂ$
60	59 2	mulcli	$⊢ 4 A \in ℂ$
61		4ne0	$⊢ 4 \neq 0$
62	59 2 61 3	mulne0i	$⊢ 4 A \neq 0$
63	60 60 54 2 62 3	divmuldivi	$⊢ (\frac{4 A}{4 A}) (\frac{- C}{A}) = \frac{4 A (- C)}{4 A A}$
64	60 62	dividi	$⊢ \frac{4 A}{4 A} = 1$
65	64	eqcomi	$⊢ 1 = \frac{4 A}{4 A}$
66	65	oveq1i	$⊢ 1 (\frac{- C}{A}) = (\frac{4 A}{4 A}) (\frac{- C}{A})$
67	55	mulid2i	$⊢ 1 (\frac{- C}{A}) = \frac{- C}{A}$
68	66 67	eqtr3i	$⊢ (\frac{4 A}{4 A}) (\frac{- C}{A}) = \frac{- C}{A}$
69	5	mulm1i	$⊢ -1 C = - C$
70	69	eqcomi	$⊢ - C = -1 C$
71	70	oveq2i	$⊢ 4 A (- C) = 4 A -1 C$
72		neg1cn	$⊢ - 1 \in ℂ$
73	60 72 5	mulassi	$⊢ 4 A -1 C = 4 A -1 C$
74	71 73	eqtr4i	$⊢ 4 A (- C) = 4 A -1 C$
75	60 72	mulcomi	$⊢ 4 A -1 = -1 4 A$
76	75	oveq1i	$⊢ 4 A -1 C = -1 4 A C$
77	72 60 5	mulassi	$⊢ -1 4 A C = -1 4 A C$
78	74 76 77	3eqtri	$⊢ 4 A (- C) = -1 4 A C$
79	59 2 5	mulassi	$⊢ 4 A C = 4 A C$
80	79	oveq2i	$⊢ -1 4 A C = -1 4 A C$
81	2 5	mulcli	$⊢ A C \in ℂ$
82	59 81	mulcli	$⊢ 4 A C \in ℂ$
83	82	mulm1i	$⊢ -1 4 A C = - 4 A C$
84	78 80 83	3eqtri	$⊢ 4 A (- C) = - 4 A C$
85		2t2e4	$⊢ 2 \cdot 2 = 4$
86	85	eqcomi	$⊢ 4 = 2 \cdot 2$
87	86	oveq1i	$⊢ 4 A = 2 \cdot 2 A$
88	87	oveq1i	$⊢ 4 A A = 2 \cdot 2 A A$
89	7 7 2	mulassi	$⊢ 2 \cdot 2 A = 2 2 A$
90	89	oveq1i	$⊢ 2 \cdot 2 A A = 2 2 A A$
91	88 90	eqtri	$⊢ 4 A A = 2 2 A A$
92	7 8	mulcomi	$⊢ 2 2 A = 2 A \cdot 2$
93	92	oveq1i	$⊢ 2 2 A A = 2 A \cdot 2 A$
94	8 7 2	mulassi	$⊢ 2 A \cdot 2 A = 2 A 2 A$
95	91 93 94	3eqtri	$⊢ 4 A A = 2 A 2 A$
96	8	sqvali	$⊢ {2 A}^{2} = 2 A 2 A$
97	95 96	eqtr4i	$⊢ 4 A A = {2 A}^{2}$
98	84 97	oveq12i	$⊢ \frac{4 A (- C)}{4 A A} = \frac{- 4 A C}{{2 A}^{2}}$
99	63 68 98	3eqtr3i	$⊢ \frac{- C}{A} = \frac{- 4 A C}{{2 A}^{2}}$
100	58 99	oveq12i	$⊢ {(\frac{B}{2 A})}^{2} + (\frac{- C}{A}) = (\frac{B^{2}}{{2 A}^{2}}) + (\frac{- 4 A C}{{2 A}^{2}})$
101	4	sqcli	$⊢ B^{2} \in ℂ$
102	82	negcli	$⊢ - 4 A C \in ℂ$
103	8	sqcli	$⊢ {2 A}^{2} \in ℂ$
104	8 8 10 10	mulne0i	$⊢ 2 A 2 A \neq 0$
105	96 104	eqnetri	$⊢ {2 A}^{2} \neq 0$
106	101 102 103 105	divdiri	$⊢ \frac{B^{2} + (- 4 A C)}{{2 A}^{2}} = (\frac{B^{2}}{{2 A}^{2}}) + (\frac{- 4 A C}{{2 A}^{2}})$
107	101 82	negsubi	$⊢ B^{2} + (- 4 A C) = B^{2} - 4 A C$
108	107	oveq1i	$⊢ \frac{B^{2} + (- 4 A C)}{{2 A}^{2}} = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
109	100 106 108	3eqtr2i	$⊢ {(\frac{B}{2 A})}^{2} + (\frac{- C}{A}) = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
110	53 57 109	3eqtri	$⊢ {(X + (\frac{B}{2 A}))}^{2} = \frac{B^{2} - 4 A C}{{2 A}^{2}}$
111	110	oveq2i	$⊢ {2 A}^{2} {(X + (\frac{B}{2 A}))}^{2} = {2 A}^{2} (\frac{B^{2} - 4 A C}{{2 A}^{2}})$
112	101 82	subcli	$⊢ B^{2} - 4 A C \in ℂ$
113	112 103 105	divcan2i	$⊢ {2 A}^{2} (\frac{B^{2} - 4 A C}{{2 A}^{2}}) = B^{2} - 4 A C$
114	13 111 113	3eqtri	$⊢ {2 A (X + (\frac{B}{2 A}))}^{2} = B^{2} - 4 A C$
115	8 12	mulcli	$⊢ 2 A (X + (\frac{B}{2 A})) \in ℂ$
116	115 112	pm3.2i	$⊢ (2 A (X + (\frac{B}{2 A})) \in ℂ \land B^{2} - 4 A C \in ℂ)$
117		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}))$
118	116 117	ax-mp	$⊢ {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})$
119	114 118	mpbi	$⊢ (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})$
120		sqrtcl	$⊢ B^{2} - 4 A C \in ℂ \to \sqrt{B^{2} - 4 A C} \in ℂ$
121	112 120	ax-mp	$⊢ \sqrt{B^{2} - 4 A C} \in ℂ$
122	121 8 12 10	divmuli	$⊢ \frac{\sqrt{B^{2} - 4 A C}}{2 A} = X + (\frac{B}{2 A}) \leftrightarrow 2 A (X + (\frac{B}{2 A})) = \sqrt{B^{2} - 4 A C}$
123		eqcom	$⊢ \frac{\sqrt{B^{2} - 4 A C}}{2 A} = X + (\frac{B}{2 A}) \leftrightarrow X + (\frac{B}{2 A}) = \frac{\sqrt{B^{2} - 4 A C}}{2 A}$
124	122 123	bitr3i	$⊢ 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}$
125	121 8 10	divcli	$⊢ \frac{\sqrt{B^{2} - 4 A C}}{2 A} \in ℂ$
126	125 11 1	subadd2i	$⊢ (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = X \leftrightarrow X + (\frac{B}{2 A}) = \frac{\sqrt{B^{2} - 4 A C}}{2 A}$
127		eqcom	$⊢ (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = X \leftrightarrow X = (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A})$
128	126 127	bitr3i	$⊢ 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})$
129		divneg	$⊢ (B \in ℂ \land 2 A \in ℂ \land 2 A \neq 0) \to - \frac{B}{2 A} = \frac{- B}{2 A}$
130	4 8 10 129	mp3an	$⊢ - \frac{B}{2 A} = \frac{- B}{2 A}$
131	130	oveq2i	$⊢ (\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})$
132	125 11	negsubi	$⊢ (\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})$
133	4	negcli	$⊢ - B \in ℂ$
134	133 8 10	divcli	$⊢ \frac{- B}{2 A} \in ℂ$
135	125 134	addcomi	$⊢ (\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})$
136	131 132 135	3eqtr3i	$⊢ (\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})$
137	133 121 8 10	divdiri	$⊢ \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A} = (\frac{- B}{2 A}) + (\frac{\sqrt{B^{2} - 4 A C}}{2 A})$
138	136 137	eqtr4i	$⊢ (\frac{\sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = \frac{- B + \sqrt{B^{2} - 4 A C}}{2 A}$
139	138	eqeq2i	$⊢ 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}$
140	124 128 139	3bitri	$⊢ 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}$
141	121	negcli	$⊢ - \sqrt{B^{2} - 4 A C} \in ℂ$
142	141 8 12 10	divmuli	$⊢ \frac{- \sqrt{B^{2} - 4 A C}}{2 A} = X + (\frac{B}{2 A}) \leftrightarrow 2 A (X + (\frac{B}{2 A})) = - \sqrt{B^{2} - 4 A C}$
143		eqcom	$⊢ \frac{- \sqrt{B^{2} - 4 A C}}{2 A} = X + (\frac{B}{2 A}) \leftrightarrow X + (\frac{B}{2 A}) = \frac{- \sqrt{B^{2} - 4 A C}}{2 A}$
144	142 143	bitr3i	$⊢ 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}$
145	141 8 10	divcli	$⊢ \frac{- \sqrt{B^{2} - 4 A C}}{2 A} \in ℂ$
146	145 11 1	subadd2i	$⊢ (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = X \leftrightarrow X + (\frac{B}{2 A}) = \frac{- \sqrt{B^{2} - 4 A C}}{2 A}$
147		eqcom	$⊢ (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = X \leftrightarrow X = (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A})$
148	146 147	bitr3i	$⊢ 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})$
149	130	oveq2i	$⊢ (\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})$
150	145 11	negsubi	$⊢ (\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})$
151	145 134	addcomi	$⊢ (\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})$
152	149 150 151	3eqtr3i	$⊢ (\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})$
153	133 141 8 10	divdiri	$⊢ \frac{- B + (- \sqrt{B^{2} - 4 A C})}{2 A} = (\frac{- B}{2 A}) + (\frac{- \sqrt{B^{2} - 4 A C}}{2 A})$
154	133 121	negsubi	$⊢ - B + (- \sqrt{B^{2} - 4 A C}) = - B - \sqrt{B^{2} - 4 A C}$
155	154	oveq1i	$⊢ \frac{- B + (- \sqrt{B^{2} - 4 A C})}{2 A} = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A}$
156	152 153 155	3eqtr2i	$⊢ (\frac{- \sqrt{B^{2} - 4 A C}}{2 A}) - (\frac{B}{2 A}) = \frac{- B - \sqrt{B^{2} - 4 A C}}{2 A}$
157	156	eqeq2i	$⊢ 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}$
158	144 148 157	3bitri	$⊢ 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}$
159	140 158	orbi12i	$⊢ (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})$
160	119 159	mpbi	$⊢ (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 quad3

Proof