Theorem zconstr

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

	Ref	Expression
Hypothesis	zconstr.1	|- ( ph -> X e. ZZ )
Assertion	zconstr	|- ( ph -> X e. Constr )

Proof

Step	Hyp	Ref	Expression
1		zconstr.1	|- ( ph -> X e. ZZ )
2		simpr	|- ( ( ph /\ X e. NN0 ) -> X e. NN0 )
3	2	nn0constr	|- ( ( ph /\ X e. NN0 ) -> X e. Constr )
4	1	zcnd	|- ( ph -> X e. CC )
5	4	negnegd	|- ( ph -> -u -u X = X )
6	5	adantr	|- ( ( ph /\ -u X e. NN0 ) -> -u -u X = X )
7		simpr	|- ( ( ph /\ -u X e. NN0 ) -> -u X e. NN0 )
8	7	nn0constr	|- ( ( ph /\ -u X e. NN0 ) -> -u X e. Constr )
9	8	constrnegcl	|- ( ( ph /\ -u X e. NN0 ) -> -u -u X e. Constr )
10	6 9	eqeltrrd	|- ( ( ph /\ -u X e. NN0 ) -> X e. Constr )
11		elznn0	|- ( X e. ZZ <-> ( X e. RR /\ ( X e. NN0 \/ -u X e. NN0 ) ) )
12	1 11	sylib	|- ( ph -> ( X e. RR /\ ( X e. NN0 \/ -u X e. NN0 ) ) )
13	12	simprd	|- ( ph -> ( X e. NN0 \/ -u X e. NN0 ) )
14	3 10 13	mpjaodan	|- ( ph -> X e. Constr )