Metamath Proof Explorer


Theorem ltexpi

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

Proof

Step Hyp Ref Expression
1 pinn A𝑵Aω
2 pinn B𝑵Bω
3 nnaordex AωBωABxωxA+𝑜x=B
4 1 2 3 syl2an A𝑵B𝑵ABxωxA+𝑜x=B
5 ltpiord A𝑵B𝑵A<𝑵BAB
6 addpiord A𝑵x𝑵A+𝑵x=A+𝑜x
7 6 eqeq1d A𝑵x𝑵A+𝑵x=BA+𝑜x=B
8 7 pm5.32da A𝑵x𝑵A+𝑵x=Bx𝑵A+𝑜x=B
9 elni2 x𝑵xωx
10 9 anbi1i x𝑵A+𝑜x=BxωxA+𝑜x=B
11 anass xωxA+𝑜x=BxωxA+𝑜x=B
12 10 11 bitri x𝑵A+𝑜x=BxωxA+𝑜x=B
13 8 12 bitrdi A𝑵x𝑵A+𝑵x=BxωxA+𝑜x=B
14 13 rexbidv2 A𝑵x𝑵A+𝑵x=BxωxA+𝑜x=B
15 14 adantr A𝑵B𝑵x𝑵A+𝑵x=BxωxA+𝑜x=B
16 4 5 15 3bitr4d A𝑵B𝑵A<𝑵Bx𝑵A+𝑵x=B