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 e. N. /\ B e. N. ) -> ( A E. x e. N. ( A +N x ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		pinn	|- ( A e. N. -> A e. _om )
2		pinn	|- ( B e. N. -> B e. _om )
3		nnaordex	|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
4	1 2 3	syl2an	|- ( ( A e. N. /\ B e. N. ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
5		ltpiord	|- ( ( A e. N. /\ B e. N. ) -> ( A A e. B ) )
6		addpiord	|- ( ( A e. N. /\ x e. N. ) -> ( A +N x ) = ( A +o x ) )
7	6	eqeq1d	|- ( ( A e. N. /\ x e. N. ) -> ( ( A +N x ) = B <-> ( A +o x ) = B ) )
8	7	pm5.32da	|- ( A e. N. -> ( ( x e. N. /\ ( A +N x ) = B ) <-> ( x e. N. /\ ( A +o x ) = B ) ) )
9		elni2	|- ( x e. N. <-> ( x e. _om /\ (/) e. x ) )
10	9	anbi1i	|- ( ( x e. N. /\ ( A +o x ) = B ) <-> ( ( x e. _om /\ (/) e. x ) /\ ( A +o x ) = B ) )
11		anass	|- ( ( ( x e. _om /\ (/) e. x ) /\ ( A +o x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) )
12	10 11	bitri	|- ( ( x e. N. /\ ( A +o x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) )
13	8 12	bitrdi	|- ( A e. N. -> ( ( x e. N. /\ ( A +N x ) = B ) <-> ( x e. _om /\ ( (/) e. x /\ ( A +o x ) = B ) ) ) )
14	13	rexbidv2	|- ( A e. N. -> ( E. x e. N. ( A +N x ) = B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
15	14	adantr	|- ( ( A e. N. /\ B e. N. ) -> ( E. x e. N. ( A +N x ) = B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
16	4 5 15	3bitr4d	|- ( ( A e. N. /\ B e. N. ) -> ( A E. x e. N. ( A +N x ) = B ) )