constrrtcclem

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. Case of non-degenerate circles. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	constrrtcc.s	$⊢ φ \to S \subseteq ℂ$
	constrrtcc.a	$⊢ φ \to A \in S$
	constrrtcc.b	$⊢ φ \to B \in S$
	constrrtcc.c	$⊢ φ \to C \in S$
	constrrtcc.d	$⊢ φ \to D \in S$
	constrrtcc.e	$⊢ φ \to E \in S$
	constrrtcc.f	$⊢ φ \to F \in S$
	constrrtcc.x	$⊢ φ \to X \in ℂ$
	constrrtcc.1	$⊢ φ \to A \neq D$
	constrrtcc.2	$⊢ φ \to \|X - A\| = \|B - C\|$
	constrrtcc.3	$⊢ φ \to \|X - D\| = \|E - F\|$
	constrrtcc.4	$⊢ P = (B - C) \overline{B - C}$
	constrrtcc.5	$⊢ Q = (E - F) \overline{E - F}$
	constrrtcc.m	$⊢ M = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
	constrrtcc.n	$⊢ N = - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}$
	constrrtcclem.1	$⊢ φ \to B \neq C$
	constrrtcclem.2	$⊢ φ \to E \neq F$
Assertion	constrrtcclem	$⊢ φ \to X^{2} + M X + N = 0$

Proof

Step	Hyp	Ref	Expression
1		constrrtcc.s	$⊢ φ \to S \subseteq ℂ$
2		constrrtcc.a	$⊢ φ \to A \in S$
3		constrrtcc.b	$⊢ φ \to B \in S$
4		constrrtcc.c	$⊢ φ \to C \in S$
5		constrrtcc.d	$⊢ φ \to D \in S$
6		constrrtcc.e	$⊢ φ \to E \in S$
7		constrrtcc.f	$⊢ φ \to F \in S$
8		constrrtcc.x	$⊢ φ \to X \in ℂ$
9		constrrtcc.1	$⊢ φ \to A \neq D$
10		constrrtcc.2	$⊢ φ \to \|X - A\| = \|B - C\|$
11		constrrtcc.3	$⊢ φ \to \|X - D\| = \|E - F\|$
12		constrrtcc.4	$⊢ P = (B - C) \overline{B - C}$
13		constrrtcc.5	$⊢ Q = (E - F) \overline{E - F}$
14		constrrtcc.m	$⊢ M = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
15		constrrtcc.n	$⊢ N = - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}$
16		constrrtcclem.1	$⊢ φ \to B \neq C$
17		constrrtcclem.2	$⊢ φ \to E \neq F$
18	8	sqcld	$⊢ φ \to X^{2} \in ℂ$
19	1 6	sseldd	$⊢ φ \to E \in ℂ$
20	1 7	sseldd	$⊢ φ \to F \in ℂ$
21	19 20	subcld	$⊢ φ \to E - F \in ℂ$
22	21	cjcld	$⊢ φ \to \overline{E - F} \in ℂ$
23	21 22	mulcld	$⊢ φ \to (E - F) \overline{E - F} \in ℂ$
24	13 23	eqeltrid	$⊢ φ \to Q \in ℂ$
25	1 5	sseldd	$⊢ φ \to D \in ℂ$
26	25	cjcld	$⊢ φ \to \overline{D} \in ℂ$
27	1 2	sseldd	$⊢ φ \to A \in ℂ$
28	25 27	addcld	$⊢ φ \to D + A \in ℂ$
29	26 28	mulcld	$⊢ φ \to \overline{D} (D + A) \in ℂ$
30	24 29	subcld	$⊢ φ \to Q - \overline{D} (D + A) \in ℂ$
31	1 3	sseldd	$⊢ φ \to B \in ℂ$
32	1 4	sseldd	$⊢ φ \to C \in ℂ$
33	31 32	subcld	$⊢ φ \to B - C \in ℂ$
34	33	cjcld	$⊢ φ \to \overline{B - C} \in ℂ$
35	33 34	mulcld	$⊢ φ \to (B - C) \overline{B - C} \in ℂ$
36	12 35	eqeltrid	$⊢ φ \to P \in ℂ$
37	27	cjcld	$⊢ φ \to \overline{A} \in ℂ$
38	37 28	mulcld	$⊢ φ \to \overline{A} (D + A) \in ℂ$
39	36 38	subcld	$⊢ φ \to P - \overline{A} (D + A) \in ℂ$
40	30 39	subcld	$⊢ φ \to Q - \overline{D} (D + A) - (P - \overline{A} (D + A)) \in ℂ$
41	26 37	subcld	$⊢ φ \to \overline{D} - \overline{A} \in ℂ$
42	25 27	cjsubd	$⊢ φ \to \overline{D - A} = \overline{D} - \overline{A}$
43	25 27	subcld	$⊢ φ \to D - A \in ℂ$
44	9	necomd	$⊢ φ \to D \neq A$
45	25 27 44	subne0d	$⊢ φ \to D - A \neq 0$
46	43 45	cjne0d	$⊢ φ \to \overline{D - A} \neq 0$
47	42 46	eqnetrrd	$⊢ φ \to \overline{D} - \overline{A} \neq 0$
48	40 41 47	divcld	$⊢ φ \to \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}} \in ℂ$
49	14 48	eqeltrid	$⊢ φ \to M \in ℂ$
50	49 8	mulcld	$⊢ φ \to M X \in ℂ$
51	25 27	mulcld	$⊢ φ \to D A \in ℂ$
52	37 51	mulcld	$⊢ φ \to \overline{A} D A \in ℂ$
53	36 25	mulcld	$⊢ φ \to P D \in ℂ$
54	52 53	subcld	$⊢ φ \to \overline{A} D A - P D \in ℂ$
55	26 51	mulcld	$⊢ φ \to \overline{D} D A \in ℂ$
56	24 27	mulcld	$⊢ φ \to Q A \in ℂ$
57	55 56	subcld	$⊢ φ \to \overline{D} D A - Q A \in ℂ$
58	54 57	subcld	$⊢ φ \to \overline{A} D A - P D - (\overline{D} D A - Q A) \in ℂ$
59	58 41 47	divcld	$⊢ φ \to \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} \in ℂ$
60	59	negcld	$⊢ φ \to - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} \in ℂ$
61	15 60	eqeltrid	$⊢ φ \to N \in ℂ$
62	18 50 61	addassd	$⊢ φ \to X^{2} + M X + N = X^{2} + M X + N$
63	15	eqcomi	$⊢ - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = N$
64	63	a1i	$⊢ φ \to - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = N$
65	59 64	negcon1ad	$⊢ φ \to - N = \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}$
66	65 59	eqeltrd	$⊢ φ \to - N \in ℂ$
67	41 18	mulcld	$⊢ φ \to (\overline{D} - \overline{A}) X^{2} \in ℂ$
68	40 8	mulcld	$⊢ φ \to (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X \in ℂ$
69	26 37 18	subdird	$⊢ φ \to (\overline{D} - \overline{A}) X^{2} = \overline{D} X^{2} - \overline{A} X^{2}$
70	30 39 8	subdird	$⊢ φ \to (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X = (Q - \overline{D} (D + A)) X - (P - \overline{A} (D + A)) X$
71	69 70	oveq12d	$⊢ φ \to (\overline{D} - \overline{A}) X^{2} + (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X = (\overline{D} X^{2} - \overline{A} X^{2}) + (Q - \overline{D} (D + A)) X - (P - \overline{A} (D + A)) X$
72	26 18	mulcld	$⊢ φ \to \overline{D} X^{2} \in ℂ$
73	30 8	mulcld	$⊢ φ \to (Q - \overline{D} (D + A)) X \in ℂ$
74	37 18	mulcld	$⊢ φ \to \overline{A} X^{2} \in ℂ$
75	39 8	mulcld	$⊢ φ \to (P - \overline{A} (D + A)) X \in ℂ$
76	72 73 74 75	addsub4d	$⊢ φ \to \overline{D} X^{2} + (Q - \overline{D} (D + A)) X - (\overline{A} X^{2} + (P - \overline{A} (D + A)) X) = (\overline{D} X^{2} - \overline{A} X^{2}) + (Q - \overline{D} (D + A)) X - (P - \overline{A} (D + A)) X$
77	8 27	subcld	$⊢ φ \to X - A \in ℂ$
78	8 25	subcld	$⊢ φ \to X - D \in ℂ$
79	77 78	mulcomd	$⊢ φ \to (X - A) (X - D) = (X - D) (X - A)$
80	79	oveq2d	$⊢ φ \to \overline{X} (X - A) (X - D) = \overline{X} (X - D) (X - A)$
81	77	cjcld	$⊢ φ \to \overline{X - A} \in ℂ$
82	31 32 16	subne0d	$⊢ φ \to B - C \neq 0$
83	33 82	absne0d	$⊢ φ \to \|B - C\| \neq 0$
84	10 83	eqnetrd	$⊢ φ \to \|X - A\| \neq 0$
85	77	abs00ad	$⊢ φ \to (\|X - A\| = 0 \leftrightarrow X - A = 0)$
86	85	necon3bid	$⊢ φ \to (\|X - A\| \neq 0 \leftrightarrow X - A \neq 0)$
87	84 86	mpbid	$⊢ φ \to X - A \neq 0$
88	10	oveq1d	$⊢ φ \to {\|X - A\|}^{2} = {\|B - C\|}^{2}$
89	77	absvalsqd	$⊢ φ \to {\|X - A\|}^{2} = (X - A) \overline{X - A}$
90	33	absvalsqd	$⊢ φ \to {\|B - C\|}^{2} = (B - C) \overline{B - C}$
91	88 89 90	3eqtr3d	$⊢ φ \to (X - A) \overline{X - A} = (B - C) \overline{B - C}$
92	91 12	eqtr4di	$⊢ φ \to (X - A) \overline{X - A} = P$
93	77 81 87 92	mvllmuld	$⊢ φ \to \overline{X - A} = \frac{P}{X - A}$
94	93 81	eqeltrrd	$⊢ φ \to \frac{P}{X - A} \in ℂ$
95	37 94	addcld	$⊢ φ \to \overline{A} + (\frac{P}{X - A}) \in ℂ$
96	95 77 78	mulassd	$⊢ φ \to (\overline{A} + (\frac{P}{X - A})) (X - A) (X - D) = (\overline{A} + (\frac{P}{X - A})) (X - A) (X - D)$
97	36 77 87	divcan1d	$⊢ φ \to (\frac{P}{X - A}) (X - A) = P$
98	97	oveq2d	$⊢ φ \to \overline{A} (X - A) + (\frac{P}{X - A}) (X - A) = \overline{A} (X - A) + P$
99	37 77 94 98	joinlmuladdmuld	$⊢ φ \to (\overline{A} + (\frac{P}{X - A})) (X - A) = \overline{A} (X - A) + P$
100	99	oveq1d	$⊢ φ \to (\overline{A} + (\frac{P}{X - A})) (X - A) (X - D) = (\overline{A} (X - A) + P) (X - D)$
101	37 77	mulcld	$⊢ φ \to \overline{A} (X - A) \in ℂ$
102	101 36 78	adddird	$⊢ φ \to (\overline{A} (X - A) + P) (X - D) = \overline{A} (X - A) (X - D) + P (X - D)$
103	37 77 78	mulassd	$⊢ φ \to \overline{A} (X - A) (X - D) = \overline{A} (X - A) (X - D)$
104	8 27 8 25	mulsubd	$⊢ φ \to (X - A) (X - D) = X X + D A - (X D + X A)$
105	8	sqvald	$⊢ φ \to X^{2} = X X$
106	105	oveq1d	$⊢ φ \to X^{2} + D A = X X + D A$
107	8 25 27	adddid	$⊢ φ \to X (D + A) = X D + X A$
108	106 107	oveq12d	$⊢ φ \to X^{2} + D A - X (D + A) = X X + D A - (X D + X A)$
109	8 28	mulcld	$⊢ φ \to X (D + A) \in ℂ$
110	18 51 109	addsubd	$⊢ φ \to X^{2} + D A - X (D + A) = X^{2} - X (D + A) + D A$
111	104 108 110	3eqtr2d	$⊢ φ \to (X - A) (X - D) = X^{2} - X (D + A) + D A$
112	111	oveq2d	$⊢ φ \to \overline{A} (X - A) (X - D) = \overline{A} (X^{2} - X (D + A) + D A)$
113	18 109	subcld	$⊢ φ \to X^{2} - X (D + A) \in ℂ$
114	37 113 51	adddid	$⊢ φ \to \overline{A} (X^{2} - X (D + A) + D A) = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A$
115	103 112 114	3eqtrd	$⊢ φ \to \overline{A} (X - A) (X - D) = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A$
116	36 8 25	subdid	$⊢ φ \to P (X - D) = P X - P D$
117	115 116	oveq12d	$⊢ φ \to \overline{A} (X - A) (X - D) + P (X - D) = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A + (P X - P D)$
118	100 102 117	3eqtrd	$⊢ φ \to (\overline{A} + (\frac{P}{X - A})) (X - A) (X - D) = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A + (P X - P D)$
119	8 27	cjsubd	$⊢ φ \to \overline{X - A} = \overline{X} - \overline{A}$
120	119 93	eqtr3d	$⊢ φ \to \overline{X} - \overline{A} = \frac{P}{X - A}$
121	8	cjcld	$⊢ φ \to \overline{X} \in ℂ$
122	121 37 94	subaddd	$⊢ φ \to (\overline{X} - \overline{A} = \frac{P}{X - A} \leftrightarrow \overline{A} + (\frac{P}{X - A}) = \overline{X})$
123	120 122	mpbid	$⊢ φ \to \overline{A} + (\frac{P}{X - A}) = \overline{X}$
124	123	oveq1d	$⊢ φ \to (\overline{A} + (\frac{P}{X - A})) (X - A) (X - D) = \overline{X} (X - A) (X - D)$
125	96 118 124	3eqtr3rd	$⊢ φ \to \overline{X} (X - A) (X - D) = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A + (P X - P D)$
126	37 113	mulcld	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) \in ℂ$
127	126 52	addcld	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + \overline{A} D A \in ℂ$
128	36 8	mulcld	$⊢ φ \to P X \in ℂ$
129	127 128 53	addsubassd	$⊢ φ \to (\overline{A} (X^{2} - X (D + A)) + \overline{A} D A) + P X - P D = \overline{A} (X^{2} - X (D + A)) + \overline{A} D A + (P X - P D)$
130	126 52 128	add32d	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + \overline{A} D A + P X = \overline{A} (X^{2} - X (D + A)) + P X + \overline{A} D A$
131	130	oveq1d	$⊢ φ \to (\overline{A} (X^{2} - X (D + A)) + \overline{A} D A) + P X - P D = (\overline{A} (X^{2} - X (D + A)) + P X) + \overline{A} D A - P D$
132	125 129 131	3eqtr2d	$⊢ φ \to \overline{X} (X - A) (X - D) = (\overline{A} (X^{2} - X (D + A)) + P X) + \overline{A} D A - P D$
133	126 128	addcld	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + P X \in ℂ$
134	133 52 53	addsubassd	$⊢ φ \to (\overline{A} (X^{2} - X (D + A)) + P X) + \overline{A} D A - P D = \overline{A} (X^{2} - X (D + A)) + P X + (\overline{A} D A - P D)$
135	38 8	mulcld	$⊢ φ \to \overline{A} (D + A) X \in ℂ$
136	74 135 128	subadd23d	$⊢ φ \to \overline{A} X^{2} - \overline{A} (D + A) X + P X = \overline{A} X^{2} + P X - \overline{A} (D + A) X$
137	37 18 109	subdid	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) = \overline{A} X^{2} - \overline{A} X (D + A)$
138	37 8 28	mul12d	$⊢ φ \to \overline{A} X (D + A) = X \overline{A} (D + A)$
139	8 38	mulcomd	$⊢ φ \to X \overline{A} (D + A) = \overline{A} (D + A) X$
140	138 139	eqtrd	$⊢ φ \to \overline{A} X (D + A) = \overline{A} (D + A) X$
141	140	oveq2d	$⊢ φ \to \overline{A} X^{2} - \overline{A} X (D + A) = \overline{A} X^{2} - \overline{A} (D + A) X$
142	137 141	eqtrd	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) = \overline{A} X^{2} - \overline{A} (D + A) X$
143	142	oveq1d	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + P X = \overline{A} X^{2} - \overline{A} (D + A) X + P X$
144	36 38 8	subdird	$⊢ φ \to (P - \overline{A} (D + A)) X = P X - \overline{A} (D + A) X$
145	144	oveq2d	$⊢ φ \to \overline{A} X^{2} + (P - \overline{A} (D + A)) X = \overline{A} X^{2} + P X - \overline{A} (D + A) X$
146	136 143 145	3eqtr4d	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + P X = \overline{A} X^{2} + (P - \overline{A} (D + A)) X$
147	146	oveq1d	$⊢ φ \to \overline{A} (X^{2} - X (D + A)) + P X + (\overline{A} D A - P D) = \overline{A} X^{2} + (P - \overline{A} (D + A)) X + (\overline{A} D A - P D)$
148	132 134 147	3eqtrd	$⊢ φ \to \overline{X} (X - A) (X - D) = \overline{A} X^{2} + (P - \overline{A} (D + A)) X + (\overline{A} D A - P D)$
149	78	cjcld	$⊢ φ \to \overline{X - D} \in ℂ$
150	19 20 17	subne0d	$⊢ φ \to E - F \neq 0$
151	21 150	absne0d	$⊢ φ \to \|E - F\| \neq 0$
152	11 151	eqnetrd	$⊢ φ \to \|X - D\| \neq 0$
153	78	abs00ad	$⊢ φ \to (\|X - D\| = 0 \leftrightarrow X - D = 0)$
154	153	necon3bid	$⊢ φ \to (\|X - D\| \neq 0 \leftrightarrow X - D \neq 0)$
155	152 154	mpbid	$⊢ φ \to X - D \neq 0$
156	11	oveq1d	$⊢ φ \to {\|X - D\|}^{2} = {\|E - F\|}^{2}$
157	78	absvalsqd	$⊢ φ \to {\|X - D\|}^{2} = (X - D) \overline{X - D}$
158	21	absvalsqd	$⊢ φ \to {\|E - F\|}^{2} = (E - F) \overline{E - F}$
159	156 157 158	3eqtr3d	$⊢ φ \to (X - D) \overline{X - D} = (E - F) \overline{E - F}$
160	159 13	eqtr4di	$⊢ φ \to (X - D) \overline{X - D} = Q$
161	78 149 155 160	mvllmuld	$⊢ φ \to \overline{X - D} = \frac{Q}{X - D}$
162	161 149	eqeltrrd	$⊢ φ \to \frac{Q}{X - D} \in ℂ$
163	26 162	addcld	$⊢ φ \to \overline{D} + (\frac{Q}{X - D}) \in ℂ$
164	163 78 77	mulassd	$⊢ φ \to (\overline{D} + (\frac{Q}{X - D})) (X - D) (X - A) = (\overline{D} + (\frac{Q}{X - D})) (X - D) (X - A)$
165	24 78 155	divcan1d	$⊢ φ \to (\frac{Q}{X - D}) (X - D) = Q$
166	165	oveq2d	$⊢ φ \to \overline{D} (X - D) + (\frac{Q}{X - D}) (X - D) = \overline{D} (X - D) + Q$
167	26 78 162 166	joinlmuladdmuld	$⊢ φ \to (\overline{D} + (\frac{Q}{X - D})) (X - D) = \overline{D} (X - D) + Q$
168	167	oveq1d	$⊢ φ \to (\overline{D} + (\frac{Q}{X - D})) (X - D) (X - A) = (\overline{D} (X - D) + Q) (X - A)$
169	26 78	mulcld	$⊢ φ \to \overline{D} (X - D) \in ℂ$
170	169 24 77	adddird	$⊢ φ \to (\overline{D} (X - D) + Q) (X - A) = \overline{D} (X - D) (X - A) + Q (X - A)$
171	26 78 77	mulassd	$⊢ φ \to \overline{D} (X - D) (X - A) = \overline{D} (X - D) (X - A)$
172	79	oveq2d	$⊢ φ \to \overline{D} (X - A) (X - D) = \overline{D} (X - D) (X - A)$
173	171 172	eqtr4d	$⊢ φ \to \overline{D} (X - D) (X - A) = \overline{D} (X - A) (X - D)$
174	111	oveq2d	$⊢ φ \to \overline{D} (X - A) (X - D) = \overline{D} (X^{2} - X (D + A) + D A)$
175	26 113 51	adddid	$⊢ φ \to \overline{D} (X^{2} - X (D + A) + D A) = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A$
176	173 174 175	3eqtrd	$⊢ φ \to \overline{D} (X - D) (X - A) = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A$
177	24 8 27	subdid	$⊢ φ \to Q (X - A) = Q X - Q A$
178	176 177	oveq12d	$⊢ φ \to \overline{D} (X - D) (X - A) + Q (X - A) = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A + (Q X - Q A)$
179	168 170 178	3eqtrd	$⊢ φ \to (\overline{D} + (\frac{Q}{X - D})) (X - D) (X - A) = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A + (Q X - Q A)$
180	8 25	cjsubd	$⊢ φ \to \overline{X - D} = \overline{X} - \overline{D}$
181	180 161	eqtr3d	$⊢ φ \to \overline{X} - \overline{D} = \frac{Q}{X - D}$
182	121 26 162	subaddd	$⊢ φ \to (\overline{X} - \overline{D} = \frac{Q}{X - D} \leftrightarrow \overline{D} + (\frac{Q}{X - D}) = \overline{X})$
183	181 182	mpbid	$⊢ φ \to \overline{D} + (\frac{Q}{X - D}) = \overline{X}$
184	183	oveq1d	$⊢ φ \to (\overline{D} + (\frac{Q}{X - D})) (X - D) (X - A) = \overline{X} (X - D) (X - A)$
185	164 179 184	3eqtr3rd	$⊢ φ \to \overline{X} (X - D) (X - A) = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A + (Q X - Q A)$
186	26 113	mulcld	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) \in ℂ$
187	186 55	addcld	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + \overline{D} D A \in ℂ$
188	24 8	mulcld	$⊢ φ \to Q X \in ℂ$
189	187 188 56	addsubassd	$⊢ φ \to (\overline{D} (X^{2} - X (D + A)) + \overline{D} D A) + Q X - Q A = \overline{D} (X^{2} - X (D + A)) + \overline{D} D A + (Q X - Q A)$
190	186 55 188	add32d	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + \overline{D} D A + Q X = \overline{D} (X^{2} - X (D + A)) + Q X + \overline{D} D A$
191	190	oveq1d	$⊢ φ \to (\overline{D} (X^{2} - X (D + A)) + \overline{D} D A) + Q X - Q A = (\overline{D} (X^{2} - X (D + A)) + Q X) + \overline{D} D A - Q A$
192	185 189 191	3eqtr2d	$⊢ φ \to \overline{X} (X - D) (X - A) = (\overline{D} (X^{2} - X (D + A)) + Q X) + \overline{D} D A - Q A$
193	186 188	addcld	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + Q X \in ℂ$
194	193 55 56	addsubassd	$⊢ φ \to (\overline{D} (X^{2} - X (D + A)) + Q X) + \overline{D} D A - Q A = \overline{D} (X^{2} - X (D + A)) + Q X + (\overline{D} D A - Q A)$
195	29 8	mulcld	$⊢ φ \to \overline{D} (D + A) X \in ℂ$
196	72 195 188	subadd23d	$⊢ φ \to \overline{D} X^{2} - \overline{D} (D + A) X + Q X = \overline{D} X^{2} + Q X - \overline{D} (D + A) X$
197	26 18 109	subdid	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) = \overline{D} X^{2} - \overline{D} X (D + A)$
198	26 8 28	mul12d	$⊢ φ \to \overline{D} X (D + A) = X \overline{D} (D + A)$
199	8 29	mulcomd	$⊢ φ \to X \overline{D} (D + A) = \overline{D} (D + A) X$
200	198 199	eqtrd	$⊢ φ \to \overline{D} X (D + A) = \overline{D} (D + A) X$
201	200	oveq2d	$⊢ φ \to \overline{D} X^{2} - \overline{D} X (D + A) = \overline{D} X^{2} - \overline{D} (D + A) X$
202	197 201	eqtrd	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) = \overline{D} X^{2} - \overline{D} (D + A) X$
203	202	oveq1d	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + Q X = \overline{D} X^{2} - \overline{D} (D + A) X + Q X$
204	24 29 8	subdird	$⊢ φ \to (Q - \overline{D} (D + A)) X = Q X - \overline{D} (D + A) X$
205	204	oveq2d	$⊢ φ \to \overline{D} X^{2} + (Q - \overline{D} (D + A)) X = \overline{D} X^{2} + Q X - \overline{D} (D + A) X$
206	196 203 205	3eqtr4d	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + Q X = \overline{D} X^{2} + (Q - \overline{D} (D + A)) X$
207	206	oveq1d	$⊢ φ \to \overline{D} (X^{2} - X (D + A)) + Q X + (\overline{D} D A - Q A) = \overline{D} X^{2} + (Q - \overline{D} (D + A)) X + (\overline{D} D A - Q A)$
208	192 194 207	3eqtrd	$⊢ φ \to \overline{X} (X - D) (X - A) = \overline{D} X^{2} + (Q - \overline{D} (D + A)) X + (\overline{D} D A - Q A)$
209	80 148 208	3eqtr3d	$⊢ φ \to \overline{A} X^{2} + (P - \overline{A} (D + A)) X + (\overline{A} D A - P D) = \overline{D} X^{2} + (Q - \overline{D} (D + A)) X + (\overline{D} D A - Q A)$
210	146 133	eqeltrrd	$⊢ φ \to \overline{A} X^{2} + (P - \overline{A} (D + A)) X \in ℂ$
211	206 193	eqeltrrd	$⊢ φ \to \overline{D} X^{2} + (Q - \overline{D} (D + A)) X \in ℂ$
212	210 54 211 57	addsubeq4d	$⊢ φ \to (\overline{A} X^{2} + (P - \overline{A} (D + A)) X + (\overline{A} D A - P D) = \overline{D} X^{2} + (Q - \overline{D} (D + A)) X + (\overline{D} D A - Q A) \leftrightarrow \overline{D} X^{2} + (Q - \overline{D} (D + A)) X - (\overline{A} X^{2} + (P - \overline{A} (D + A)) X) = \overline{A} D A - P D - (\overline{D} D A - Q A))$
213	209 212	mpbid	$⊢ φ \to \overline{D} X^{2} + (Q - \overline{D} (D + A)) X - (\overline{A} X^{2} + (P - \overline{A} (D + A)) X) = \overline{A} D A - P D - (\overline{D} D A - Q A)$
214	71 76 213	3eqtr2d	$⊢ φ \to (\overline{D} - \overline{A}) X^{2} + (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X = \overline{A} D A - P D - (\overline{D} D A - Q A)$
215	67 68 214	mvlraddd	$⊢ φ \to (\overline{D} - \overline{A}) X^{2} = (\overline{A} D A - P D) - (\overline{D} D A - Q A) - (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X$
216	41 18 47 215	mvllmuld	$⊢ φ \to X^{2} = \frac{(\overline{A} D A - P D) - (\overline{D} D A - Q A) - (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}}$
217	58 68 41 47	divsubdird	$⊢ φ \to \frac{(\overline{A} D A - P D) - (\overline{D} D A - Q A) - (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}} = (\frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}) - (\frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}})$
218	65	oveq1d	$⊢ φ \to - N - (\frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}}) = (\frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}) - (\frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}})$
219	217 218	eqtr4d	$⊢ φ \to \frac{(\overline{A} D A - P D) - (\overline{D} D A - Q A) - (Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}} = - N - (\frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}})$
220	40 8 41 47	div23d	$⊢ φ \to \frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}} = (\frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}) X$
221	14	oveq1i	$⊢ M X = (\frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}) X$
222	220 221	eqtr4di	$⊢ φ \to \frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}} = M X$
223	222	oveq2d	$⊢ φ \to - N - (\frac{(Q - \overline{D} (D + A) - (P - \overline{A} (D + A))) X}{\overline{D} - \overline{A}}) = - N - M X$
224	216 219 223	3eqtrd	$⊢ φ \to X^{2} = - N - M X$
225	66 50 224	mvrrsubd	$⊢ φ \to X^{2} + M X = - N$
226	18 50	addcld	$⊢ φ \to X^{2} + M X \in ℂ$
227		addeq0	$⊢ (X^{2} + M X \in ℂ \land N \in ℂ) \to (X^{2} + M X + N = 0 \leftrightarrow X^{2} + M X = - N)$
228	226 61 227	syl2anc	$⊢ φ \to (X^{2} + M X + N = 0 \leftrightarrow X^{2} + M X = - N)$
229	225 228	mpbird	$⊢ φ \to X^{2} + M X + N = 0$
230	62 229	eqtr3d	$⊢ φ \to X^{2} + M X + N = 0$

Metamath Proof Explorer

Theorem constrrtcclem

Proof