Theorem addnidpi

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 \neg A{+}_{𝑵}B=A$$

Proof

Step	Hyp	Ref	Expression
1		pinn	$$⊢A\in 𝑵\to A\in \mathrm{\omega }$$
2		elni2	$$⊢B\in 𝑵\leftrightarrow \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)\leftrightarrow A\in \left(A{+}_{𝑜}B\right)\right)$$
6		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
7		ordirr	$$⊢\mathrm{Ord}A\to \neg A\in A$$
8	6 7	syl	$$⊢A\in \mathrm{\omega }\to \neg A\in A$$
9		eleq2	$$⊢A{+}_{𝑜}B=A\to \left(A\in \left(A{+}_{𝑜}B\right)\leftrightarrow A\in A\right)$$
10	9	notbid	$$⊢A{+}_{𝑜}B=A\to \left(\neg A\in \left(A{+}_{𝑜}B\right)\leftrightarrow \neg A\in A\right)$$
11	8 10	syl5ibrcom	$$⊢A\in \mathrm{\omega }\to \left(A{+}_{𝑜}B=A\to \neg A\in \left(A{+}_{𝑜}B\right)\right)$$
12	11	con2d	$$⊢A\in \mathrm{\omega }\to \left(A\in \left(A{+}_{𝑜}B\right)\to \neg A{+}_{𝑜}B=A\right)$$
13	5 12	sylbid	$$⊢A\in \mathrm{\omega }\to \left(A{+}_{𝑜}\varnothing \in \left(A{+}_{𝑜}B\right)\to \neg 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 \neg 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 \neg A{+}_{𝑜}B=A\right)$$
16	15	expcom	$$⊢A\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to \left(\varnothing \in B\to \neg 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 \neg A{+}_{𝑜}B=A$$
18	2 17	sylan2b	$$⊢\left(A\in \mathrm{\omega }\wedge B\in 𝑵\right)\to \neg A{+}_{𝑜}B=A$$
19	1 18	sylan	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \neg 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\leftrightarrow A{+}_{𝑜}B=A\right)$$
22	19 21	mtbird	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \neg A{+}_{𝑵}B=A$$
23	22	a1d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A\in 𝑵\to \neg A{+}_{𝑵}B=A\right)$$
24		dmaddpi	$$⊢\mathrm{dom}{+}_{𝑵}=𝑵\times 𝑵$$
25	24	ndmov	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=\varnothing$$
26	25	eqeq1d	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A{+}_{𝑵}B=A\leftrightarrow \varnothing =A\right)$$
27		0npi	$$⊢\neg \varnothing \in 𝑵$$
28		eleq1	$$⊢\varnothing =A\to \left(\varnothing \in 𝑵\leftrightarrow A\in 𝑵\right)$$
29	27 28	mtbii	$$⊢\varnothing =A\to \neg A\in 𝑵$$
30	26 29	syl6bi	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A{+}_{𝑵}B=A\to \neg A\in 𝑵\right)$$
31	30	con2d	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A\in 𝑵\to \neg A{+}_{𝑵}B=A\right)$$
32	23 31	pm2.61i	$$⊢A\in 𝑵\to \neg A{+}_{𝑵}B=A$$