Theorem constrcjcl

Description: Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypothesis	constrcjcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion	constrcjcl	⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		constrcbvlem	⊢ rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
3	2	isconstr	⊢ ( 𝑋 ∈ Constr ↔ ∃ 𝑛 ∈ ω 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
4	1 3	sylib	⊢ ( 𝜑 → ∃ 𝑛 ∈ ω 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
5		nnon	⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
6	5	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) ) → 𝑛 ∈ On )
7		simpr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) ) → 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
8	2 6 7	constrconj	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ω ) ∧ 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) ) → ( ∗ ‘ 𝑋 ) ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
9	8	ex	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ω ) → ( 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) → ( ∗ ‘ 𝑋 ) ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) ) )
10	9	reximdva	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ω 𝑋 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) → ∃ 𝑛 ∈ ω ( ∗ ‘ 𝑋 ) ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) ) )
11	4 10	mpd	⊢ ( 𝜑 → ∃ 𝑛 ∈ ω ( ∗ ‘ 𝑋 ) ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
12	2	isconstr	⊢ ( ( ∗ ‘ 𝑋 ) ∈ Constr ↔ ∃ 𝑛 ∈ ω ( ∗ ‘ 𝑋 ) ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
13	11 12	sylibr	⊢ ( 𝜑 → ( ∗ ‘ 𝑋 ) ∈ Constr )