Theorem constrcccl

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

	Ref	Expression
Hypotheses	constrcccl.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
	constrcccl.b	⊢ ( 𝜑 → 𝐵 ∈ Constr )
	constrcccl.c	⊢ ( 𝜑 → 𝐶 ∈ Constr )
	constrcccl.d	⊢ ( 𝜑 → 𝐷 ∈ Constr )
	constrcccl.e	⊢ ( 𝜑 → 𝐸 ∈ Constr )
	constrcccl.f	⊢ ( 𝜑 → 𝐹 ∈ Constr )
	constrcccl.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	constrcccl.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
	constrcccl.2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
	constrcccl.3	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
Assertion	constrcccl	⊢ ( 𝜑 → 𝑋 ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrcccl.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
2		constrcccl.b	⊢ ( 𝜑 → 𝐵 ∈ Constr )
3		constrcccl.c	⊢ ( 𝜑 → 𝐶 ∈ Constr )
4		constrcccl.d	⊢ ( 𝜑 → 𝐷 ∈ Constr )
5		constrcccl.e	⊢ ( 𝜑 → 𝐸 ∈ Constr )
6		constrcccl.f	⊢ ( 𝜑 → 𝐹 ∈ Constr )
7		constrcccl.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
8		constrcccl.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
9		constrcccl.2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐴 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
10		constrcccl.3	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐷 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
11		constrcbvlem	⊢ rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
12	11 1 2 3 4 5 6 7 8 9 10	constrcccllem	⊢ ( 𝜑 → 𝑋 ∈ Constr )