Theorem constrnegcl

Description: Constructible numbers are closed under additive inverse. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypothesis	constrnegcl.1	|- ( ph -> X e. Constr )
Assertion	constrnegcl	|- ( ph -> -u X e. Constr )

Proof

Step	Hyp	Ref	Expression
1		constrnegcl.1	|- ( ph -> X e. Constr )
2		0nn0	|- 0 e. NN0
3	2	a1i	|- ( ph -> 0 e. NN0 )
4	3	nn0constr	|- ( ph -> 0 e. Constr )
5		1red	|- ( ph -> 1 e. RR )
6	5	renegcld	|- ( ph -> -u 1 e. RR )
7	1	constrcn	|- ( ph -> X e. CC )
8	7	negcld	|- ( ph -> -u X e. CC )
9	6	recnd	|- ( ph -> -u 1 e. CC )
10	7	subid1d	|- ( ph -> ( X - 0 ) = X )
11	10 7	eqeltrd	|- ( ph -> ( X - 0 ) e. CC )
12	9 11	mulcld	|- ( ph -> ( -u 1 x. ( X - 0 ) ) e. CC )
13	12	addlidd	|- ( ph -> ( 0 + ( -u 1 x. ( X - 0 ) ) ) = ( -u 1 x. ( X - 0 ) ) )
14	11	mulm1d	|- ( ph -> ( -u 1 x. ( X - 0 ) ) = -u ( X - 0 ) )
15	10	negeqd	|- ( ph -> -u ( X - 0 ) = -u X )
16	13 14 15	3eqtrrd	|- ( ph -> -u X = ( 0 + ( -u 1 x. ( X - 0 ) ) ) )
17	7	absnegd	|- ( ph -> ( abs ` -u X ) = ( abs ` X ) )
18	8	subid1d	|- ( ph -> ( -u X - 0 ) = -u X )
19	18	fveq2d	|- ( ph -> ( abs ` ( -u X - 0 ) ) = ( abs ` -u X ) )
20	10	fveq2d	|- ( ph -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
21	17 19 20	3eqtr4d	|- ( ph -> ( abs ` ( -u X - 0 ) ) = ( abs ` ( X - 0 ) ) )
22	4 1 4 1 4 6 8 16 21	constrlccl	|- ( ph -> -u X e. Constr )