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	|- ( ph -> S C_ CC )
	constrrtlc.a	|- ( ph -> A e. S )
	constrrtlc.b	|- ( ph -> B e. S )
	constrrtlc.c	|- ( ph -> C e. S )
	constrrtlc.e	|- ( ph -> E e. S )
	constrrtlc.f	|- ( ph -> F e. S )
	constrrtlc.t	|- ( ph -> T e. RR )
	constrrtlc.1	|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
	constrrtlc.2	|- ( ph -> ( abs ` ( X - C ) ) = ( abs ` ( E - F ) ) )
	constrrtlc2.1	|- ( ph -> A = B )
Assertion	constrrtlc2	|- ( ph -> X = A )

Proof

Step	Hyp	Ref	Expression
1		constrrtlc.s	|- ( ph -> S C_ CC )
2		constrrtlc.a	|- ( ph -> A e. S )
3		constrrtlc.b	|- ( ph -> B e. S )
4		constrrtlc.c	|- ( ph -> C e. S )
5		constrrtlc.e	|- ( ph -> E e. S )
6		constrrtlc.f	|- ( ph -> F e. S )
7		constrrtlc.t	|- ( ph -> T e. RR )
8		constrrtlc.1	|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
9		constrrtlc.2	|- ( ph -> ( abs ` ( X - C ) ) = ( abs ` ( E - F ) ) )
10		constrrtlc2.1	|- ( ph -> A = B )
11	1 3	sseldd	|- ( ph -> B e. CC )
12	10	eqcomd	|- ( ph -> B = A )
13	11 12	subeq0bd	|- ( ph -> ( B - A ) = 0 )
14	13	oveq2d	|- ( ph -> ( T x. ( B - A ) ) = ( T x. 0 ) )
15	7	recnd	|- ( ph -> T e. CC )
16	15	mul01d	|- ( ph -> ( T x. 0 ) = 0 )
17	14 16	eqtrd	|- ( ph -> ( T x. ( B - A ) ) = 0 )
18	17	oveq2d	|- ( ph -> ( A + ( T x. ( B - A ) ) ) = ( A + 0 ) )
19	1 2	sseldd	|- ( ph -> A e. CC )
20	19	addridd	|- ( ph -> ( A + 0 ) = A )
21	8 18 20	3eqtrd	|- ( ph -> X = A )