Theorem constrnegcl

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

	Ref	Expression
Hypothesis	constrnegcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion	constrnegcl	⊢ ( 𝜑 → - 𝑋 ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrnegcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		0nn0	⊢ 0 ∈ ℕ0
3	2	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
4	3	nn0constr	⊢ ( 𝜑 → 0 ∈ Constr )
5		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
6	5	renegcld	⊢ ( 𝜑 → - 1 ∈ ℝ )
7	1	constrcn	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
8	7	negcld	⊢ ( 𝜑 → - 𝑋 ∈ ℂ )
9	6	recnd	⊢ ( 𝜑 → - 1 ∈ ℂ )
10	7	subid1d	⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
11	10 7	eqeltrd	⊢ ( 𝜑 → ( 𝑋 − 0 ) ∈ ℂ )
12	9 11	mulcld	⊢ ( 𝜑 → ( - 1 · ( 𝑋 − 0 ) ) ∈ ℂ )
13	12	addlidd	⊢ ( 𝜑 → ( 0 + ( - 1 · ( 𝑋 − 0 ) ) ) = ( - 1 · ( 𝑋 − 0 ) ) )
14	11	mulm1d	⊢ ( 𝜑 → ( - 1 · ( 𝑋 − 0 ) ) = - ( 𝑋 − 0 ) )
15	10	negeqd	⊢ ( 𝜑 → - ( 𝑋 − 0 ) = - 𝑋 )
16	13 14 15	3eqtrrd	⊢ ( 𝜑 → - 𝑋 = ( 0 + ( - 1 · ( 𝑋 − 0 ) ) ) )
17	7	absnegd	⊢ ( 𝜑 → ( abs ‘ - 𝑋 ) = ( abs ‘ 𝑋 ) )
18	8	subid1d	⊢ ( 𝜑 → ( - 𝑋 − 0 ) = - 𝑋 )
19	18	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( - 𝑋 − 0 ) ) = ( abs ‘ - 𝑋 ) )
20	10	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) )
21	17 19 20	3eqtr4d	⊢ ( 𝜑 → ( abs ‘ ( - 𝑋 − 0 ) ) = ( abs ‘ ( 𝑋 − 0 ) ) )
22	4 1 4 1 4 6 8 16 21	constrlccl	⊢ ( 𝜑 → - 𝑋 ∈ Constr )