Theorem oddinmgm

Description: The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl , and even a non-unital ring, see 2zrng . (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypotheses	oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
	oddinmgm.r	|- M = ( CCfld |`s O )
Assertion	oddinmgm	|- M e/ Mgm

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2		oddinmgm.r	|- M = ( CCfld |`s O )
3	1	1odd	|- 1 e. O
4	1	2nodd	|- 2 e/ O
5		1p1e2	|- ( 1 + 1 ) = 2
6		neleq1	|- ( ( 1 + 1 ) = 2 -> ( ( 1 + 1 ) e/ O <-> 2 e/ O ) )
7	5 6	ax-mp	|- ( ( 1 + 1 ) e/ O <-> 2 e/ O )
8	4 7	mpbir	|- ( 1 + 1 ) e/ O
9	1 2	oddibas	|- O = ( Base ` M )
10	1 2	oddiadd	|- + = ( +g ` M )
11	9 10	isnmgm	|- ( ( 1 e. O /\ 1 e. O /\ ( 1 + 1 ) e/ O ) -> M e/ Mgm )
12	3 3 8 11	mp3an	|- M e/ Mgm