Metamath Proof Explorer


Theorem metdscnlem

Description: Lemma for metdscn . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f F=xXsupranySxDy*<
metdscn.j J=MetOpenD
metdscn.c C=dist𝑠*
metdscn.k K=MetOpenC
metdscnlem.1 φD∞MetX
metdscnlem.2 φSX
metdscnlem.3 φAX
metdscnlem.4 φBX
metdscnlem.5 φR+
metdscnlem.6 φADB<R
Assertion metdscnlem φFA+𝑒FB<R

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 metdscn.j J=MetOpenD
3 metdscn.c C=dist𝑠*
4 metdscn.k K=MetOpenC
5 metdscnlem.1 φD∞MetX
6 metdscnlem.2 φSX
7 metdscnlem.3 φAX
8 metdscnlem.4 φBX
9 metdscnlem.5 φR+
10 metdscnlem.6 φADB<R
11 1 metdsf D∞MetXSXF:X0+∞
12 5 6 11 syl2anc φF:X0+∞
13 12 7 ffvelrnd φFA0+∞
14 eliccxr FA0+∞FA*
15 13 14 syl φFA*
16 12 8 ffvelrnd φFB0+∞
17 eliccxr FB0+∞FB*
18 16 17 syl φFB*
19 18 xnegcld φFB*
20 15 19 xaddcld φFA+𝑒FB*
21 xmetcl D∞MetXAXBXADB*
22 5 7 8 21 syl3anc φADB*
23 9 rpxrd φR*
24 1 metdstri D∞MetXSXAXBXFAADB+𝑒FB
25 5 6 7 8 24 syl22anc φFAADB+𝑒FB
26 elxrge0 FA0+∞FA*0FA
27 26 simprbi FA0+∞0FA
28 13 27 syl φ0FA
29 elxrge0 FB0+∞FB*0FB
30 29 simprbi FB0+∞0FB
31 16 30 syl φ0FB
32 ge0nemnf FB*0FBFB−∞
33 18 31 32 syl2anc φFB−∞
34 xmetge0 D∞MetXAXBX0ADB
35 5 7 8 34 syl3anc φ0ADB
36 xlesubadd FA*FB*ADB*0FAFB−∞0ADBFA+𝑒FBADBFAADB+𝑒FB
37 15 18 22 28 33 35 36 syl33anc φFA+𝑒FBADBFAADB+𝑒FB
38 25 37 mpbird φFA+𝑒FBADB
39 20 22 23 38 10 xrlelttrd φFA+𝑒FB<R