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	$$⊢\phi \to X\in \mathrm{Constr}$$
	constrdircl.1	$$⊢\phi \to X\ne 0$$
Assertion	constrdircl	$$⊢\phi \to \frac{X}{\left|X\right|}\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrdircl.x	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constrdircl.1	$$⊢\phi \to X\ne 0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	3	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
5	4	nn0constr	$$⊢\phi \to 0\in \mathrm{Constr}$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7	6	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
8	7	nn0constr	$$⊢\phi \to 1\in \mathrm{Constr}$$
9	1	constrcn	$$⊢\phi \to X\in ℂ$$
10	9	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
11	9 2	absne0d	$$⊢\phi \to \left|X\right|\ne 0$$
12	10 11	rereccld	$$⊢\phi \to \frac{1}{\left|X\right|}\in ℝ$$
13	10	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
14	9 13 11	divcld	$$⊢\phi \to \frac{X}{\left|X\right|}\in ℂ$$
15	9	subid1d	$$⊢\phi \to X-0=X$$
16	15	oveq2d	$$⊢\phi \to \left(\frac{1}{\left|X\right|}\right)\left(X-0\right)=\left(\frac{1}{\left|X\right|}\right)X$$
17	12	recnd	$$⊢\phi \to \frac{1}{\left|X\right|}\in ℂ$$
18	15 9	eqeltrd	$$⊢\phi \to X-0\in ℂ$$
19	17 18	mulcld	$$⊢\phi \to \left(\frac{1}{\left|X\right|}\right)\left(X-0\right)\in ℂ$$
20	19	addlidd	$$⊢\phi \to 0+\left(\frac{1}{\left|X\right|}\right)\left(X-0\right)=\left(\frac{1}{\left|X\right|}\right)\left(X-0\right)$$
21	9 13 11	divrec2d	$$⊢\phi \to \frac{X}{\left|X\right|}=\left(\frac{1}{\left|X\right|}\right)X$$
22	16 20 21	3eqtr4rd	$$⊢\phi \to \frac{X}{\left|X\right|}=0+\left(\frac{1}{\left|X\right|}\right)\left(X-0\right)$$
23		1red	$$⊢\phi \to 1\in ℝ$$
24	7	nn0ge0d	$$⊢\phi \to 0\le 1$$
25	23 24	absidd	$$⊢\phi \to \left|1\right|=1$$
26		1m0e1	$$⊢1-0=1$$
27	26	a1i	$$⊢\phi \to 1-0=1$$
28	27	fveq2d	$$⊢\phi \to \left|1-0\right|=\left|1\right|$$
29	14	subid1d	$$⊢\phi \to \left(\frac{X}{\left|X\right|}\right)-0=\frac{X}{\left|X\right|}$$
30	29	fveq2d	$$⊢\phi \to \left|\left(\frac{X}{\left|X\right|}\right)-0\right|=\left|\frac{X}{\left|X\right|}\right|$$
31	9 13 11	absdivd	$$⊢\phi \to \left|\frac{X}{\left|X\right|}\right|=\frac{\left|X\right|}{\left|\left|X\right|\right|}$$
32		absidm	$$⊢X\in ℂ\to \left|\left|X\right|\right|=\left|X\right|$$
33	9 32	syl	$$⊢\phi \to \left|\left|X\right|\right|=\left|X\right|$$
34	33	oveq2d	$$⊢\phi \to \frac{\left|X\right|}{\left|\left|X\right|\right|}=\frac{\left|X\right|}{\left|X\right|}$$
35	13 11	dividd	$$⊢\phi \to \frac{\left|X\right|}{\left|X\right|}=1$$
36	34 35	eqtrd	$$⊢\phi \to \frac{\left|X\right|}{\left|\left|X\right|\right|}=1$$
37	30 31 36	3eqtrd	$$⊢\phi \to \left|\left(\frac{X}{\left|X\right|}\right)-0\right|=1$$
38	25 28 37	3eqtr4rd	$$⊢\phi \to \left|\left(\frac{X}{\left|X\right|}\right)-0\right|=\left|1-0\right|$$
39	5 1 5 8 5 12 14 22 38	constrlccl	$$⊢\phi \to \frac{X}{\left|X\right|}\in \mathrm{Constr}$$