Theorem constrabscl

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

	Ref	Expression
Hypothesis	constrabscl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion	constrabscl	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrabscl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
3	2	zconstr	⊢ ( 𝜑 → 0 ∈ Constr )
4		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
5	4	zconstr	⊢ ( 𝜑 → 1 ∈ Constr )
6	1	constrcn	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
7	6	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
9		1m0e1	⊢ ( 1 − 0 ) = 1
10	9	a1i	⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
11		ax-1cn	⊢ 1 ∈ ℂ
12	10 11	eqeltrdi	⊢ ( 𝜑 → ( 1 − 0 ) ∈ ℂ )
13	8 12	mulcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ∈ ℂ )
14	13	addlidd	⊢ ( 𝜑 → ( 0 + ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ) = ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) )
15	10	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) = ( ( abs ‘ 𝑋 ) · 1 ) )
16	8	mulridd	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) · 1 ) = ( abs ‘ 𝑋 ) )
17	14 15 16	3eqtrrd	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) = ( 0 + ( ( abs ‘ 𝑋 ) · ( 1 − 0 ) ) ) )
18	6	absge0d	⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑋 ) )
19	7 18	absidd	⊢ ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) )
20	8	subid1d	⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) − 0 ) = ( abs ‘ 𝑋 ) )
21	20	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( abs ‘ 𝑋 ) ) )
22	6	subid1d	⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
23	22	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) )
24	19 21 23	3eqtr4d	⊢ ( 𝜑 → ( abs ‘ ( ( abs ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( 𝑋 − 0 ) ) )
25	3 5 3 1 3 7 8 17 24	constrlccl	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ Constr )