quadfac

Description: The solution of a quadratic equation via factoring. (Contributed by Luke Murphy, 10-Jul-2026)

	Ref	Expression
Hypotheses	quadfac.a	$⊢ φ \to A \in ℂ$
	quadfac.z	$⊢ φ \to A \neq 0$
	quadfac.b	$⊢ φ \to B \in ℂ$
	quadfac.c	$⊢ φ \to C \in ℂ$
	quadfac.x	$⊢ φ \to X \in ℂ$
	quadfac.m	$⊢ φ \to M \in ℂ$
	quadfac.n	$⊢ φ \to N \in ℂ$
	quadfac.mpn	$⊢ φ \to M + N = - \frac{B}{A}$
	quadfac.mtn	$⊢ φ \to M \cdot N = \frac{C}{A}$
Assertion	quadfac	$⊢ φ \to (A X^{2} + B X + C = 0 \leftrightarrow (X = M \lor X = N))$

Proof

Step	Hyp	Ref	Expression
1		quadfac.a	$⊢ φ \to A \in ℂ$
2		quadfac.z	$⊢ φ \to A \neq 0$
3		quadfac.b	$⊢ φ \to B \in ℂ$
4		quadfac.c	$⊢ φ \to C \in ℂ$
5		quadfac.x	$⊢ φ \to X \in ℂ$
6		quadfac.m	$⊢ φ \to M \in ℂ$
7		quadfac.n	$⊢ φ \to N \in ℂ$
8		quadfac.mpn	$⊢ φ \to M + N = - \frac{B}{A}$
9		quadfac.mtn	$⊢ φ \to M \cdot N = \frac{C}{A}$
10	5 6	subcld	$⊢ φ \to X - M \in ℂ$
11	5 7	subcld	$⊢ φ \to X - N \in ℂ$
12	10 11	mul0ord	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow (X - M = 0 \lor X - N = 0))$
13		olc	$⊢ X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0 \to (A = 0 \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0)$
14	2	neneqd	$⊢ φ \to \neg A = 0$
15		id	$⊢ A = 0 \to A = 0$
16		falim	$⊢ ⊥ \to A = 0$
17	15 16	pm5.21ni	$⊢ \neg A = 0 \to (A = 0 \leftrightarrow ⊥)$
18	14 17	syl	$⊢ φ \to (A = 0 \leftrightarrow ⊥)$
19	18	orbi1d	$⊢ φ \to ((A = 0 \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0) \leftrightarrow (⊥ \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0))$
20		falim	$⊢ ⊥ \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0$
21		id	$⊢ X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0 \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0$
22	20 21	jaoi	$⊢ (⊥ \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0) \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0$
23	22	a1i	$⊢ φ \to ((⊥ \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0) \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0)$
24	19 23	sylbid	$⊢ φ \to ((A = 0 \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0) \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0)$
25	13 24	impbid2	$⊢ φ \to (X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0 \leftrightarrow (A = 0 \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0))$
26	5 6 5 7	mulsubd	$⊢ φ \to (X - M) (X - N) = X X + N \cdot M - (X \cdot N + X \cdot M)$
27	5	sqvald	$⊢ φ \to X^{2} = X X$
28	27	eqcomd	$⊢ φ \to X X = X^{2}$
29	6 7	mulcomd	$⊢ φ \to M \cdot N = N \cdot M$
30	29 9	eqtr3d	$⊢ φ \to N \cdot M = \frac{C}{A}$
31	28 30	oveq12d	$⊢ φ \to X X + N \cdot M = X^{2} + (\frac{C}{A})$
32	7 6	addcomd	$⊢ φ \to N + M = M + N$
33	32	oveq1d	$⊢ φ \to (N + M) X = (M + N) X$
34	7 5	mulcomd	$⊢ φ \to N X = X \cdot N$
35	6 5	mulcomd	$⊢ φ \to M X = X \cdot M$
36	34 35	oveq12d	$⊢ φ \to N X + M X = X \cdot N + X \cdot M$
37	7 5 6 36	joinlmuladdmuld	$⊢ φ \to (N + M) X = X \cdot N + X \cdot M$
38	8	oveq1d	$⊢ φ \to (M + N) X = (- \frac{B}{A}) X$
39	33 37 38	3eqtr3d	$⊢ φ \to X \cdot N + X \cdot M = (- \frac{B}{A}) X$
40	31 39	oveq12d	$⊢ φ \to X X + N \cdot M - (X \cdot N + X \cdot M) = X^{2} + (\frac{C}{A}) - (- \frac{B}{A}) X$
41	26 40	eqtrd	$⊢ φ \to (X - M) (X - N) = X^{2} + (\frac{C}{A}) - (- \frac{B}{A}) X$
42	41	eqeq1d	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow X^{2} + (\frac{C}{A}) - (- \frac{B}{A}) X = 0)$
43	3 1 2	divcld	$⊢ φ \to \frac{B}{A} \in ℂ$
44	43 5	mulneg1d	$⊢ φ \to (- \frac{B}{A}) X = - (\frac{B}{A}) X$
45	44	oveq2d	$⊢ φ \to X^{2} + (\frac{C}{A}) - (- \frac{B}{A}) X = X^{2} + (\frac{C}{A}) - (- (\frac{B}{A}) X)$
46	45	eqeq1d	$⊢ φ \to (X^{2} + (\frac{C}{A}) - (- \frac{B}{A}) X = 0 \leftrightarrow X^{2} + (\frac{C}{A}) - (- (\frac{B}{A}) X) = 0)$
47	5	sqcld	$⊢ φ \to X^{2} \in ℂ$
48	4 1 2	divcld	$⊢ φ \to \frac{C}{A} \in ℂ$
49	47 48	addcld	$⊢ φ \to X^{2} + (\frac{C}{A}) \in ℂ$
50	43 5	mulcld	$⊢ φ \to (\frac{B}{A}) X \in ℂ$
51	49 50	subnegd	$⊢ φ \to X^{2} + (\frac{C}{A}) - (- (\frac{B}{A}) X) = X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X$
52	51	eqeq1d	$⊢ φ \to (X^{2} + (\frac{C}{A}) - (- (\frac{B}{A}) X) = 0 \leftrightarrow X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0)$
53	42 46 52	3bitrd	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0)$
54	49 50	addcld	$⊢ φ \to X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X \in ℂ$
55	1 54	mul0ord	$⊢ φ \to (A (X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X) = 0 \leftrightarrow (A = 0 \lor X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X = 0))$
56	25 53 55	3bitr4d	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow A (X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X) = 0)$
57	1 49 50	adddid	$⊢ φ \to A (X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X) = A (X^{2} + (\frac{C}{A})) + A (\frac{B}{A}) X$
58	57	eqeq1d	$⊢ φ \to (A (X^{2} + (\frac{C}{A}) + (\frac{B}{A}) X) = 0 \leftrightarrow A (X^{2} + (\frac{C}{A})) + A (\frac{B}{A}) X = 0)$
59	1 47 48	adddid	$⊢ φ \to A (X^{2} + (\frac{C}{A})) = A X^{2} + A (\frac{C}{A})$
60	4 1 2	divcan2d	$⊢ φ \to A (\frac{C}{A}) = C$
61	60	oveq2d	$⊢ φ \to A X^{2} + A (\frac{C}{A}) = A X^{2} + C$
62	59 61	eqtrd	$⊢ φ \to A (X^{2} + (\frac{C}{A})) = A X^{2} + C$
63	1 43 5	mulassd	$⊢ φ \to A (\frac{B}{A}) X = A (\frac{B}{A}) X$
64	3 1 2	divcan2d	$⊢ φ \to A (\frac{B}{A}) = B$
65	64	oveq1d	$⊢ φ \to A (\frac{B}{A}) X = B X$
66	63 65	eqtr3d	$⊢ φ \to A (\frac{B}{A}) X = B X$
67	62 66	oveq12d	$⊢ φ \to A (X^{2} + (\frac{C}{A})) + A (\frac{B}{A}) X = A X^{2} + C + B X$
68	67	eqeq1d	$⊢ φ \to (A (X^{2} + (\frac{C}{A})) + A (\frac{B}{A}) X = 0 \leftrightarrow A X^{2} + C + B X = 0)$
69	56 58 68	3bitrd	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow A X^{2} + C + B X = 0)$
70	1 47	mulcld	$⊢ φ \to A X^{2} \in ℂ$
71	3 5	mulcld	$⊢ φ \to B X \in ℂ$
72	70 4 71	addassd	$⊢ φ \to A X^{2} + C + B X = A X^{2} + C + B X$
73	72	eqeq1d	$⊢ φ \to (A X^{2} + C + B X = 0 \leftrightarrow A X^{2} + C + B X = 0)$
74	4 71	addcomd	$⊢ φ \to C + B X = B X + C$
75	74	oveq2d	$⊢ φ \to A X^{2} + C + B X = A X^{2} + B X + C$
76	75	eqeq1d	$⊢ φ \to (A X^{2} + C + B X = 0 \leftrightarrow A X^{2} + B X + C = 0)$
77	69 73 76	3bitrd	$⊢ φ \to ((X - M) (X - N) = 0 \leftrightarrow A X^{2} + B X + C = 0)$
78	5 6	subeq0ad	$⊢ φ \to (X - M = 0 \leftrightarrow X = M)$
79	5 7	subeq0ad	$⊢ φ \to (X - N = 0 \leftrightarrow X = N)$
80	78 79	orbi12d	$⊢ φ \to ((X - M = 0 \lor X - N = 0) \leftrightarrow (X = M \lor X = N))$
81	12 77 80	3bitr3d	$⊢ φ \to (A X^{2} + B X + C = 0 \leftrightarrow (X = M \lor X = N))$

Metamath Proof Explorer

Theorem quadfac

Proof