Metamath Proof Explorer


Theorem caubl

Description: Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses caubl.2 φ D ∞Met X
caubl.3 φ F : X × +
caubl.4 φ n ball D F n + 1 ball D F n
caubl.5 φ r + n 2 nd F n < r
Assertion caubl φ 1 st F Cau D

Proof

Step Hyp Ref Expression
1 caubl.2 φ D ∞Met X
2 caubl.3 φ F : X × +
3 caubl.4 φ n ball D F n + 1 ball D F n
4 caubl.5 φ r + n 2 nd F n < r
5 2fveq3 r = n ball D F r = ball D F n
6 5 sseq1d r = n ball D F r ball D F n ball D F n ball D F n
7 6 imbi2d r = n φ n ball D F r ball D F n φ n ball D F n ball D F n
8 2fveq3 r = k ball D F r = ball D F k
9 8 sseq1d r = k ball D F r ball D F n ball D F k ball D F n
10 9 imbi2d r = k φ n ball D F r ball D F n φ n ball D F k ball D F n
11 2fveq3 r = k + 1 ball D F r = ball D F k + 1
12 11 sseq1d r = k + 1 ball D F r ball D F n ball D F k + 1 ball D F n
13 12 imbi2d r = k + 1 φ n ball D F r ball D F n φ n ball D F k + 1 ball D F n
14 ssid ball D F n ball D F n
15 14 2a1i n φ n ball D F n ball D F n
16 eluznn n k n k
17 fvoveq1 n = k F n + 1 = F k + 1
18 17 fveq2d n = k ball D F n + 1 = ball D F k + 1
19 2fveq3 n = k ball D F n = ball D F k
20 18 19 sseq12d n = k ball D F n + 1 ball D F n ball D F k + 1 ball D F k
21 20 rspccva n ball D F n + 1 ball D F n k ball D F k + 1 ball D F k
22 3 16 21 syl2an φ n k n ball D F k + 1 ball D F k
23 22 anassrs φ n k n ball D F k + 1 ball D F k
24 sstr2 ball D F k + 1 ball D F k ball D F k ball D F n ball D F k + 1 ball D F n
25 23 24 syl φ n k n ball D F k ball D F n ball D F k + 1 ball D F n
26 25 expcom k n φ n ball D F k ball D F n ball D F k + 1 ball D F n
27 26 a2d k n φ n ball D F k ball D F n φ n ball D F k + 1 ball D F n
28 7 10 13 10 15 27 uzind4 k n φ n ball D F k ball D F n
29 28 com12 φ n k n ball D F k ball D F n
30 29 ad2ant2r φ r + n 2 nd F n < r k n ball D F k ball D F n
31 relxp Rel X × +
32 2 ad3antrrr φ r + n 2 nd F n < r k n F : X × +
33 simplrl φ r + n 2 nd F n < r k n n
34 32 33 ffvelrnd φ r + n 2 nd F n < r k n F n X × +
35 1st2nd Rel X × + F n X × + F n = 1 st F n 2 nd F n
36 31 34 35 sylancr φ r + n 2 nd F n < r k n F n = 1 st F n 2 nd F n
37 36 fveq2d φ r + n 2 nd F n < r k n ball D F n = ball D 1 st F n 2 nd F n
38 df-ov 1 st F n ball D 2 nd F n = ball D 1 st F n 2 nd F n
39 37 38 eqtr4di φ r + n 2 nd F n < r k n ball D F n = 1 st F n ball D 2 nd F n
40 1 ad3antrrr φ r + n 2 nd F n < r k n D ∞Met X
41 xp1st F n X × + 1 st F n X
42 34 41 syl φ r + n 2 nd F n < r k n 1 st F n X
43 xp2nd F n X × + 2 nd F n +
44 34 43 syl φ r + n 2 nd F n < r k n 2 nd F n +
45 44 rpxrd φ r + n 2 nd F n < r k n 2 nd F n *
46 simpllr φ r + n 2 nd F n < r k n r +
47 46 rpxrd φ r + n 2 nd F n < r k n r *
48 simplrr φ r + n 2 nd F n < r k n 2 nd F n < r
49 rpre 2 nd F n + 2 nd F n
50 rpre r + r
51 ltle 2 nd F n r 2 nd F n < r 2 nd F n r
52 49 50 51 syl2an 2 nd F n + r + 2 nd F n < r 2 nd F n r
53 44 46 52 syl2anc φ r + n 2 nd F n < r k n 2 nd F n < r 2 nd F n r
54 48 53 mpd φ r + n 2 nd F n < r k n 2 nd F n r
55 ssbl D ∞Met X 1 st F n X 2 nd F n * r * 2 nd F n r 1 st F n ball D 2 nd F n 1 st F n ball D r
56 40 42 45 47 54 55 syl221anc φ r + n 2 nd F n < r k n 1 st F n ball D 2 nd F n 1 st F n ball D r
57 39 56 eqsstrd φ r + n 2 nd F n < r k n ball D F n 1 st F n ball D r
58 sstr2 ball D F k ball D F n ball D F n 1 st F n ball D r ball D F k 1 st F n ball D r
59 57 58 syl5com φ r + n 2 nd F n < r k n ball D F k ball D F n ball D F k 1 st F n ball D r
60 simprl φ r + n 2 nd F n < r n
61 60 16 sylan φ r + n 2 nd F n < r k n k
62 32 61 ffvelrnd φ r + n 2 nd F n < r k n F k X × +
63 xp1st F k X × + 1 st F k X
64 62 63 syl φ r + n 2 nd F n < r k n 1 st F k X
65 xp2nd F k X × + 2 nd F k +
66 62 65 syl φ r + n 2 nd F n < r k n 2 nd F k +
67 blcntr D ∞Met X 1 st F k X 2 nd F k + 1 st F k 1 st F k ball D 2 nd F k
68 40 64 66 67 syl3anc φ r + n 2 nd F n < r k n 1 st F k 1 st F k ball D 2 nd F k
69 1st2nd Rel X × + F k X × + F k = 1 st F k 2 nd F k
70 31 62 69 sylancr φ r + n 2 nd F n < r k n F k = 1 st F k 2 nd F k
71 70 fveq2d φ r + n 2 nd F n < r k n ball D F k = ball D 1 st F k 2 nd F k
72 df-ov 1 st F k ball D 2 nd F k = ball D 1 st F k 2 nd F k
73 71 72 eqtr4di φ r + n 2 nd F n < r k n ball D F k = 1 st F k ball D 2 nd F k
74 68 73 eleqtrrd φ r + n 2 nd F n < r k n 1 st F k ball D F k
75 ssel ball D F k 1 st F n ball D r 1 st F k ball D F k 1 st F k 1 st F n ball D r
76 59 74 75 syl6ci φ r + n 2 nd F n < r k n ball D F k ball D F n 1 st F k 1 st F n ball D r
77 elbl2 D ∞Met X r * 1 st F n X 1 st F k X 1 st F k 1 st F n ball D r 1 st F n D 1 st F k < r
78 40 47 42 64 77 syl22anc φ r + n 2 nd F n < r k n 1 st F k 1 st F n ball D r 1 st F n D 1 st F k < r
79 76 78 sylibd φ r + n 2 nd F n < r k n ball D F k ball D F n 1 st F n D 1 st F k < r
80 79 ex φ r + n 2 nd F n < r k n ball D F k ball D F n 1 st F n D 1 st F k < r
81 30 80 mpdd φ r + n 2 nd F n < r k n 1 st F n D 1 st F k < r
82 81 ralrimiv φ r + n 2 nd F n < r k n 1 st F n D 1 st F k < r
83 82 expr φ r + n 2 nd F n < r k n 1 st F n D 1 st F k < r
84 83 reximdva φ r + n 2 nd F n < r n k n 1 st F n D 1 st F k < r
85 84 ralimdva φ r + n 2 nd F n < r r + n k n 1 st F n D 1 st F k < r
86 4 85 mpd φ r + n k n 1 st F n D 1 st F k < r
87 nnuz = 1
88 1zzd φ 1
89 fvco3 F : X × + k 1 st F k = 1 st F k
90 2 89 sylan φ k 1 st F k = 1 st F k
91 fvco3 F : X × + n 1 st F n = 1 st F n
92 2 91 sylan φ n 1 st F n = 1 st F n
93 1stcof F : X × + 1 st F : X
94 2 93 syl φ 1 st F : X
95 87 1 88 90 92 94 iscauf φ 1 st F Cau D r + n k n 1 st F n D 1 st F k < r
96 86 95 mpbird φ 1 st F Cau D