Metamath Proof Explorer

Theorem xrsdsreclblem

Description: Lemma for xrsdsreclb . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrsds.d 
|- D = ( dist ` RR*s )
Assertion xrsdsreclblem 
|- ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ A <_ B ) -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d 
 |-  D = ( dist ` RR*s )
2 necom 
 |-  ( A =/= B <-> B =/= A )
3 xrleltne 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B <-> B =/= A ) )
4 mnfxr 
 |-  -oo e. RR*
5 4 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -oo e. RR* )
6 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> A e. RR* )
7 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> B e. RR* )
8 pnfnre 
 |-  +oo e/ RR
9 8 neli 
 |-  -. +oo e. RR
10 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
11 6 10 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -oo <_ A )
12 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> A < B )
13 5 6 7 11 12 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -oo < B )
14 xrltne 
 |-  ( ( -oo e. RR* /\ B e. RR* /\ -oo < B ) -> B =/= -oo )
15 5 7 13 14 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> B =/= -oo )
16 xaddpnf1 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
17 7 15 16 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( B +e +oo ) = +oo )
18 17 eleq1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( ( B +e +oo ) e. RR <-> +oo e. RR ) )
19 9 18 mtbiri 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -. ( B +e +oo ) e. RR )
20 ngtmnft 
 |-  ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
21 6 20 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( A = -oo <-> -. -oo < A ) )
22 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( B +e -e A ) e. RR )
23 xnegeq 
 |-  ( A = -oo -> -e A = -e -oo )
24 xnegmnf 
 |-  -e -oo = +oo
25 23 24 eqtrdi 
 |-  ( A = -oo -> -e A = +oo )
26 25 oveq2d 
 |-  ( A = -oo -> ( B +e -e A ) = ( B +e +oo ) )
27 26 eleq1d 
 |-  ( A = -oo -> ( ( B +e -e A ) e. RR <-> ( B +e +oo ) e. RR ) )
28 22 27 syl5ibcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( A = -oo -> ( B +e +oo ) e. RR ) )
29 21 28 sylbird 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( -. -oo < A -> ( B +e +oo ) e. RR ) )
30 19 29 mt3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -oo < A )
31 xrre2 
 |-  ( ( ( -oo e. RR* /\ A e. RR* /\ B e. RR* ) /\ ( -oo < A /\ A < B ) ) -> A e. RR )
32 5 6 7 30 12 31 syl32anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> A e. RR )
33 pnfxr 
 |-  +oo e. RR*
34 33 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> +oo e. RR* )
35 6 xnegcld 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -e A e. RR* )
36 xnegpnf 
 |-  -e +oo = -oo
37 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
38 7 37 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> B <_ +oo )
39 6 7 34 12 38 xrltletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> A < +oo )
40 xltnegi 
 |-  ( ( A e. RR* /\ +oo e. RR* /\ A < +oo ) -> -e +oo < -e A )
41 6 34 39 40 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -e +oo < -e A )
42 36 41 eqbrtrrid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -oo < -e A )
43 xrltne 
 |-  ( ( -oo e. RR* /\ -e A e. RR* /\ -oo < -e A ) -> -e A =/= -oo )
44 5 35 42 43 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -e A =/= -oo )
45 xaddpnf2 
 |-  ( ( -e A e. RR* /\ -e A =/= -oo ) -> ( +oo +e -e A ) = +oo )
46 35 44 45 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( +oo +e -e A ) = +oo )
47 46 eleq1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( ( +oo +e -e A ) e. RR <-> +oo e. RR ) )
48 9 47 mtbiri 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> -. ( +oo +e -e A ) e. RR )
49 nltpnft 
 |-  ( B e. RR* -> ( B = +oo <-> -. B < +oo ) )
50 7 49 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( B = +oo <-> -. B < +oo ) )
51 oveq1 
 |-  ( B = +oo -> ( B +e -e A ) = ( +oo +e -e A ) )
52 51 eleq1d 
 |-  ( B = +oo -> ( ( B +e -e A ) e. RR <-> ( +oo +e -e A ) e. RR ) )
53 22 52 syl5ibcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( B = +oo -> ( +oo +e -e A ) e. RR ) )
54 50 53 sylbird 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( -. B < +oo -> ( +oo +e -e A ) e. RR ) )
55 48 54 mt3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> B < +oo )
56 xrre2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) /\ ( A < B /\ B < +oo ) ) -> B e. RR )
57 6 7 34 12 55 56 syl32anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> B e. RR )
58 32 57 jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( B +e -e A ) e. RR ) -> ( A e. RR /\ B e. RR ) )
59 58 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) )
60 59 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
61 60 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A < B -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
62 3 61 sylbird 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( B =/= A -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
63 2 62 biimtrid 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A =/= B -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
64 63 3exp 
 |-  ( A e. RR* -> ( B e. RR* -> ( A <_ B -> ( A =/= B -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) ) ) )
65 64 com34 
 |-  ( A e. RR* -> ( B e. RR* -> ( A =/= B -> ( A <_ B -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) ) ) ) )
66 65 3imp1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ A <_ B ) -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) )