Theorem constrlccl

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

	Ref	Expression
Hypotheses	constrlccl.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
	constrlccl.b	⊢ ( 𝜑 → 𝐵 ∈ Constr )
	constrlccl.c	⊢ ( 𝜑 → 𝐺 ∈ Constr )
	constrlccl.e	⊢ ( 𝜑 → 𝐸 ∈ Constr )
	constrlccl.f	⊢ ( 𝜑 → 𝐹 ∈ Constr )
	constrlccl.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	constrlccl.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	constrlccl.1	⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
	constrlccl.2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐺 ) ) = ( abs ‘ ( 𝐸 − 𝐹 ) ) )
Assertion	constrlccl	⊢ ( 𝜑 → 𝑋 ∈ Constr )

Proof

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