Theorem constrnegcl

Description: Constructible numbers are closed under additive inverse. Item (2) of Theorem 7.10 of Stewart p. 96. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypothesis	constrnegcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
Assertion	constrnegcl	$$⊢\phi \to -X\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrnegcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
4	3	nn0constr	$$⊢\phi \to 0\in \mathrm{Constr}$$
5		1red	$$⊢\phi \to 1\in ℝ$$
6	5	renegcld	$$⊢\phi \to -1\in ℝ$$
7	1	constrcn	$$⊢\phi \to X\in ℂ$$
8	7	negcld	$$⊢\phi \to -X\in ℂ$$
9	6	recnd	$$⊢\phi \to -1\in ℂ$$
10	7	subid1d	$$⊢\phi \to X-0=X$$
11	10 7	eqeltrd	$$⊢\phi \to X-0\in ℂ$$
12	9 11	mulcld	$$⊢\phi \to -1\left(X-0\right)\in ℂ$$
13	12	addlidd	$$⊢\phi \to 0+-1\left(X-0\right)=-1\left(X-0\right)$$
14	11	mulm1d	$$⊢\phi \to -1\left(X-0\right)=-\left(X-0\right)$$
15	10	negeqd	$$⊢\phi \to -\left(X-0\right)=-X$$
16	13 14 15	3eqtrrd	$$⊢\phi \to -X=0+-1\left(X-0\right)$$
17	7	absnegd	$$⊢\phi \to \left|-X\right|=\left|X\right|$$
18	8	subid1d	$$⊢\phi \to -X-0=-X$$
19	18	fveq2d	$$⊢\phi \to \left|-X-0\right|=\left|-X\right|$$
20	10	fveq2d	$$⊢\phi \to \left|X-0\right|=\left|X\right|$$
21	17 19 20	3eqtr4d	$$⊢\phi \to \left|-X-0\right|=\left|X-0\right|$$
22	4 1 4 1 4 6 8 16 21	constrlccl	$$⊢\phi \to -X\in \mathrm{Constr}$$