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 φ S
constrrtlc.a φ A S
constrrtlc.b φ B S
constrrtlc.c φ C S
constrrtlc.e φ E S
constrrtlc.f φ F S
constrrtlc.t φ T
constrrtlc.1 φ X = A + T B A
constrrtlc.2 φ X C = E F
constrrtlc2.1 φ A = B
Assertion constrrtlc2 φ X = A

Proof

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