Metamath Proof Explorer


Theorem xrsdsreclblem

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

Ref Expression
Hypothesis xrsds.d D = dist 𝑠 *
Assertion xrsdsreclblem A * B * A B A B B + 𝑒 A A B

Proof

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