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

Metamath Proof Explorer

Theorem constrrtcclem

Proof