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	⊢ 𝑀 = ( ℂfld ↾s ℕ )
Assertion	nnsgrpnmnd	⊢ 𝑀 ∉ Mnd

Proof

Step	Hyp	Ref	Expression
1		nnsgrp.m	⊢ 𝑀 = ( ℂfld ↾s ℕ )
2		nnsscn	⊢ ℕ ⊆ ℂ
3	1	cnfldsrngbas	⊢ ( ℕ ⊆ ℂ → ℕ = ( Base ‘ 𝑀 ) )
4	2 3	ax-mp	⊢ ℕ = ( Base ‘ 𝑀 )
5		nnex	⊢ ℕ ∈ V
6	1	cnfldsrngadd	⊢ ( ℕ ∈ V → + = ( +g ‘ 𝑀 ) )
7	5 6	ax-mp	⊢ + = ( +g ‘ 𝑀 )
8	4 7	isnmnd	⊢ ( ∀ 𝑧 ∈ ℕ ∃ 𝑥 ∈ ℕ ( 𝑧 + 𝑥 ) ≠ 𝑥 → 𝑀 ∉ Mnd )
9		1nn	⊢ 1 ∈ ℕ
10	9	a1i	⊢ ( 𝑧 ∈ ℕ → 1 ∈ ℕ )
11		oveq2	⊢ ( 𝑥 = 1 → ( 𝑧 + 𝑥 ) = ( 𝑧 + 1 ) )
12		id	⊢ ( 𝑥 = 1 → 𝑥 = 1 )
13	11 12	neeq12d	⊢ ( 𝑥 = 1 → ( ( 𝑧 + 𝑥 ) ≠ 𝑥 ↔ ( 𝑧 + 1 ) ≠ 1 ) )
14	13	adantl	⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑥 = 1 ) → ( ( 𝑧 + 𝑥 ) ≠ 𝑥 ↔ ( 𝑧 + 1 ) ≠ 1 ) )
15		nnne0	⊢ ( 𝑧 ∈ ℕ → 𝑧 ≠ 0 )
16	15	necomd	⊢ ( 𝑧 ∈ ℕ → 0 ≠ 𝑧 )
17		1cnd	⊢ ( 𝑧 ∈ ℕ → 1 ∈ ℂ )
18		nncn	⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℂ )
19	17 17 18	subadd2d	⊢ ( 𝑧 ∈ ℕ → ( ( 1 − 1 ) = 𝑧 ↔ ( 𝑧 + 1 ) = 1 ) )
20		1m1e0	⊢ ( 1 − 1 ) = 0
21	20	a1i	⊢ ( 𝑧 ∈ ℕ → ( 1 − 1 ) = 0 )
22	21	eqeq1d	⊢ ( 𝑧 ∈ ℕ → ( ( 1 − 1 ) = 𝑧 ↔ 0 = 𝑧 ) )
23	19 22	bitr3d	⊢ ( 𝑧 ∈ ℕ → ( ( 𝑧 + 1 ) = 1 ↔ 0 = 𝑧 ) )
24	23	necon3bid	⊢ ( 𝑧 ∈ ℕ → ( ( 𝑧 + 1 ) ≠ 1 ↔ 0 ≠ 𝑧 ) )
25	16 24	mpbird	⊢ ( 𝑧 ∈ ℕ → ( 𝑧 + 1 ) ≠ 1 )
26	10 14 25	rspcedvd	⊢ ( 𝑧 ∈ ℕ → ∃ 𝑥 ∈ ℕ ( 𝑧 + 𝑥 ) ≠ 𝑥 )
27	8 26	mprg	⊢ 𝑀 ∉ Mnd