This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xltnegi

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

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

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
3 ltneg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -u B < -u A ) )
4 rexneg 
 |-  ( B e. RR -> -e B = -u B )
5 rexneg 
 |-  ( A e. RR -> -e A = -u A )
6 4 5 breqan12rd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -e B < -e A <-> -u B < -u A ) )
7 3 6 bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -e B < -e A ) )
8 7 biimpd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B -> -e B < -e A ) )
9 xnegeq 
 |-  ( B = +oo -> -e B = -e +oo )
10 xnegpnf 
 |-  -e +oo = -oo
11 9 10 eqtrdi 
 |-  ( B = +oo -> -e B = -oo )
12 11 adantl 
 |-  ( ( A e. RR /\ B = +oo ) -> -e B = -oo )
13 renegcl 
 |-  ( A e. RR -> -u A e. RR )
14 5 13 eqeltrd 
 |-  ( A e. RR -> -e A e. RR )
15 14 mnfltd 
 |-  ( A e. RR -> -oo < -e A )
16 15 adantr 
 |-  ( ( A e. RR /\ B = +oo ) -> -oo < -e A )
17 12 16 eqbrtrd 
 |-  ( ( A e. RR /\ B = +oo ) -> -e B < -e A )
18 17 a1d 
 |-  ( ( A e. RR /\ B = +oo ) -> ( A < B -> -e B < -e A ) )
19 simpr 
 |-  ( ( A e. RR /\ B = -oo ) -> B = -oo )
20 19 breq2d 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < B <-> A < -oo ) )
21 rexr 
 |-  ( A e. RR -> A e. RR* )
22 nltmnf 
 |-  ( A e. RR* -> -. A < -oo )
23 21 22 syl 
 |-  ( A e. RR -> -. A < -oo )
24 23 adantr 
 |-  ( ( A e. RR /\ B = -oo ) -> -. A < -oo )
25 24 pm2.21d 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < -oo -> -e B < -e A ) )
26 20 25 sylbid 
 |-  ( ( A e. RR /\ B = -oo ) -> ( A < B -> -e B < -e A ) )
27 8 18 26 3jaodan 
 |-  ( ( A e. RR /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A < B -> -e B < -e A ) )
28 2 27 sylan2b 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A < B -> -e B < -e A ) )
29 28 expimpd 
 |-  ( A e. RR -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
30 simpl 
 |-  ( ( A = +oo /\ B e. RR* ) -> A = +oo )
31 30 breq1d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B <-> +oo < B ) )
32 pnfnlt 
 |-  ( B e. RR* -> -. +oo < B )
33 32 adantl 
 |-  ( ( A = +oo /\ B e. RR* ) -> -. +oo < B )
34 33 pm2.21d 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( +oo < B -> -e B < -e A ) )
35 31 34 sylbid 
 |-  ( ( A = +oo /\ B e. RR* ) -> ( A < B -> -e B < -e A ) )
36 35 expimpd 
 |-  ( A = +oo -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
37 breq1 
 |-  ( A = -oo -> ( A < B <-> -oo < B ) )
38 37 anbi2d 
 |-  ( A = -oo -> ( ( B e. RR* /\ A < B ) <-> ( B e. RR* /\ -oo < B ) ) )
39 renegcl 
 |-  ( B e. RR -> -u B e. RR )
40 4 39 eqeltrd 
 |-  ( B e. RR -> -e B e. RR )
41 40 adantr 
 |-  ( ( B e. RR /\ -oo < B ) -> -e B e. RR )
42 41 ltpnfd 
 |-  ( ( B e. RR /\ -oo < B ) -> -e B < +oo )
43 11 adantr 
 |-  ( ( B = +oo /\ -oo < B ) -> -e B = -oo )
44 mnfltpnf 
 |-  -oo < +oo
45 43 44 eqbrtrdi 
 |-  ( ( B = +oo /\ -oo < B ) -> -e B < +oo )
46 breq2 
 |-  ( B = -oo -> ( -oo < B <-> -oo < -oo ) )
47 mnfxr 
 |-  -oo e. RR*
48 nltmnf 
 |-  ( -oo e. RR* -> -. -oo < -oo )
49 47 48 ax-mp 
 |-  -. -oo < -oo
50 49 pm2.21i 
 |-  ( -oo < -oo -> -e B < +oo )
51 46 50 biimtrdi 
 |-  ( B = -oo -> ( -oo < B -> -e B < +oo ) )
52 51 imp 
 |-  ( ( B = -oo /\ -oo < B ) -> -e B < +oo )
53 42 45 52 3jaoian 
 |-  ( ( ( B e. RR \/ B = +oo \/ B = -oo ) /\ -oo < B ) -> -e B < +oo )
54 2 53 sylanb 
 |-  ( ( B e. RR* /\ -oo < B ) -> -e B < +oo )
55 xnegeq 
 |-  ( A = -oo -> -e A = -e -oo )
56 xnegmnf 
 |-  -e -oo = +oo
57 55 56 eqtrdi 
 |-  ( A = -oo -> -e A = +oo )
58 57 breq2d 
 |-  ( A = -oo -> ( -e B < -e A <-> -e B < +oo ) )
59 54 58 imbitrrid 
 |-  ( A = -oo -> ( ( B e. RR* /\ -oo < B ) -> -e B < -e A ) )
60 38 59 sylbid 
 |-  ( A = -oo -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
61 29 36 60 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
62 1 61 sylbi 
 |-  ( A e. RR* -> ( ( B e. RR* /\ A < B ) -> -e B < -e A ) )
63 62 3impib 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )