Metamath Proof Explorer

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 ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
oddinmgm.r ⊢ M = ℂ fld ↾ 𝑠 O
Assertion oddinmgm ⊢ M ∉ Mgm

Proof

Step Hyp Ref Expression
1 oddinmgm.e ⊢ O = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x + 1
2 oddinmgm.r ⊢ M = ℂ fld ↾ 𝑠 O
3 1 1odd ⊢ 1 ∈ O
4 1 2nodd ⊢ 2 ∉ O
5 1p1e2 ⊢ 1 + 1 = 2
6 neleq1 ⊢ 1 + 1 = 2 → 1 + 1 ∉ O ↔ 2 ∉ O
7 5 6 ax-mp ⊢ 1 + 1 ∉ O ↔ 2 ∉ O
8 4 7 mpbir ⊢ 1 + 1 ∉ O
9 1 2 oddibas ⊢ O = Base M
10 1 2 oddiadd ⊢ + = + M
11 9 10 isnmgm ⊢ 1 ∈ O ∧ 1 ∈ O ∧ 1 + 1 ∉ O → M ∉ Mgm
12 3 3 8 11 mp3an ⊢ M ∉ Mgm