Theorem constrllcl

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

	Ref	Expression
Hypotheses	constrllcl.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
	constrllcl.b	⊢ ( 𝜑 → 𝐵 ∈ Constr )
	constrllcl.c	⊢ ( 𝜑 → 𝐺 ∈ Constr )
	constrllcl.e	⊢ ( 𝜑 → 𝐷 ∈ Constr )
	constrllcl.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
	constrllcl.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
	constrllcl.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	constrllcl.1	⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
	constrllcl.2	⊢ ( 𝜑 → 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
	constrllcl.3	⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 )
Assertion	constrllcl	⊢ ( 𝜑 → 𝑋 ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrllcl.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
2		constrllcl.b	⊢ ( 𝜑 → 𝐵 ∈ Constr )
3		constrllcl.c	⊢ ( 𝜑 → 𝐺 ∈ Constr )
4		constrllcl.e	⊢ ( 𝜑 → 𝐷 ∈ Constr )
5		constrllcl.t	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
6		constrllcl.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
7		constrllcl.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
8		constrllcl.1	⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) )
9		constrllcl.2	⊢ ( 𝜑 → 𝑋 = ( 𝐺 + ( 𝑅 · ( 𝐷 − 𝐺 ) ) ) )
10		constrllcl.3	⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐺 ) ) ) ≠ 0 )
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	constrllcllem	⊢ ( 𝜑 → 𝑋 ∈ Constr )