Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Constructible Numbers
constrrtlc2
Metamath Proof Explorer
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
⊢ ( 𝜑 → 𝑋 = 𝐴 )