Theorem zconstr

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

	Ref	Expression
Hypothesis	zconstr.1	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
Assertion	zconstr	⊢ ( 𝜑 → 𝑋 ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		zconstr.1	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
2		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℕ0 )
3	2	nn0constr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℕ0 ) → 𝑋 ∈ Constr )
4	1	zcnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5	4	negnegd	⊢ ( 𝜑 → - - 𝑋 = 𝑋 )
6	5	adantr	⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℕ0 ) → - - 𝑋 = 𝑋 )
7		simpr	⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℕ0 ) → - 𝑋 ∈ ℕ0 )
8	7	nn0constr	⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℕ0 ) → - 𝑋 ∈ Constr )
9	8	constrnegcl	⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℕ0 ) → - - 𝑋 ∈ Constr )
10	6 9	eqeltrrd	⊢ ( ( 𝜑 ∧ - 𝑋 ∈ ℕ0 ) → 𝑋 ∈ Constr )
11		elznn0	⊢ ( 𝑋 ∈ ℤ ↔ ( 𝑋 ∈ ℝ ∧ ( 𝑋 ∈ ℕ0 ∨ - 𝑋 ∈ ℕ0 ) ) )
12	1 11	sylib	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ ( 𝑋 ∈ ℕ0 ∨ - 𝑋 ∈ ℕ0 ) ) )
13	12	simprd	⊢ ( 𝜑 → ( 𝑋 ∈ ℕ0 ∨ - 𝑋 ∈ ℕ0 ) )
14	3 10 13	mpjaodan	⊢ ( 𝜑 → 𝑋 ∈ Constr )