Theorem constrrtlc2

Description: In the construction of constructible numbers, line-circle intersections are one of the original points, in a degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	constrrtlc.s	$$⊢\phi \to S\subseteq ℂ$$
	constrrtlc.a	$$⊢\phi \to A\in S$$
	constrrtlc.b	$$⊢\phi \to B\in S$$
	constrrtlc.c	$$⊢\phi \to C\in S$$
	constrrtlc.e	$$⊢\phi \to E\in S$$
	constrrtlc.f	$$⊢\phi \to F\in S$$
	constrrtlc.t	$$⊢\phi \to T\in ℝ$$
	constrrtlc.1	$$⊢\phi \to X=A+T\left(B-A\right)$$
	constrrtlc.2	$$⊢\phi \to \left|X-C\right|=\left|E-F\right|$$
	constrrtlc2.1	$$⊢\phi \to A=B$$
Assertion	constrrtlc2	$$⊢\phi \to X=A$$

Proof

Step	Hyp	Ref	Expression
1		constrrtlc.s	$$⊢\phi \to S\subseteq ℂ$$
2		constrrtlc.a	$$⊢\phi \to A\in S$$
3		constrrtlc.b	$$⊢\phi \to B\in S$$
4		constrrtlc.c	$$⊢\phi \to C\in S$$
5		constrrtlc.e	$$⊢\phi \to E\in S$$
6		constrrtlc.f	$$⊢\phi \to F\in S$$
7		constrrtlc.t	$$⊢\phi \to T\in ℝ$$
8		constrrtlc.1	$$⊢\phi \to X=A+T\left(B-A\right)$$
9		constrrtlc.2	$$⊢\phi \to \left|X-C\right|=\left|E-F\right|$$
10		constrrtlc2.1	$$⊢\phi \to A=B$$
11	1 3	sseldd	$$⊢\phi \to B\in ℂ$$
12	10	eqcomd	$$⊢\phi \to B=A$$
13	11 12	subeq0bd	$$⊢\phi \to B-A=0$$
14	13	oveq2d	$$⊢\phi \to T\left(B-A\right)=T\cdot 0$$
15	7	recnd	$$⊢\phi \to T\in ℂ$$
16	15	mul01d	$$⊢\phi \to T\cdot 0=0$$
17	14 16	eqtrd	$$⊢\phi \to T\left(B-A\right)=0$$
18	17	oveq2d	$$⊢\phi \to A+T\left(B-A\right)=A+0$$
19	1 2	sseldd	$$⊢\phi \to A\in ℂ$$
20	19	addridd	$$⊢\phi \to A+0=A$$
21	8 18 20	3eqtrd	$$⊢\phi \to X=A$$