Theorem addclpi

Description: Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addclpi	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) e. N. )

Proof

Step	Hyp	Ref	Expression
1		addpiord	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
2		pinn	|- ( A e. N. -> A e. _om )
3		pinn	|- ( B e. N. -> B e. _om )
4		nnacl	|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
5	3 4	sylan2	|- ( ( A e. _om /\ B e. N. ) -> ( A +o B ) e. _om )
6		elni2	|- ( B e. N. <-> ( B e. _om /\ (/) e. B ) )
7		nnaordi	|- ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> ( A +o (/) ) e. ( A +o B ) ) )
8		ne0i	|- ( ( A +o (/) ) e. ( A +o B ) -> ( A +o B ) =/= (/) )
9	7 8	syl6	|- ( ( B e. _om /\ A e. _om ) -> ( (/) e. B -> ( A +o B ) =/= (/) ) )
10	9	expcom	|- ( A e. _om -> ( B e. _om -> ( (/) e. B -> ( A +o B ) =/= (/) ) ) )
11	10	imp32	|- ( ( A e. _om /\ ( B e. _om /\ (/) e. B ) ) -> ( A +o B ) =/= (/) )
12	6 11	sylan2b	|- ( ( A e. _om /\ B e. N. ) -> ( A +o B ) =/= (/) )
13		elni	|- ( ( A +o B ) e. N. <-> ( ( A +o B ) e. _om /\ ( A +o B ) =/= (/) ) )
14	5 12 13	sylanbrc	|- ( ( A e. _om /\ B e. N. ) -> ( A +o B ) e. N. )
15	2 14	sylan	|- ( ( A e. N. /\ B e. N. ) -> ( A +o B ) e. N. )
16	1 15	eqeltrd	|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) e. N. )