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

Proof

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