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𝑵B𝑵A+𝑵B𝑵

Proof

Step Hyp Ref Expression
1 addpiord A𝑵B𝑵A+𝑵B=A+𝑜B
2 pinn A𝑵Aω
3 pinn B𝑵Bω
4 nnacl AωBωA+𝑜Bω
5 3 4 sylan2 AωB𝑵A+𝑜Bω
6 elni2 B𝑵BωB
7 nnaordi BωAωBA+𝑜A+𝑜B
8 ne0i A+𝑜A+𝑜BA+𝑜B
9 7 8 syl6 BωAωBA+𝑜B
10 9 expcom AωBωBA+𝑜B
11 10 imp32 AωBωBA+𝑜B
12 6 11 sylan2b AωB𝑵A+𝑜B
13 elni A+𝑜B𝑵A+𝑜BωA+𝑜B
14 5 12 13 sylanbrc AωB𝑵A+𝑜B𝑵
15 2 14 sylan A𝑵B𝑵A+𝑜B𝑵
16 1 15 eqeltrd A𝑵B𝑵A+𝑵B𝑵