Theorem constrdircl

Description: Constructible numbers are closed under taking the point on the unit circle having the same argument. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	constrdircl.x	⊢ ( 𝜑 → 𝑋 ∈ Constr )
	constrdircl.1	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	constrdircl	⊢ ( 𝜑 → ( 𝑋 / ( abs ‘ 𝑋 ) ) ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrdircl.x	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		constrdircl.1	⊢ ( 𝜑 → 𝑋 ≠ 0 )
3		0nn0	⊢ 0 ∈ ℕ0
4	3	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
5	4	nn0constr	⊢ ( 𝜑 → 0 ∈ Constr )
6		1nn0	⊢ 1 ∈ ℕ0
7	6	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
8	7	nn0constr	⊢ ( 𝜑 → 1 ∈ Constr )
9	1	constrcn	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
10	9	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
11	9 2	absne0d	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≠ 0 )
12	10 11	rereccld	⊢ ( 𝜑 → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℝ )
13	10	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
14	9 13 11	divcld	⊢ ( 𝜑 → ( 𝑋 / ( abs ‘ 𝑋 ) ) ∈ ℂ )
15	9	subid1d	⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
16	15	oveq2d	⊢ ( 𝜑 → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( 𝑋 − 0 ) ) = ( ( 1 / ( abs ‘ 𝑋 ) ) · 𝑋 ) )
17	12	recnd	⊢ ( 𝜑 → ( 1 / ( abs ‘ 𝑋 ) ) ∈ ℂ )
18	15 9	eqeltrd	⊢ ( 𝜑 → ( 𝑋 − 0 ) ∈ ℂ )
19	17 18	mulcld	⊢ ( 𝜑 → ( ( 1 / ( abs ‘ 𝑋 ) ) · ( 𝑋 − 0 ) ) ∈ ℂ )
20	19	addlidd	⊢ ( 𝜑 → ( 0 + ( ( 1 / ( abs ‘ 𝑋 ) ) · ( 𝑋 − 0 ) ) ) = ( ( 1 / ( abs ‘ 𝑋 ) ) · ( 𝑋 − 0 ) ) )
21	9 13 11	divrec2d	⊢ ( 𝜑 → ( 𝑋 / ( abs ‘ 𝑋 ) ) = ( ( 1 / ( abs ‘ 𝑋 ) ) · 𝑋 ) )
22	16 20 21	3eqtr4rd	⊢ ( 𝜑 → ( 𝑋 / ( abs ‘ 𝑋 ) ) = ( 0 + ( ( 1 / ( abs ‘ 𝑋 ) ) · ( 𝑋 − 0 ) ) ) )
23		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
24	7	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 1 )
25	23 24	absidd	⊢ ( 𝜑 → ( abs ‘ 1 ) = 1 )
26		1m0e1	⊢ ( 1 − 0 ) = 1
27	26	a1i	⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
28	27	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( 1 − 0 ) ) = ( abs ‘ 1 ) )
29	14	subid1d	⊢ ( 𝜑 → ( ( 𝑋 / ( abs ‘ 𝑋 ) ) − 0 ) = ( 𝑋 / ( abs ‘ 𝑋 ) ) )
30	29	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 / ( abs ‘ 𝑋 ) ) − 0 ) ) = ( abs ‘ ( 𝑋 / ( abs ‘ 𝑋 ) ) ) )
31	9 13 11	absdivd	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 / ( abs ‘ 𝑋 ) ) ) = ( ( abs ‘ 𝑋 ) / ( abs ‘ ( abs ‘ 𝑋 ) ) ) )
32		absidm	⊢ ( 𝑋 ∈ ℂ → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
33	9 32	syl	⊢ ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
34	33	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ ( abs ‘ 𝑋 ) ) ) = ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )
35	13 11	dividd	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) = 1 )
36	34 35	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) / ( abs ‘ ( abs ‘ 𝑋 ) ) ) = 1 )
37	30 31 36	3eqtrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 / ( abs ‘ 𝑋 ) ) − 0 ) ) = 1 )
38	25 28 37	3eqtr4rd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 / ( abs ‘ 𝑋 ) ) − 0 ) ) = ( abs ‘ ( 1 − 0 ) ) )
39	5 1 5 8 5 12 14 22 38	constrlccl	⊢ ( 𝜑 → ( 𝑋 / ( abs ‘ 𝑋 ) ) ∈ Constr )