This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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