Theorem xltnegi 9459

Description: Forward direction of xltneg 9460. (Contributed by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
xltnegi	|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )

Proof of Theorem xltnegi

Step	Hyp	Ref	Expression
1		elxr 9404	. . 3 |- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2		elxr 9404	. . . . . 6 |- ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
3		ltneg 8091	. . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -u B < -u A ) )
4		rexneg 9454	. . . . . . . . . 10 |- ( B e. RR -> -e B = -u B )
5		rexneg 9454	. . . . . . . . . 10 |- ( A e. RR -> -e A = -u A )
6	4, 5	breqan12rd 3891	. . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( -e B < -e A <-> -u B < -u A ) )
7	3, 6	bitr4d 190	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -e B < -e A ) )
8	7	biimpd 143	. . . . . . 7 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -e B < -e A ) )
9		xnegeq 9451	. . . . . . . . . . 11 |- ( B = +oo -> -e B = -e +oo )
10		xnegpnf 9452	. . . . . . . . . . 11 |- -e +oo = -oo
11	9, 10	syl6eq 2148	. . . . . . . . . 10 |- ( B = +oo -> -e B = -oo )
12	11	adantl 273	. . . . . . . . 9 |- ( ( A e. RR /\ B = +oo ) -> -e B = -oo )
13		renegcl 7894	. . . . . . . . . . . 12 |- ( A e. RR -> -u A e. RR )
14	5, 13	eqeltrd 2176	. . . . . . . . . . 11 |- ( A e. RR -> -e A e. RR )
15		mnflt 9410	. . . . . . . . . . 11 |- ( -e A e. RR -> -oo < -e A )
16	14, 15	syl 14	. . . . . . . . . 10 |- ( A e. RR -> -oo < -e A )
17	16	adantr 272	. . . . . . . . 9 |- ( ( A e. RR /\ B = +oo ) -> -oo < -e A )
18	12, 17	eqbrtrd 3895	. . . . . . . 8 |- ( ( A e. RR /\ B = +oo ) -> -e B < -e A )
19	18	a1d 22	. . . . . . 7 |- ( ( A e. RR /\ B = +oo ) -> ( A < B -> -e B < -e A ) )
20		simpr 109	. . . . . . . . 9 |- ( ( A e. RR /\ B = -oo ) -> B = -oo )
21	20	breq2d 3887	. . . . . . . 8 |- ( ( A e. RR /\ B = -oo ) -> ( A < B <-> A < -oo ) )
22		rexr 7683	. . . . . . . . . . 11 |- ( A e. RR -> A e. RR* )
23		nltmnf 9415	. . . . . . . . . . 11 |- ( A e. RR* -> -. A < -oo )
24	22, 23	syl 14	. . . . . . . . . 10 |- ( A e. RR -> -. A < -oo )
25	24	adantr 272	. . . . . . . . 9 |- ( ( A e. RR /\ B = -oo ) -> -. A < -oo )
26	25	pm2.21d 589	. . . . . . . 8 |- ( ( A e. RR /\ B = -oo ) -> ( A < -oo -> -e B < -e A ) )
27	21, 26	sylbid 149	. . . . . . 7 |- ( ( A e. RR /\ B = -oo ) -> ( A < B -> -e B < -e A ) )
28	8, 19, 27	3jaodan 1252	. . . . . 6 |- ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -e B < -e A ) )
29	2, 28	sylan2b 283	. . . . 5 |- ( ( A e. RR /\ B e. RR* ) -> ( A < B -> -e B < -e A ) )
30	29	expimpd 358	. . . 4 |- ( A e. RR -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
31		simpl 108	. . . . . . 7 |- ( ( A = +oo /\ B e. RR* ) -> A = +oo )
32	31	breq1d 3885	. . . . . 6 |- ( ( A = +oo /\ B e. RR* ) -> ( A < B <-> +oo < B ) )
33		pnfnlt 9414	. . . . . . . 8 |- ( B e. RR* -> -. +oo < B )
34	33	adantl 273	. . . . . . 7 |- ( ( A = +oo /\ B e. RR* ) -> -. +oo < B )
35	34	pm2.21d 589	. . . . . 6 |- ( ( A = +oo /\ B e. RR* ) -> ( +oo < B -> -e B < -e A ) )
36	32, 35	sylbid 149	. . . . 5 |- ( ( A = +oo /\ B e. RR* ) -> ( A < B -> -e B < -e A ) )
37	36	expimpd 358	. . . 4 |- ( A = +oo -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
38		breq1 3878	. . . . . 6 |- ( A = -oo -> ( A < B <-> -oo < B ) )
39	38	anbi2d 455	. . . . 5 |- ( A = -oo -> ( ( B e. RR* /\ A < B ) <-> ( B e. RR* /\ -oo < B ) ) )
40		renegcl 7894	. . . . . . . . . . 11 |- ( B e. RR -> -u B e. RR )
41	4, 40	eqeltrd 2176	. . . . . . . . . 10 |- ( B e. RR -> -e B e. RR )
42	41	adantr 272	. . . . . . . . 9 |- ( ( B e. RR /\ -oo < B ) -> -e B e. RR )
43		ltpnf 9408	. . . . . . . . 9 |- ( -e B e. RR -> -e B < +oo )
44	42, 43	syl 14	. . . . . . . 8 |- ( ( B e. RR /\ -oo < B ) -> -e B < +oo )
45	11	adantr 272	. . . . . . . . 9 |- ( ( B = +oo /\ -oo < B ) -> -e B = -oo )
46		mnfltpnf 9412	. . . . . . . . 9 |- -oo < +oo
47	45, 46	syl6eqbr 3912	. . . . . . . 8 |- ( ( B = +oo /\ -oo < B ) -> -e B < +oo )
48		breq2 3879	. . . . . . . . . 10 |- ( B = -oo -> ( -oo < B <-> -oo < -oo ) )
49		mnfxr 7694	. . . . . . . . . . . 12 |- -oo e. RR*
50		nltmnf 9415	. . . . . . . . . . . 12 |- ( -oo e. RR* -> -. -oo < -oo )
51	49, 50	ax-mp 7	. . . . . . . . . . 11 |- -. -oo < -oo
52	51	pm2.21i 615	. . . . . . . . . 10 |- ( -oo < -oo -> -e B < +oo )
53	48, 52	syl6bi 162	. . . . . . . . 9 |- ( B = -oo -> ( -oo < B -> -e B < +oo ) )
54	53	imp 123	. . . . . . . 8 |- ( ( B = -oo /\ -oo < B ) -> -e B < +oo )
55	44, 47, 54	3jaoian 1251	. . . . . . 7 |- ( ( ( B e. RR \/ B = +oo \/ B = -oo ) /\ -oo < B ) -> -e B < +oo )
56	2, 55	sylanb 280	. . . . . 6 |- ( ( B e. RR* /\ -oo < B ) -> -e B < +oo )
57		xnegeq 9451	. . . . . . . 8 |- ( A = -oo -> -e A = -e -oo )
58		xnegmnf 9453	. . . . . . . 8 |- -e -oo = +oo
59	57, 58	syl6eq 2148	. . . . . . 7 |- ( A = -oo -> -e A = +oo )
60	59	breq2d 3887	. . . . . 6 |- ( A = -oo -> ( -e B < -e A <-> -e B < +oo ) )
61	56, 60	syl5ibr 155	. . . . 5 |- ( A = -oo -> ( ( B e. RR* /\ -oo < B ) -> -e B < -e A ) )
62	39, 61	sylbid 149	. . . 4 |- ( A = -oo -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
63	30, 37, 62	3jaoi 1249	. . 3 |- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
64	1, 63	sylbi 120	. 2 |- ( A e. RR* -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
65	64	3impib 1147	1 |- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ w3o 929   /\ w3a 930   = wceq 1299   e. wcel 1448   class class class wbr 3875   RRcr 7499   +oocpnf 7669   -oocmnf 7670   RR*cxr 7671   < clt 7672   -ucneg 7805   -ecxne 9397

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-iota 5024  df-fun 5061  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-sub 7806  df-neg 7807  df-xneg 9400

This theorem is referenced by:  xltneg  9460