Description: Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ltexpi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pinn | |
|
2 | pinn | |
|
3 | nnaordex | |
|
4 | 1 2 3 | syl2an | |
5 | ltpiord | |
|
6 | addpiord | |
|
7 | 6 | eqeq1d | |
8 | 7 | pm5.32da | |
9 | elni2 | |
|
10 | 9 | anbi1i | |
11 | anass | |
|
12 | 10 11 | bitri | |
13 | 8 12 | bitrdi | |
14 | 13 | rexbidv2 | |
15 | 14 | adantr | |
16 | 4 5 15 | 3bitr4d | |