Metamath Proof Explorer

Theorem constrllcl

Description: Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constrllcl.a ⊢ φ → A ∈ Constr
constrllcl.b ⊢ φ → B ∈ Constr
constrllcl.c ⊢ φ → G ∈ Constr
constrllcl.e ⊢ φ → D ∈ Constr
constrllcl.t ⊢ φ → T ∈ ℝ
constrllcl.r ⊢ φ → R ∈ ℝ
constrllcl.x ⊢ φ → X ∈ ℂ
constrllcl.1 ⊢ φ → X = A + T ⁢ B − A
constrllcl.2 ⊢ φ → X = G + R ⁢ D − G
constrllcl.3 ⊢ φ → ℑ ⁡ B − A ‾ ⁢ D − G ≠ 0
Assertion constrllcl ⊢ φ → X ∈ Constr

Proof

Step Hyp Ref Expression
1 constrllcl.a ⊢ φ → A ∈ Constr
2 constrllcl.b ⊢ φ → B ∈ Constr
3 constrllcl.c ⊢ φ → G ∈ Constr
4 constrllcl.e ⊢ φ → D ∈ Constr
5 constrllcl.t ⊢ φ → T ∈ ℝ
6 constrllcl.r ⊢ φ → R ∈ ℝ
7 constrllcl.x ⊢ φ → X ∈ ℂ
8 constrllcl.1 ⊢ φ → X = A + T ⁢ B − A
9 constrllcl.2 ⊢ φ → X = G + R ⁢ D − G
10 constrllcl.3 ⊢ φ → ℑ ⁡ B − A ‾ ⁢ D − G ≠ 0
11 constrcbvlem ⊢ rec ⁡ z ∈ V ⟼ y ∈ ℂ | ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ l ∈ z ∃ o ∈ ℝ ∃ p ∈ ℝ y = i + o ⁢ j − i ∧ y = k + p ⁢ l − k ∧ ℑ ⁡ j − i ‾ ⁢ l − k ≠ 0 ∨ ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ m ∈ z ∃ q ∈ z ∃ o ∈ ℝ y = i + o ⁢ j − i ∧ y − k = m − q ∨ ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ l ∈ z ∃ m ∈ z ∃ q ∈ z i ≠ l ∧ y − i = j − k ∧ y − l = m − q 0 1 = rec ⁡ s ∈ V ⟼ x ∈ ℂ | ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ t ∈ ℝ ∃ r ∈ ℝ x = a + t ⁢ b − a ∧ x = c + r ⁢ d − c ∧ ℑ ⁡ b − a ‾ ⁢ d − c ≠ 0 ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ e ∈ s ∃ f ∈ s ∃ t ∈ ℝ x = a + t ⁢ b − a ∧ x − c = e − f ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ e ∈ s ∃ f ∈ s a ≠ d ∧ x − a = b − c ∧ x − d = e − f 0 1
12 11 1 2 3 4 5 6 7 8 9 10 constrllcllem ⊢ φ → X ∈ Constr