Theorem zconstr

Description: Integers are constructible. (Contributed by Thierry Arnoux, 3-Nov-2025)

	Ref	Expression
Hypothesis	zconstr.1	$$⊢\phi \to X\in \mathbb{Z}$$
Assertion	zconstr	$$⊢\phi \to X\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		zconstr.1	$$⊢\phi \to X\in \mathbb{Z}$$
2		simpr	$$⊢\left(\phi \wedge X\in {\mathbb{N}}_0\right)\to X\in {\mathbb{N}}_0$$
3	2	nn0constr	$$⊢\left(\phi \wedge X\in {\mathbb{N}}_0\right)\to X\in \mathrm{Constr}$$
4	1	zcnd	$$⊢\phi \to X\in ℂ$$
5	4	negnegd	$$⊢\phi \to -\left(-X\right)=X$$
6	5	adantr	$$⊢\left(\phi \wedge -X\in {\mathbb{N}}_0\right)\to -\left(-X\right)=X$$
7		simpr	$$⊢\left(\phi \wedge -X\in {\mathbb{N}}_0\right)\to -X\in {\mathbb{N}}_0$$
8	7	nn0constr	$$⊢\left(\phi \wedge -X\in {\mathbb{N}}_0\right)\to -X\in \mathrm{Constr}$$
9	8	constrnegcl	$$⊢\left(\phi \wedge -X\in {\mathbb{N}}_0\right)\to -\left(-X\right)\in \mathrm{Constr}$$
10	6 9	eqeltrrd	$$⊢\left(\phi \wedge -X\in {\mathbb{N}}_0\right)\to X\in \mathrm{Constr}$$
11		elznn0	$$⊢X\in \mathbb{Z}\leftrightarrow \left(X\in ℝ\wedge \left(X\in {\mathbb{N}}_0\vee -X\in {\mathbb{N}}_0\right)\right)$$
12	1 11	sylib	$$⊢\phi \to \left(X\in ℝ\wedge \left(X\in {\mathbb{N}}_0\vee -X\in {\mathbb{N}}_0\right)\right)$$
13	12	simprd	$$⊢\phi \to \left(X\in {\mathbb{N}}_0\vee -X\in {\mathbb{N}}_0\right)$$
14	3 10 13	mpjaodan	$$⊢\phi \to X\in \mathrm{Constr}$$