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	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
	oddinmgm.r	⊢ 𝑀 = ( ℂfld ↾s 𝑂 )
Assertion	oddinmgm	⊢ 𝑀 ∉ Mgm

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
2		oddinmgm.r	⊢ 𝑀 = ( ℂfld ↾s 𝑂 )
3	1	1odd	⊢ 1 ∈ 𝑂
4	1	2nodd	⊢ 2 ∉ 𝑂
5		1p1e2	⊢ ( 1 + 1 ) = 2
6		neleq1	⊢ ( ( 1 + 1 ) = 2 → ( ( 1 + 1 ) ∉ 𝑂 ↔ 2 ∉ 𝑂 ) )
7	5 6	ax-mp	⊢ ( ( 1 + 1 ) ∉ 𝑂 ↔ 2 ∉ 𝑂 )
8	4 7	mpbir	⊢ ( 1 + 1 ) ∉ 𝑂
9	1 2	oddibas	⊢ 𝑂 = ( Base ‘ 𝑀 )
10	1 2	oddiadd	⊢ + = ( +g ‘ 𝑀 )
11	9 10	isnmgm	⊢ ( ( 1 ∈ 𝑂 ∧ 1 ∈ 𝑂 ∧ ( 1 + 1 ) ∉ 𝑂 ) → 𝑀 ∉ Mgm )
12	3 3 8 11	mp3an	⊢ 𝑀 ∉ Mgm