constrrtcc

Description: In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (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}}$
Assertion	constrrtcc	$⊢ φ \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	14	a1i	$⊢ (φ \land B = C) \to M = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
17	1 6	sseldd	$⊢ φ \to E \in ℂ$
18	1 7	sseldd	$⊢ φ \to F \in ℂ$
19	17 18	subcld	$⊢ φ \to E - F \in ℂ$
20	19	adantr	$⊢ (φ \land B = C) \to E - F \in ℂ$
21	20	absvalsqd	$⊢ (φ \land B = C) \to {\|E - F\|}^{2} = (E - F) \overline{E - F}$
22	13 21	eqtr4id	$⊢ (φ \land B = C) \to Q = {\|E - F\|}^{2}$
23	8	adantr	$⊢ (φ \land B = C) \to X \in ℂ$
24	1 2	sseldd	$⊢ φ \to A \in ℂ$
25	24	adantr	$⊢ (φ \land B = C) \to A \in ℂ$
26	8 24	subcld	$⊢ φ \to X - A \in ℂ$
27	26	adantr	$⊢ (φ \land B = C) \to X - A \in ℂ$
28	10	adantr	$⊢ (φ \land B = C) \to \|X - A\| = \|B - C\|$
29	1 3	sseldd	$⊢ φ \to B \in ℂ$
30	29	adantr	$⊢ (φ \land B = C) \to B \in ℂ$
31		simpr	$⊢ (φ \land B = C) \to B = C$
32	30 31	subeq0bd	$⊢ (φ \land B = C) \to B - C = 0$
33	32	abs00bd	$⊢ (φ \land B = C) \to \|B - C\| = 0$
34	28 33	eqtrd	$⊢ (φ \land B = C) \to \|X - A\| = 0$
35	27 34	abs00d	$⊢ (φ \land B = C) \to X - A = 0$
36	23 25 35	subeq0d	$⊢ (φ \land B = C) \to X = A$
37	36	fvoveq1d	$⊢ (φ \land B = C) \to \|X - D\| = \|A - D\|$
38	11	adantr	$⊢ (φ \land B = C) \to \|X - D\| = \|E - F\|$
39	1 5	sseldd	$⊢ φ \to D \in ℂ$
40	39	adantr	$⊢ (φ \land B = C) \to D \in ℂ$
41	25 40	abssubd	$⊢ (φ \land B = C) \to \|A - D\| = \|D - A\|$
42	37 38 41	3eqtr3d	$⊢ (φ \land B = C) \to \|E - F\| = \|D - A\|$
43	42	oveq1d	$⊢ (φ \land B = C) \to {\|E - F\|}^{2} = {\|D - A\|}^{2}$
44	39 24	subcld	$⊢ φ \to D - A \in ℂ$
45	44	absvalsqd	$⊢ φ \to {\|D - A\|}^{2} = (D - A) \overline{D - A}$
46	45	adantr	$⊢ (φ \land B = C) \to {\|D - A\|}^{2} = (D - A) \overline{D - A}$
47	22 43 46	3eqtrd	$⊢ (φ \land B = C) \to Q = (D - A) \overline{D - A}$
48	47	oveq1d	$⊢ (φ \land B = C) \to Q - \overline{D} (D + A) = (D - A) \overline{D - A} - \overline{D} (D + A)$
49	32	oveq1d	$⊢ (φ \land B = C) \to (B - C) \overline{B - C} = 0 \cdot \overline{B - C}$
50	1 4	sseldd	$⊢ φ \to C \in ℂ$
51	29 50	subcld	$⊢ φ \to B - C \in ℂ$
52	51	cjcld	$⊢ φ \to \overline{B - C} \in ℂ$
53	52	adantr	$⊢ (φ \land B = C) \to \overline{B - C} \in ℂ$
54	53	mul02d	$⊢ (φ \land B = C) \to 0 \cdot \overline{B - C} = 0$
55	49 54	eqtrd	$⊢ (φ \land B = C) \to (B - C) \overline{B - C} = 0$
56	12 55	eqtrid	$⊢ (φ \land B = C) \to P = 0$
57	56	oveq1d	$⊢ (φ \land B = C) \to P - \overline{A} (D + A) = 0 - \overline{A} (D + A)$
58	48 57	oveq12d	$⊢ (φ \land B = C) \to Q - \overline{D} (D + A) - (P - \overline{A} (D + A)) = (D - A) \overline{D - A} - \overline{D} (D + A) - (0 - \overline{A} (D + A))$
59	44	adantr	$⊢ (φ \land B = C) \to D - A \in ℂ$
60	59	cjcld	$⊢ (φ \land B = C) \to \overline{D - A} \in ℂ$
61	59 60	mulcld	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} \in ℂ$
62	40	cjcld	$⊢ (φ \land B = C) \to \overline{D} \in ℂ$
63	40 25	addcld	$⊢ (φ \land B = C) \to D + A \in ℂ$
64	62 63	mulcld	$⊢ (φ \land B = C) \to \overline{D} (D + A) \in ℂ$
65		0cnd	$⊢ (φ \land B = C) \to 0 \in ℂ$
66	25	cjcld	$⊢ (φ \land B = C) \to \overline{A} \in ℂ$
67	66 63	mulcld	$⊢ (φ \land B = C) \to \overline{A} (D + A) \in ℂ$
68	61 64 65 67	sub4d	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} - \overline{D} (D + A) - (0 - \overline{A} (D + A)) = (D - A) \overline{D - A} - 0 - (\overline{D} (D + A) - \overline{A} (D + A))$
69	61	subid1d	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} - 0 = (D - A) \overline{D - A}$
70	39 24	cjsubd	$⊢ φ \to \overline{D - A} = \overline{D} - \overline{A}$
71	70	oveq1d	$⊢ φ \to \overline{D - A} (D + A) = (\overline{D} - \overline{A}) (D + A)$
72	44	cjcld	$⊢ φ \to \overline{D - A} \in ℂ$
73	39 24	addcld	$⊢ φ \to D + A \in ℂ$
74	72 73	mulcomd	$⊢ φ \to \overline{D - A} (D + A) = (D + A) \overline{D - A}$
75	39	cjcld	$⊢ φ \to \overline{D} \in ℂ$
76	24	cjcld	$⊢ φ \to \overline{A} \in ℂ$
77	75 76 73	subdird	$⊢ φ \to (\overline{D} - \overline{A}) (D + A) = \overline{D} (D + A) - \overline{A} (D + A)$
78	71 74 77	3eqtr3rd	$⊢ φ \to \overline{D} (D + A) - \overline{A} (D + A) = (D + A) \overline{D - A}$
79	78	adantr	$⊢ (φ \land B = C) \to \overline{D} (D + A) - \overline{A} (D + A) = (D + A) \overline{D - A}$
80	69 79	oveq12d	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} - 0 - (\overline{D} (D + A) - \overline{A} (D + A)) = (D - A) \overline{D - A} - (D + A) \overline{D - A}$
81	58 68 80	3eqtrd	$⊢ (φ \land B = C) \to Q - \overline{D} (D + A) - (P - \overline{A} (D + A)) = (D - A) \overline{D - A} - (D + A) \overline{D - A}$
82	59 63 60	subdird	$⊢ (φ \land B = C) \to (D - A - (D + A)) \overline{D - A} = (D - A) \overline{D - A} - (D + A) \overline{D - A}$
83	63 59	negsubdi2d	$⊢ (φ \land B = C) \to - (D + A - (D - A)) = D - A - (D + A)$
84	40 25 25	pnncand	$⊢ (φ \land B = C) \to D + A - (D - A) = A + A$
85	25	2timesd	$⊢ (φ \land B = C) \to 2 A = A + A$
86	84 85	eqtr4d	$⊢ (φ \land B = C) \to D + A - (D - A) = 2 A$
87	86	negeqd	$⊢ (φ \land B = C) \to - (D + A - (D - A)) = - 2 A$
88	83 87	eqtr3d	$⊢ (φ \land B = C) \to D - A - (D + A) = - 2 A$
89	88	oveq1d	$⊢ (φ \land B = C) \to (D - A - (D + A)) \overline{D - A} = (- 2 A) \overline{D - A}$
90	81 82 89	3eqtr2rd	$⊢ (φ \land B = C) \to (- 2 A) \overline{D - A} = Q - \overline{D} (D + A) - (P - \overline{A} (D + A))$
91	70	adantr	$⊢ (φ \land B = C) \to \overline{D - A} = \overline{D} - \overline{A}$
92	90 91	oveq12d	$⊢ (φ \land B = C) \to \frac{(- 2 A) \overline{D - A}}{\overline{D - A}} = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
93		2cnd	$⊢ (φ \land B = C) \to 2 \in ℂ$
94	93 25	mulcld	$⊢ (φ \land B = C) \to 2 A \in ℂ$
95	94	negcld	$⊢ (φ \land B = C) \to - 2 A \in ℂ$
96	9	necomd	$⊢ φ \to D \neq A$
97	39 24 96	subne0d	$⊢ φ \to D - A \neq 0$
98	44 97	cjne0d	$⊢ φ \to \overline{D - A} \neq 0$
99	98	adantr	$⊢ (φ \land B = C) \to \overline{D - A} \neq 0$
100	95 60 99	divcan4d	$⊢ (φ \land B = C) \to \frac{(- 2 A) \overline{D - A}}{\overline{D - A}} = - 2 A$
101	16 92 100	3eqtr2d	$⊢ (φ \land B = C) \to M = - 2 A$
102	101	oveq1d	$⊢ (φ \land B = C) \to M X = (- 2 A) X$
103	94 23	mulneg1d	$⊢ (φ \land B = C) \to (- 2 A) X = - 2 A X$
104	93 25 23	mulassd	$⊢ (φ \land B = C) \to 2 A X = 2 A X$
105	25 23	mulcomd	$⊢ (φ \land B = C) \to A X = X A$
106	105	oveq2d	$⊢ (φ \land B = C) \to 2 A X = 2 X A$
107	104 106	eqtrd	$⊢ (φ \land B = C) \to 2 A X = 2 X A$
108	107	negeqd	$⊢ (φ \land B = C) \to - 2 A X = - 2 X A$
109	102 103 108	3eqtrd	$⊢ (φ \land B = C) \to M X = - 2 X A$
110	25	sqcld	$⊢ (φ \land B = C) \to A^{2} \in ℂ$
111	56	oveq1d	$⊢ (φ \land B = C) \to P D = 0 \cdot D$
112	40	mul02d	$⊢ (φ \land B = C) \to 0 \cdot D = 0$
113	111 112	eqtrd	$⊢ (φ \land B = C) \to P D = 0$
114	113	oveq2d	$⊢ (φ \land B = C) \to \overline{A} D A - P D = \overline{A} D A - 0$
115	40 25	mulcld	$⊢ (φ \land B = C) \to D A \in ℂ$
116	66 115	mulcld	$⊢ (φ \land B = C) \to \overline{A} D A \in ℂ$
117	116	subid1d	$⊢ (φ \land B = C) \to \overline{A} D A - 0 = \overline{A} D A$
118	114 117	eqtrd	$⊢ (φ \land B = C) \to \overline{A} D A - P D = \overline{A} D A$
119	47	oveq1d	$⊢ (φ \land B = C) \to Q A = (D - A) \overline{D - A} A$
120	119	oveq2d	$⊢ (φ \land B = C) \to \overline{D} D A - Q A = \overline{D} D A - (D - A) \overline{D - A} A$
121	118 120	oveq12d	$⊢ (φ \land B = C) \to \overline{A} D A - P D - (\overline{D} D A - Q A) = \overline{A} D A - (\overline{D} D A - (D - A) \overline{D - A} A)$
122	62 115	mulcld	$⊢ (φ \land B = C) \to \overline{D} D A \in ℂ$
123	61 25	mulcld	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} A \in ℂ$
124	116 122 123	subsubd	$⊢ (φ \land B = C) \to \overline{A} D A - (\overline{D} D A - (D - A) \overline{D - A} A) = \overline{A} D A - \overline{D} D A + (D - A) \overline{D - A} A$
125	70	negeqd	$⊢ φ \to - \overline{D - A} = - (\overline{D} - \overline{A})$
126	75 76	negsubdi2d	$⊢ φ \to - (\overline{D} - \overline{A}) = \overline{A} - \overline{D}$
127	125 126	eqtr2d	$⊢ φ \to \overline{A} - \overline{D} = - \overline{D - A}$
128	127	oveq1d	$⊢ φ \to (\overline{A} - \overline{D}) D A = (- \overline{D - A}) D A$
129	39 24	mulcld	$⊢ φ \to D A \in ℂ$
130	76 75 129	subdird	$⊢ φ \to (\overline{A} - \overline{D}) D A = \overline{A} D A - \overline{D} D A$
131	72 129	mulcomd	$⊢ φ \to \overline{D - A} D A = D A \overline{D - A}$
132	131	negeqd	$⊢ φ \to - \overline{D - A} D A = - D A \overline{D - A}$
133	72 129	mulneg1d	$⊢ φ \to (- \overline{D - A}) D A = - \overline{D - A} D A$
134	129 72	mulneg1d	$⊢ φ \to (- D A) \overline{D - A} = - D A \overline{D - A}$
135	132 133 134	3eqtr4d	$⊢ φ \to (- \overline{D - A}) D A = (- D A) \overline{D - A}$
136	128 130 135	3eqtr3d	$⊢ φ \to \overline{A} D A - \overline{D} D A = (- D A) \overline{D - A}$
137	136	adantr	$⊢ (φ \land B = C) \to \overline{A} D A - \overline{D} D A = (- D A) \overline{D - A}$
138	59 60 25	mul32d	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} A = (D - A) A \overline{D - A}$
139	40 25 25	subdird	$⊢ (φ \land B = C) \to (D - A) A = D A - A A$
140	25	sqvald	$⊢ (φ \land B = C) \to A^{2} = A A$
141	140	oveq2d	$⊢ (φ \land B = C) \to D A - A^{2} = D A - A A$
142	139 141	eqtr4d	$⊢ (φ \land B = C) \to (D - A) A = D A - A^{2}$
143	142	oveq1d	$⊢ (φ \land B = C) \to (D - A) A \overline{D - A} = (D A - A^{2}) \overline{D - A}$
144	138 143	eqtrd	$⊢ (φ \land B = C) \to (D - A) \overline{D - A} A = (D A - A^{2}) \overline{D - A}$
145	137 144	oveq12d	$⊢ (φ \land B = C) \to \overline{A} D A - \overline{D} D A + (D - A) \overline{D - A} A = (- D A) \overline{D - A} + (D A - A^{2}) \overline{D - A}$
146	115	negcld	$⊢ (φ \land B = C) \to - D A \in ℂ$
147	115 110	subcld	$⊢ (φ \land B = C) \to D A - A^{2} \in ℂ$
148	146 147 60	adddird	$⊢ (φ \land B = C) \to ((- D A) + D A - A^{2}) \overline{D - A} = (- D A) \overline{D - A} + (D A - A^{2}) \overline{D - A}$
149	115	subidd	$⊢ (φ \land B = C) \to D A - D A = 0$
150	149	oveq1d	$⊢ (φ \land B = C) \to D A - D A - A^{2} = 0 - A^{2}$
151	146 147	addcomd	$⊢ (φ \land B = C) \to (- D A) + D A - A^{2} = D A - A^{2} + (- D A)$
152	147 115	negsubd	$⊢ (φ \land B = C) \to D A - A^{2} + (- D A) = D A - A^{2} - D A$
153	115 110 115	sub32d	$⊢ (φ \land B = C) \to D A - A^{2} - D A = D A - D A - A^{2}$
154	151 152 153	3eqtrd	$⊢ (φ \land B = C) \to (- D A) + D A - A^{2} = D A - D A - A^{2}$
155		df-neg	$⊢ - A^{2} = 0 - A^{2}$
156	155	a1i	$⊢ (φ \land B = C) \to - A^{2} = 0 - A^{2}$
157	150 154 156	3eqtr4d	$⊢ (φ \land B = C) \to (- D A) + D A - A^{2} = - A^{2}$
158	157	oveq1d	$⊢ (φ \land B = C) \to ((- D A) + D A - A^{2}) \overline{D - A} = (- A^{2}) \overline{D - A}$
159	145 148 158	3eqtr2d	$⊢ (φ \land B = C) \to \overline{A} D A - \overline{D} D A + (D - A) \overline{D - A} A = (- A^{2}) \overline{D - A}$
160	121 124 159	3eqtrd	$⊢ (φ \land B = C) \to \overline{A} D A - P D - (\overline{D} D A - Q A) = (- A^{2}) \overline{D - A}$
161	91	eqcomd	$⊢ (φ \land B = C) \to \overline{D} - \overline{A} = \overline{D - A}$
162	160 161	oveq12d	$⊢ (φ \land B = C) \to \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = \frac{(- A^{2}) \overline{D - A}}{\overline{D - A}}$
163	110	negcld	$⊢ (φ \land B = C) \to - A^{2} \in ℂ$
164	163 60 99	divcan4d	$⊢ (φ \land B = C) \to \frac{(- A^{2}) \overline{D - A}}{\overline{D - A}} = - A^{2}$
165	162 164	eqtr2d	$⊢ (φ \land B = C) \to - A^{2} = \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}$
166	110 165	negcon1ad	$⊢ (φ \land B = C) \to - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = A^{2}$
167	15 166	eqtrid	$⊢ (φ \land B = C) \to N = A^{2}$
168	109 167	oveq12d	$⊢ (φ \land B = C) \to M X + N = - 2 X A + A^{2}$
169	168	oveq2d	$⊢ (φ \land B = C) \to X^{2} + M X + N = X^{2} + (- 2 X A) + A^{2}$
170	23	sqcld	$⊢ (φ \land B = C) \to X^{2} \in ℂ$
171	23 25	mulcld	$⊢ (φ \land B = C) \to X A \in ℂ$
172	93 171	mulcld	$⊢ (φ \land B = C) \to 2 X A \in ℂ$
173	172	negcld	$⊢ (φ \land B = C) \to - 2 X A \in ℂ$
174	170 173 110	addassd	$⊢ (φ \land B = C) \to X^{2} + (- 2 X A) + A^{2} = X^{2} + (- 2 X A) + A^{2}$
175	170 172	negsubd	$⊢ (φ \land B = C) \to X^{2} + (- 2 X A) = X^{2} - 2 X A$
176	175	oveq1d	$⊢ (φ \land B = C) \to X^{2} + (- 2 X A) + A^{2} = X^{2} - 2 X A + A^{2}$
177	169 174 176	3eqtr2d	$⊢ (φ \land B = C) \to X^{2} + M X + N = X^{2} - 2 X A + A^{2}$
178		binom2sub	$⊢ (X \in ℂ \land A \in ℂ) \to {(X - A)}^{2} = X^{2} - 2 X A + A^{2}$
179	23 25 178	syl2anc	$⊢ (φ \land B = C) \to {(X - A)}^{2} = X^{2} - 2 X A + A^{2}$
180	35	sq0id	$⊢ (φ \land B = C) \to {(X - A)}^{2} = 0$
181	177 179 180	3eqtr2d	$⊢ (φ \land B = C) \to X^{2} + M X + N = 0$
182	14	a1i	$⊢ (φ \land E = F) \to M = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
183	17	adantr	$⊢ (φ \land E = F) \to E \in ℂ$
184		simpr	$⊢ (φ \land E = F) \to E = F$
185	183 184	subeq0bd	$⊢ (φ \land E = F) \to E - F = 0$
186	185	oveq1d	$⊢ (φ \land E = F) \to (E - F) \overline{E - F} = 0 \cdot \overline{E - F}$
187	19	cjcld	$⊢ φ \to \overline{E - F} \in ℂ$
188	187	adantr	$⊢ (φ \land E = F) \to \overline{E - F} \in ℂ$
189	188	mul02d	$⊢ (φ \land E = F) \to 0 \cdot \overline{E - F} = 0$
190	186 189	eqtrd	$⊢ (φ \land E = F) \to (E - F) \overline{E - F} = 0$
191	13 190	eqtrid	$⊢ (φ \land E = F) \to Q = 0$
192	191	oveq1d	$⊢ (φ \land E = F) \to Q - \overline{D} (D + A) = 0 - \overline{D} (D + A)$
193	51	adantr	$⊢ (φ \land E = F) \to B - C \in ℂ$
194	193	absvalsqd	$⊢ (φ \land E = F) \to {\|B - C\|}^{2} = (B - C) \overline{B - C}$
195	12 194	eqtr4id	$⊢ (φ \land E = F) \to P = {\|B - C\|}^{2}$
196	10	adantr	$⊢ (φ \land E = F) \to \|X - A\| = \|B - C\|$
197	8	adantr	$⊢ (φ \land E = F) \to X \in ℂ$
198	39	adantr	$⊢ (φ \land E = F) \to D \in ℂ$
199	8 39	subcld	$⊢ φ \to X - D \in ℂ$
200	199	adantr	$⊢ (φ \land E = F) \to X - D \in ℂ$
201	11	adantr	$⊢ (φ \land E = F) \to \|X - D\| = \|E - F\|$
202	185	abs00bd	$⊢ (φ \land E = F) \to \|E - F\| = 0$
203	201 202	eqtrd	$⊢ (φ \land E = F) \to \|X - D\| = 0$
204	200 203	abs00d	$⊢ (φ \land E = F) \to X - D = 0$
205	197 198 204	subeq0d	$⊢ (φ \land E = F) \to X = D$
206	205	fvoveq1d	$⊢ (φ \land E = F) \to \|X - A\| = \|D - A\|$
207	196 206	eqtr3d	$⊢ (φ \land E = F) \to \|B - C\| = \|D - A\|$
208	207	oveq1d	$⊢ (φ \land E = F) \to {\|B - C\|}^{2} = {\|D - A\|}^{2}$
209	45	adantr	$⊢ (φ \land E = F) \to {\|D - A\|}^{2} = (D - A) \overline{D - A}$
210	195 208 209	3eqtrd	$⊢ (φ \land E = F) \to P = (D - A) \overline{D - A}$
211	210	oveq1d	$⊢ (φ \land E = F) \to P - \overline{A} (D + A) = (D - A) \overline{D - A} - \overline{A} (D + A)$
212	192 211	oveq12d	$⊢ (φ \land E = F) \to Q - \overline{D} (D + A) - (P - \overline{A} (D + A)) = 0 - \overline{D} (D + A) - ((D - A) \overline{D - A} - \overline{A} (D + A))$
213		0cnd	$⊢ (φ \land E = F) \to 0 \in ℂ$
214	198	cjcld	$⊢ (φ \land E = F) \to \overline{D} \in ℂ$
215	24	adantr	$⊢ (φ \land E = F) \to A \in ℂ$
216	198 215	addcld	$⊢ (φ \land E = F) \to D + A \in ℂ$
217	214 216	mulcld	$⊢ (φ \land E = F) \to \overline{D} (D + A) \in ℂ$
218	44	adantr	$⊢ (φ \land E = F) \to D - A \in ℂ$
219	218	cjcld	$⊢ (φ \land E = F) \to \overline{D - A} \in ℂ$
220	218 219	mulcld	$⊢ (φ \land E = F) \to (D - A) \overline{D - A} \in ℂ$
221	215	cjcld	$⊢ (φ \land E = F) \to \overline{A} \in ℂ$
222	221 216	mulcld	$⊢ (φ \land E = F) \to \overline{A} (D + A) \in ℂ$
223	213 217 220 222	sub4d	$⊢ (φ \land E = F) \to 0 - \overline{D} (D + A) - ((D - A) \overline{D - A} - \overline{A} (D + A)) = 0 - (D - A) \overline{D - A} - (\overline{D} (D + A) - \overline{A} (D + A))$
224	218 219	mulneg1d	$⊢ (φ \land E = F) \to (- (D - A)) \overline{D - A} = - (D - A) \overline{D - A}$
225	198 215	negsubdi2d	$⊢ (φ \land E = F) \to - (D - A) = A - D$
226	225	oveq1d	$⊢ (φ \land E = F) \to (- (D - A)) \overline{D - A} = (A - D) \overline{D - A}$
227		df-neg	$⊢ - (D - A) \overline{D - A} = 0 - (D - A) \overline{D - A}$
228	227	a1i	$⊢ (φ \land E = F) \to - (D - A) \overline{D - A} = 0 - (D - A) \overline{D - A}$
229	224 226 228	3eqtr3rd	$⊢ (φ \land E = F) \to 0 - (D - A) \overline{D - A} = (A - D) \overline{D - A}$
230	78	adantr	$⊢ (φ \land E = F) \to \overline{D} (D + A) - \overline{A} (D + A) = (D + A) \overline{D - A}$
231	229 230	oveq12d	$⊢ (φ \land E = F) \to 0 - (D - A) \overline{D - A} - (\overline{D} (D + A) - \overline{A} (D + A)) = (A - D) \overline{D - A} - (D + A) \overline{D - A}$
232	212 223 231	3eqtrd	$⊢ (φ \land E = F) \to Q - \overline{D} (D + A) - (P - \overline{A} (D + A)) = (A - D) \overline{D - A} - (D + A) \overline{D - A}$
233	215 198	subcld	$⊢ (φ \land E = F) \to A - D \in ℂ$
234	233 216 219	subdird	$⊢ (φ \land E = F) \to (A - D - (D + A)) \overline{D - A} = (A - D) \overline{D - A} - (D + A) \overline{D - A}$
235	216 233	negsubdi2d	$⊢ (φ \land E = F) \to - (D + A - (A - D)) = A - D - (D + A)$
236	198	2timesd	$⊢ (φ \land E = F) \to 2 D = D + D$
237	215 198 198	pnncand	$⊢ (φ \land E = F) \to A + D - (A - D) = D + D$
238	215 198	addcomd	$⊢ (φ \land E = F) \to A + D = D + A$
239	238	oveq1d	$⊢ (φ \land E = F) \to A + D - (A - D) = D + A - (A - D)$
240	236 237 239	3eqtr2rd	$⊢ (φ \land E = F) \to D + A - (A - D) = 2 D$
241	240	negeqd	$⊢ (φ \land E = F) \to - (D + A - (A - D)) = - 2 D$
242	235 241	eqtr3d	$⊢ (φ \land E = F) \to A - D - (D + A) = - 2 D$
243	242	oveq1d	$⊢ (φ \land E = F) \to (A - D - (D + A)) \overline{D - A} = (- 2 D) \overline{D - A}$
244	232 234 243	3eqtr2rd	$⊢ (φ \land E = F) \to (- 2 D) \overline{D - A} = Q - \overline{D} (D + A) - (P - \overline{A} (D + A))$
245	70	adantr	$⊢ (φ \land E = F) \to \overline{D - A} = \overline{D} - \overline{A}$
246	244 245	oveq12d	$⊢ (φ \land E = F) \to \frac{(- 2 D) \overline{D - A}}{\overline{D - A}} = \frac{Q - \overline{D} (D + A) - (P - \overline{A} (D + A))}{\overline{D} - \overline{A}}$
247		2cnd	$⊢ (φ \land E = F) \to 2 \in ℂ$
248	247 198	mulcld	$⊢ (φ \land E = F) \to 2 D \in ℂ$
249	248	negcld	$⊢ (φ \land E = F) \to - 2 D \in ℂ$
250	98	adantr	$⊢ (φ \land E = F) \to \overline{D - A} \neq 0$
251	249 219 250	divcan4d	$⊢ (φ \land E = F) \to \frac{(- 2 D) \overline{D - A}}{\overline{D - A}} = - 2 D$
252	182 246 251	3eqtr2d	$⊢ (φ \land E = F) \to M = - 2 D$
253	252	oveq1d	$⊢ (φ \land E = F) \to M X = (- 2 D) X$
254	248 197	mulneg1d	$⊢ (φ \land E = F) \to (- 2 D) X = - 2 D X$
255	247 198 197	mulassd	$⊢ (φ \land E = F) \to 2 D X = 2 D X$
256	198 197	mulcomd	$⊢ (φ \land E = F) \to D X = X D$
257	256	oveq2d	$⊢ (φ \land E = F) \to 2 D X = 2 X D$
258	255 257	eqtrd	$⊢ (φ \land E = F) \to 2 D X = 2 X D$
259	258	negeqd	$⊢ (φ \land E = F) \to - 2 D X = - 2 X D$
260	253 254 259	3eqtrd	$⊢ (φ \land E = F) \to M X = - 2 X D$
261	198	sqcld	$⊢ (φ \land E = F) \to D^{2} \in ℂ$
262	210	oveq1d	$⊢ (φ \land E = F) \to P D = (D - A) \overline{D - A} D$
263	262	oveq2d	$⊢ (φ \land E = F) \to \overline{A} D A - P D = \overline{A} D A - (D - A) \overline{D - A} D$
264	191	oveq1d	$⊢ (φ \land E = F) \to Q A = 0 \cdot A$
265	215	mul02d	$⊢ (φ \land E = F) \to 0 \cdot A = 0$
266	264 265	eqtrd	$⊢ (φ \land E = F) \to Q A = 0$
267	266	oveq2d	$⊢ (φ \land E = F) \to \overline{D} D A - Q A = \overline{D} D A - 0$
268	198 215	mulcld	$⊢ (φ \land E = F) \to D A \in ℂ$
269	214 268	mulcld	$⊢ (φ \land E = F) \to \overline{D} D A \in ℂ$
270	269	subid1d	$⊢ (φ \land E = F) \to \overline{D} D A - 0 = \overline{D} D A$
271	267 270	eqtrd	$⊢ (φ \land E = F) \to \overline{D} D A - Q A = \overline{D} D A$
272	263 271	oveq12d	$⊢ (φ \land E = F) \to \overline{A} D A - P D - (\overline{D} D A - Q A) = \overline{A} D A - (D - A) \overline{D - A} D - \overline{D} D A$
273	221 268	mulcld	$⊢ (φ \land E = F) \to \overline{A} D A \in ℂ$
274	220 198	mulcld	$⊢ (φ \land E = F) \to (D - A) \overline{D - A} D \in ℂ$
275	273 274 269	sub32d	$⊢ (φ \land E = F) \to \overline{A} D A - (D - A) \overline{D - A} D - \overline{D} D A = \overline{A} D A - \overline{D} D A - (D - A) \overline{D - A} D$
276	136	adantr	$⊢ (φ \land E = F) \to \overline{A} D A - \overline{D} D A = (- D A) \overline{D - A}$
277	218 219 198	mul32d	$⊢ (φ \land E = F) \to (D - A) \overline{D - A} D = (D - A) D \overline{D - A}$
278	198 215 198	subdird	$⊢ (φ \land E = F) \to (D - A) D = D D - A D$
279	198	sqvald	$⊢ (φ \land E = F) \to D^{2} = D D$
280	198 215	mulcomd	$⊢ (φ \land E = F) \to D A = A D$
281	279 280	oveq12d	$⊢ (φ \land E = F) \to D^{2} - D A = D D - A D$
282	278 281	eqtr4d	$⊢ (φ \land E = F) \to (D - A) D = D^{2} - D A$
283	282	oveq1d	$⊢ (φ \land E = F) \to (D - A) D \overline{D - A} = (D^{2} - D A) \overline{D - A}$
284	277 283	eqtrd	$⊢ (φ \land E = F) \to (D - A) \overline{D - A} D = (D^{2} - D A) \overline{D - A}$
285	276 284	oveq12d	$⊢ (φ \land E = F) \to \overline{A} D A - \overline{D} D A - (D - A) \overline{D - A} D = (- D A) \overline{D - A} - (D^{2} - D A) \overline{D - A}$
286	268	negcld	$⊢ (φ \land E = F) \to - D A \in ℂ$
287	261 268	subcld	$⊢ (φ \land E = F) \to D^{2} - D A \in ℂ$
288	286 287 219	subdird	$⊢ (φ \land E = F) \to (- D A - (D^{2} - D A)) \overline{D - A} = (- D A) \overline{D - A} - (D^{2} - D A) \overline{D - A}$
289	286 268	addcomd	$⊢ (φ \land E = F) \to - D A + D A = D A + (- D A)$
290	268 268	negsubd	$⊢ (φ \land E = F) \to D A + (- D A) = D A - D A$
291	268	subidd	$⊢ (φ \land E = F) \to D A - D A = 0$
292	289 290 291	3eqtrd	$⊢ (φ \land E = F) \to - D A + D A = 0$
293	292	oveq1d	$⊢ (φ \land E = F) \to (- D A) + D A - D^{2} = 0 - D^{2}$
294	286 261 268	subsub3d	$⊢ (φ \land E = F) \to - D A - (D^{2} - D A) = (- D A) + D A - D^{2}$
295		df-neg	$⊢ - D^{2} = 0 - D^{2}$
296	295	a1i	$⊢ (φ \land E = F) \to - D^{2} = 0 - D^{2}$
297	293 294 296	3eqtr4d	$⊢ (φ \land E = F) \to - D A - (D^{2} - D A) = - D^{2}$
298	297	oveq1d	$⊢ (φ \land E = F) \to (- D A - (D^{2} - D A)) \overline{D - A} = (- D^{2}) \overline{D - A}$
299	285 288 298	3eqtr2d	$⊢ (φ \land E = F) \to \overline{A} D A - \overline{D} D A - (D - A) \overline{D - A} D = (- D^{2}) \overline{D - A}$
300	272 275 299	3eqtrd	$⊢ (φ \land E = F) \to \overline{A} D A - P D - (\overline{D} D A - Q A) = (- D^{2}) \overline{D - A}$
301	245	eqcomd	$⊢ (φ \land E = F) \to \overline{D} - \overline{A} = \overline{D - A}$
302	300 301	oveq12d	$⊢ (φ \land E = F) \to \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = \frac{(- D^{2}) \overline{D - A}}{\overline{D - A}}$
303	261	negcld	$⊢ (φ \land E = F) \to - D^{2} \in ℂ$
304	303 219 250	divcan4d	$⊢ (φ \land E = F) \to \frac{(- D^{2}) \overline{D - A}}{\overline{D - A}} = - D^{2}$
305	302 304	eqtr2d	$⊢ (φ \land E = F) \to - D^{2} = \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}}$
306	261 305	negcon1ad	$⊢ (φ \land E = F) \to - \frac{\overline{A} D A - P D - (\overline{D} D A - Q A)}{\overline{D} - \overline{A}} = D^{2}$
307	15 306	eqtrid	$⊢ (φ \land E = F) \to N = D^{2}$
308	260 307	oveq12d	$⊢ (φ \land E = F) \to M X + N = - 2 X D + D^{2}$
309	308	oveq2d	$⊢ (φ \land E = F) \to X^{2} + M X + N = X^{2} + (- 2 X D) + D^{2}$
310	197	sqcld	$⊢ (φ \land E = F) \to X^{2} \in ℂ$
311	197 198	mulcld	$⊢ (φ \land E = F) \to X D \in ℂ$
312	247 311	mulcld	$⊢ (φ \land E = F) \to 2 X D \in ℂ$
313	312	negcld	$⊢ (φ \land E = F) \to - 2 X D \in ℂ$
314	310 313 261	addassd	$⊢ (φ \land E = F) \to X^{2} + (- 2 X D) + D^{2} = X^{2} + (- 2 X D) + D^{2}$
315	310 312	negsubd	$⊢ (φ \land E = F) \to X^{2} + (- 2 X D) = X^{2} - 2 X D$
316	315	oveq1d	$⊢ (φ \land E = F) \to X^{2} + (- 2 X D) + D^{2} = X^{2} - 2 X D + D^{2}$
317	309 314 316	3eqtr2d	$⊢ (φ \land E = F) \to X^{2} + M X + N = X^{2} - 2 X D + D^{2}$
318		binom2sub	$⊢ (X \in ℂ \land D \in ℂ) \to {(X - D)}^{2} = X^{2} - 2 X D + D^{2}$
319	197 198 318	syl2anc	$⊢ (φ \land E = F) \to {(X - D)}^{2} = X^{2} - 2 X D + D^{2}$
320	204	sq0id	$⊢ (φ \land E = F) \to {(X - D)}^{2} = 0$
321	317 319 320	3eqtr2d	$⊢ (φ \land E = F) \to X^{2} + M X + N = 0$
322	1	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to S \subseteq ℂ$
323	2	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to A \in S$
324	3	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to B \in S$
325	4	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to C \in S$
326	5	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to D \in S$
327	6	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to E \in S$
328	7	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to F \in S$
329	8	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to X \in ℂ$
330	9	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to A \neq D$
331	10	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to \|X - A\| = \|B - C\|$
332	11	adantr	$⊢ (φ \land (B \neq C \land E \neq F)) \to \|X - D\| = \|E - F\|$
333		simprl	$⊢ (φ \land (B \neq C \land E \neq F)) \to B \neq C$
334		simprr	$⊢ (φ \land (B \neq C \land E \neq F)) \to E \neq F$
335	322 323 324 325 326 327 328 329 330 331 332 12 13 14 15 333 334	constrrtcclem	$⊢ (φ \land (B \neq C \land E \neq F)) \to X^{2} + M X + N = 0$
336	181 321 335	pm2.61da2ne	$⊢ φ \to X^{2} + M X + N = 0$

Metamath Proof Explorer

Theorem constrrtcc

Proof