Metamath Proof Explorer


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. )