Metamath Proof Explorer


Theorem nnsgrpnmnd

Description: The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020)

Ref Expression
Hypothesis nnsgrp.m M = fld 𝑠
Assertion nnsgrpnmnd M Mnd

Proof

Step Hyp Ref Expression
1 nnsgrp.m M = fld 𝑠
2 nnsscn
3 1 cnfldsrngbas = Base M
4 2 3 ax-mp = Base M
5 nnex V
6 1 cnfldsrngadd V + = + M
7 5 6 ax-mp + = + M
8 4 7 isnmnd z x z + x x M Mnd
9 1nn 1
10 9 a1i z 1
11 oveq2 x = 1 z + x = z + 1
12 id x = 1 x = 1
13 11 12 neeq12d x = 1 z + x x z + 1 1
14 13 adantl z x = 1 z + x x z + 1 1
15 nnne0 z z 0
16 15 necomd z 0 z
17 1cnd z 1
18 nncn z z
19 17 17 18 subadd2d z 1 1 = z z + 1 = 1
20 1m1e0 1 1 = 0
21 20 a1i z 1 1 = 0
22 21 eqeq1d z 1 1 = z 0 = z
23 19 22 bitr3d z z + 1 = 1 0 = z
24 23 necon3bid z z + 1 1 0 z
25 16 24 mpbird z z + 1 1
26 10 14 25 rspcedvd z x z + x x
27 8 26 mprg M Mnd