Theorem constrabscl

Description: Constructible numbers are closed under absolute value (modulus). (Contributed by Thierry Arnoux, 6-Nov-2025)

	Ref	Expression
Hypothesis	constrabscl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
Assertion	constrabscl	$$⊢\phi \to \left|X\right|\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrabscl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
3	2	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
4		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
5	4	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
6	1	constrcn	$$⊢\phi \to X\in ℂ$$
7	6	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
8	7	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
9		1m0e1	$$⊢1-0=1$$
10	9	a1i	$$⊢\phi \to 1-0=1$$
11		ax-1cn	$$⊢1\in ℂ$$
12	10 11	eqeltrdi	$$⊢\phi \to 1-0\in ℂ$$
13	8 12	mulcld	$$⊢\phi \to \left|X\right|\left(1-0\right)\in ℂ$$
14	13	addlidd	$$⊢\phi \to 0+\left|X\right|\left(1-0\right)=\left|X\right|\left(1-0\right)$$
15	10	oveq2d	$$⊢\phi \to \left|X\right|\left(1-0\right)=\left|X\right|\cdot 1$$
16	8	mulridd	$$⊢\phi \to \left|X\right|\cdot 1=\left|X\right|$$
17	14 15 16	3eqtrrd	$$⊢\phi \to \left|X\right|=0+\left|X\right|\left(1-0\right)$$
18	6	absge0d	$$⊢\phi \to 0\le \left|X\right|$$
19	7 18	absidd	$$⊢\phi \to \left|\left|X\right|\right|=\left|X\right|$$
20	8	subid1d	$$⊢\phi \to \left|X\right|-0=\left|X\right|$$
21	20	fveq2d	$$⊢\phi \to \left|\left|X\right|-0\right|=\left|\left|X\right|\right|$$
22	6	subid1d	$$⊢\phi \to X-0=X$$
23	22	fveq2d	$$⊢\phi \to \left|X-0\right|=\left|X\right|$$
24	19 21 23	3eqtr4d	$$⊢\phi \to \left|\left|X\right|-0\right|=\left|X-0\right|$$
25	3 5 3 1 3 7 8 17 24	constrlccl	$$⊢\phi \to \left|X\right|\in \mathrm{Constr}$$