Theorem constrabscl

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

	Ref	Expression
Hypothesis	constrabscl.1	|- ( ph -> X e. Constr )
Assertion	constrabscl	|- ( ph -> ( abs ` X ) e. Constr )

Proof

Step	Hyp	Ref	Expression
1		constrabscl.1	|- ( ph -> X e. Constr )
2		0zd	|- ( ph -> 0 e. ZZ )
3	2	zconstr	|- ( ph -> 0 e. Constr )
4		1zzd	|- ( ph -> 1 e. ZZ )
5	4	zconstr	|- ( ph -> 1 e. Constr )
6	1	constrcn	|- ( ph -> X e. CC )
7	6	abscld	|- ( ph -> ( abs ` X ) e. RR )
8	7	recnd	|- ( ph -> ( abs ` X ) e. CC )
9		1m0e1	|- ( 1 - 0 ) = 1
10	9	a1i	|- ( ph -> ( 1 - 0 ) = 1 )
11		ax-1cn	|- 1 e. CC
12	10 11	eqeltrdi	|- ( ph -> ( 1 - 0 ) e. CC )
13	8 12	mulcld	|- ( ph -> ( ( abs ` X ) x. ( 1 - 0 ) ) e. CC )
14	13	addlidd	|- ( ph -> ( 0 + ( ( abs ` X ) x. ( 1 - 0 ) ) ) = ( ( abs ` X ) x. ( 1 - 0 ) ) )
15	10	oveq2d	|- ( ph -> ( ( abs ` X ) x. ( 1 - 0 ) ) = ( ( abs ` X ) x. 1 ) )
16	8	mulridd	|- ( ph -> ( ( abs ` X ) x. 1 ) = ( abs ` X ) )
17	14 15 16	3eqtrrd	|- ( ph -> ( abs ` X ) = ( 0 + ( ( abs ` X ) x. ( 1 - 0 ) ) ) )
18	6	absge0d	|- ( ph -> 0 <_ ( abs ` X ) )
19	7 18	absidd	|- ( ph -> ( abs ` ( abs ` X ) ) = ( abs ` X ) )
20	8	subid1d	|- ( ph -> ( ( abs ` X ) - 0 ) = ( abs ` X ) )
21	20	fveq2d	|- ( ph -> ( abs ` ( ( abs ` X ) - 0 ) ) = ( abs ` ( abs ` X ) ) )
22	6	subid1d	|- ( ph -> ( X - 0 ) = X )
23	22	fveq2d	|- ( ph -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
24	19 21 23	3eqtr4d	|- ( ph -> ( abs ` ( ( abs ` X ) - 0 ) ) = ( abs ` ( X - 0 ) ) )
25	3 5 3 1 3 7 8 17 24	constrlccl	|- ( ph -> ( abs ` X ) e. Constr )