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	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	constrrtlc.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	constrrtlc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	constrrtlc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	constrrtlc.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
	constrrtlc.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
	constrrtlc.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	constrrtlc.1	⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
	constrrtlc.2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
	constrrtlc2.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	constrrtlc2	⊢ ( 𝜑 → 𝑋 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		constrrtlc.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2		constrrtlc.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
3		constrrtlc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
4		constrrtlc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
5		constrrtlc.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
6		constrrtlc.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
7		constrrtlc.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
8		constrrtlc.1	⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
9		constrrtlc.2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
10		constrrtlc2.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
11	1 3	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
12	10	eqcomd	⊢ ( 𝜑 → 𝐵 = 𝐴 )
13	11 12	subeq0bd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = 0 )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝑇 · ( 𝐵 − 𝐴 ) ) = ( 𝑇 · 0 ) )
15	7	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
16	15	mul01d	⊢ ( 𝜑 → ( 𝑇 · 0 ) = 0 )
17	14 16	eqtrd	⊢ ( 𝜑 → ( 𝑇 · ( 𝐵 − 𝐴 ) ) = 0 )
18	17	oveq2d	⊢ ( 𝜑 → ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( 𝐴 + 0 ) )
19	1 2	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
20	19	addridd	⊢ ( 𝜑 → ( 𝐴 + 0 ) = 𝐴 )
21	8 18 20	3eqtrd	⊢ ( 𝜑 → 𝑋 = 𝐴 )