Metamath Proof Explorer

Theorem constrcccl

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

Ref Expression
Hypotheses constrcccl.a ⊢ φ → A ∈ Constr
constrcccl.b ⊢ φ → B ∈ Constr
constrcccl.c ⊢ φ → C ∈ Constr
constrcccl.d ⊢ φ → D ∈ Constr
constrcccl.e ⊢ φ → E ∈ Constr
constrcccl.f ⊢ φ → F ∈ Constr
constrcccl.x ⊢ φ → X ∈ ℂ
constrcccl.1 ⊢ φ → A ≠ D
constrcccl.2 ⊢ φ → X − A = B − C
constrcccl.3 ⊢ φ → X − D = E − F
Assertion constrcccl ⊢ φ → X ∈ Constr

Proof

Step Hyp Ref Expression
1 constrcccl.a ⊢ φ → A ∈ Constr
2 constrcccl.b ⊢ φ → B ∈ Constr
3 constrcccl.c ⊢ φ → C ∈ Constr
4 constrcccl.d ⊢ φ → D ∈ Constr
5 constrcccl.e ⊢ φ → E ∈ Constr
6 constrcccl.f ⊢ φ → F ∈ Constr
7 constrcccl.x ⊢ φ → X ∈ ℂ
8 constrcccl.1 ⊢ φ → A ≠ D
9 constrcccl.2 ⊢ φ → X − A = B − C
10 constrcccl.3 ⊢ φ → X − D = E − F
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 constrcccllem ⊢ φ → X ∈ Constr