Metamath Proof Explorer


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 ( 𝜑𝑋 = 𝐴 )