# Metamath Proof Explorer

Description: There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion addnidpi ${⊢}{A}\in 𝑵\to ¬{A}{+}_{𝑵}{B}={A}$

### Proof

Step Hyp Ref Expression
1 pinn ${⊢}{A}\in 𝑵\to {A}\in \mathrm{\omega }$
2 elni2 ${⊢}{B}\in 𝑵↔\left({B}\in \mathrm{\omega }\wedge \varnothing \in {B}\right)$
3 nnaordi ${⊢}\left({B}\in \mathrm{\omega }\wedge {A}\in \mathrm{\omega }\right)\to \left(\varnothing \in {B}\to {A}{+}_{𝑜}\varnothing \in \left({A}{+}_{𝑜}{B}\right)\right)$
4 nna0 ${⊢}{A}\in \mathrm{\omega }\to {A}{+}_{𝑜}\varnothing ={A}$
5 4 eleq1d ${⊢}{A}\in \mathrm{\omega }\to \left({A}{+}_{𝑜}\varnothing \in \left({A}{+}_{𝑜}{B}\right)↔{A}\in \left({A}{+}_{𝑜}{B}\right)\right)$
6 nnord ${⊢}{A}\in \mathrm{\omega }\to \mathrm{Ord}{A}$
7 ordirr ${⊢}\mathrm{Ord}{A}\to ¬{A}\in {A}$
8 6 7 syl ${⊢}{A}\in \mathrm{\omega }\to ¬{A}\in {A}$
9 eleq2 ${⊢}{A}{+}_{𝑜}{B}={A}\to \left({A}\in \left({A}{+}_{𝑜}{B}\right)↔{A}\in {A}\right)$
10 9 notbid ${⊢}{A}{+}_{𝑜}{B}={A}\to \left(¬{A}\in \left({A}{+}_{𝑜}{B}\right)↔¬{A}\in {A}\right)$
11 8 10 syl5ibrcom ${⊢}{A}\in \mathrm{\omega }\to \left({A}{+}_{𝑜}{B}={A}\to ¬{A}\in \left({A}{+}_{𝑜}{B}\right)\right)$
12 11 con2d ${⊢}{A}\in \mathrm{\omega }\to \left({A}\in \left({A}{+}_{𝑜}{B}\right)\to ¬{A}{+}_{𝑜}{B}={A}\right)$
13 5 12 sylbid ${⊢}{A}\in \mathrm{\omega }\to \left({A}{+}_{𝑜}\varnothing \in \left({A}{+}_{𝑜}{B}\right)\to ¬{A}{+}_{𝑜}{B}={A}\right)$
14 13 adantl ${⊢}\left({B}\in \mathrm{\omega }\wedge {A}\in \mathrm{\omega }\right)\to \left({A}{+}_{𝑜}\varnothing \in \left({A}{+}_{𝑜}{B}\right)\to ¬{A}{+}_{𝑜}{B}={A}\right)$
15 3 14 syld ${⊢}\left({B}\in \mathrm{\omega }\wedge {A}\in \mathrm{\omega }\right)\to \left(\varnothing \in {B}\to ¬{A}{+}_{𝑜}{B}={A}\right)$
16 15 expcom ${⊢}{A}\in \mathrm{\omega }\to \left({B}\in \mathrm{\omega }\to \left(\varnothing \in {B}\to ¬{A}{+}_{𝑜}{B}={A}\right)\right)$
17 16 imp32 ${⊢}\left({A}\in \mathrm{\omega }\wedge \left({B}\in \mathrm{\omega }\wedge \varnothing \in {B}\right)\right)\to ¬{A}{+}_{𝑜}{B}={A}$
18 2 17 sylan2b ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in 𝑵\right)\to ¬{A}{+}_{𝑜}{B}={A}$
19 1 18 sylan ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to ¬{A}{+}_{𝑜}{B}={A}$
20 addpiord ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to {A}{+}_{𝑵}{B}={A}{+}_{𝑜}{B}$
21 20 eqeq1d ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to \left({A}{+}_{𝑵}{B}={A}↔{A}{+}_{𝑜}{B}={A}\right)$
22 19 21 mtbird ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to ¬{A}{+}_{𝑵}{B}={A}$
23 22 a1d ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to \left({A}\in 𝑵\to ¬{A}{+}_{𝑵}{B}={A}\right)$
24 dmaddpi ${⊢}\mathrm{dom}{+}_{𝑵}=𝑵×𝑵$
25 24 ndmov ${⊢}¬\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to {A}{+}_{𝑵}{B}=\varnothing$
26 25 eqeq1d ${⊢}¬\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to \left({A}{+}_{𝑵}{B}={A}↔\varnothing ={A}\right)$
27 0npi ${⊢}¬\varnothing \in 𝑵$
28 eleq1 ${⊢}\varnothing ={A}\to \left(\varnothing \in 𝑵↔{A}\in 𝑵\right)$
29 27 28 mtbii ${⊢}\varnothing ={A}\to ¬{A}\in 𝑵$
30 26 29 syl6bi ${⊢}¬\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to \left({A}{+}_{𝑵}{B}={A}\to ¬{A}\in 𝑵\right)$
31 30 con2d ${⊢}¬\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to \left({A}\in 𝑵\to ¬{A}{+}_{𝑵}{B}={A}\right)$
32 23 31 pm2.61i ${⊢}{A}\in 𝑵\to ¬{A}{+}_{𝑵}{B}={A}$