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 e. N. -> -. ( A +N B ) = A )

Proof

Step	Hyp	Ref	Expression
1		pinn	|- ( A e. N. -> A e. _om )
2		elni2	|- ( B e. N. <-> ( B e. _om /\ (/) e. B ) )
3		nnaordi	|- ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> ( A +o (/) ) e. ( A +o B ) ) )
4		nna0	|- ( A e. _om -> ( A +o (/) ) = A )
5	4	eleq1d	|- ( A e. _om -> ( ( A +o (/) ) e. ( A +o B ) <-> A e. ( A +o B ) ) )
6		nnord	|- ( A e. _om -> Ord A )
7		ordirr	|- ( Ord A -> -. A e. A )
8	6 7	syl	|- ( A e. _om -> -. A e. A )
9		eleq2	|- ( ( A +o B ) = A -> ( A e. ( A +o B ) <-> A e. A ) )
10	9	notbid	|- ( ( A +o B ) = A -> ( -. A e. ( A +o B ) <-> -. A e. A ) )
11	8 10	syl5ibrcom	|- ( A e. _om -> ( ( A +o B ) = A -> -. A e. ( A +o B ) ) )
12	11	con2d	|- ( A e. _om -> ( A e. ( A +o B ) -> -. ( A +o B ) = A ) )
13	5 12	sylbid	|- ( A e. _om -> ( ( A +o (/) ) e. ( A +o B ) -> -. ( A +o B ) = A ) )
14	13	adantl	|- ( ( B e. _om /\ A e. _om ) -> ( ( A +o (/) ) e. ( A +o B ) -> -. ( A +o B ) = A ) )
15	3 14	syld	|- ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> -. ( A +o B ) = A ) )
16	15	expcom	|- ( A e. _om -> ( B e. _om -> ( (/) e. B -> -. ( A +o B ) = A ) ) )
17	16	imp32	|- ( ( A e. _om /\ ( B e. _om /\ (/) e. B ) ) -> -. ( A +o B ) = A )
18	2 17	sylan2b	|- ( ( A e. _om /\ B e. N. ) -> -. ( A +o B ) = A )
19	1 18	sylan	|- ( ( A e. N. /\ B e. N. ) -> -. ( A +o B ) = A )
20		addpiord	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
21	20	eqeq1d	|- ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A <-> ( A +o B ) = A ) )
22	19 21	mtbird	|- ( ( A e. N. /\ B e. N. ) -> -. ( A +N B ) = A )
23	22	a1d	|- ( ( A e. N. /\ B e. N. ) -> ( A e. N. -> -. ( A +N B ) = A ) )
24		dmaddpi	|- dom +N = ( N. X. N. )
25	24	ndmov	|- ( -. ( A e. N. /\ B e. N. ) -> ( A +N B ) = (/) )
26	25	eqeq1d	|- ( -. ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A <-> (/) = A ) )
27		0npi	|- -. (/) e. N.
28		eleq1	|- ( (/) = A -> ( (/) e. N. <-> A e. N. ) )
29	27 28	mtbii	|- ( (/) = A -> -. A e. N. )
30	26 29	syl6bi	|- ( -. ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = A -> -. A e. N. ) )
31	30	con2d	|- ( -. ( A e. N. /\ B e. N. ) -> ( A e. N. -> -. ( A +N B ) = A ) )
32	23 31	pm2.61i	|- ( A e. N. -> -. ( A +N B ) = A )