Metamath Proof Explorer

Theorem constrlccl

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

Ref Expression
Hypotheses constrlccl.a ⊢ φ → A ∈ Constr
constrlccl.b ⊢ φ → B ∈ Constr
constrlccl.c ⊢ φ → G ∈ Constr
constrlccl.e ⊢ φ → E ∈ Constr
constrlccl.f ⊢ φ → F ∈ Constr
constrlccl.t ⊢ φ → T ∈ ℝ
constrlccl.x ⊢ φ → X ∈ ℂ
constrlccl.1 ⊢ φ → X = A + T ⁢ B − A
constrlccl.2 ⊢ φ → X − G = E − F
Assertion constrlccl ⊢ φ → X ∈ Constr

Proof

Step Hyp Ref Expression
1 constrlccl.a ⊢ φ → A ∈ Constr
2 constrlccl.b ⊢ φ → B ∈ Constr
3 constrlccl.c ⊢ φ → G ∈ Constr
4 constrlccl.e ⊢ φ → E ∈ Constr
5 constrlccl.f ⊢ φ → F ∈ Constr
6 constrlccl.t ⊢ φ → T ∈ ℝ
7 constrlccl.x ⊢ φ → X ∈ ℂ
8 constrlccl.1 ⊢ φ → X = A + T ⁢ B − A
9 constrlccl.2 ⊢ φ → X − G = E − F
10 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
11 10 1 2 3 4 5 6 7 8 9 constrlccllem ⊢ φ → X ∈ Constr