Description: Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | addclpi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addpiord | |
|
2 | pinn | |
|
3 | pinn | |
|
4 | nnacl | |
|
5 | 3 4 | sylan2 | |
6 | elni2 | |
|
7 | nnaordi | |
|
8 | ne0i | |
|
9 | 7 8 | syl6 | |
10 | 9 | expcom | |
11 | 10 | imp32 | |
12 | 6 11 | sylan2b | |
13 | elni | |
|
14 | 5 12 13 | sylanbrc | |
15 | 2 14 | sylan | |
16 | 1 15 | eqeltrd | |