Theorem 2zrng

Description: The ring of integers restricted to the even integers is a (non-unital) ring, the "ring of even integers". Remark: the structure of the complementary subset of the set of integers, the odd integers, is not even a magma, see oddinmgm . (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zlidl.u	|- U = ( LIdeal ` ZZring )
	2zrng.r	|- R = ( ZZring |`s E )
Assertion	2zrng	|- R e. Rng

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2		2zlidl.u	|- U = ( LIdeal ` ZZring )
3		2zrng.r	|- R = ( ZZring |`s E )
4		zringring	|- ZZring e. Ring
5	1 2	2zlidl	|- E e. U
6	2 3	lidlrng	|- ( ( ZZring e. Ring /\ E e. U ) -> R e. Rng )
7	4 5 6	mp2an	|- R e. Rng