Metamath Proof Explorer


Theorem caures

Description: The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses caures.1 Z = M
caures.3 φ M
caures.4 φ D Met X
caures.5 φ F X 𝑝𝑚
Assertion caures φ F Cau D F Z Cau D

Proof

Step Hyp Ref Expression
1 caures.1 Z = M
2 caures.3 φ M
3 caures.4 φ D Met X
4 caures.5 φ F X 𝑝𝑚
5 1 uztrn2 j Z k j k Z
6 5 adantll φ j Z k j k Z
7 6 biantrurd φ j Z k j k dom F k Z k dom F
8 dmres dom F Z = Z dom F
9 8 elin2 k dom F Z k Z k dom F
10 7 9 bitr4di φ j Z k j k dom F k dom F Z
11 10 3anbi1d φ j Z k j k dom F F k X F k D F j < x k dom F Z F k X F k D F j < x
12 11 ralbidva φ j Z k j k dom F F k X F k D F j < x k j k dom F Z F k X F k D F j < x
13 12 rexbidva φ j Z k j k dom F F k X F k D F j < x j Z k j k dom F Z F k X F k D F j < x
14 13 ralbidv φ x + j Z k j k dom F F k X F k D F j < x x + j Z k j k dom F Z F k X F k D F j < x
15 4 biantrurd φ x + j Z k j k dom F F k X F k D F j < x F X 𝑝𝑚 x + j Z k j k dom F F k X F k D F j < x
16 elfvdm D Met X X dom Met
17 3 16 syl φ X dom Met
18 cnex V
19 ssid X X
20 uzssz M
21 zsscn
22 20 21 sstri M
23 1 22 eqsstri Z
24 pmss12g X X Z X dom Met V X 𝑝𝑚 Z X 𝑝𝑚
25 19 23 24 mpanl12 X dom Met V X 𝑝𝑚 Z X 𝑝𝑚
26 17 18 25 sylancl φ X 𝑝𝑚 Z X 𝑝𝑚
27 1 fvexi Z V
28 pmresg Z V F X 𝑝𝑚 F Z X 𝑝𝑚 Z
29 27 4 28 sylancr φ F Z X 𝑝𝑚 Z
30 26 29 sseldd φ F Z X 𝑝𝑚
31 30 biantrurd φ x + j Z k j k dom F Z F k X F k D F j < x F Z X 𝑝𝑚 x + j Z k j k dom F Z F k X F k D F j < x
32 14 15 31 3bitr3d φ F X 𝑝𝑚 x + j Z k j k dom F F k X F k D F j < x F Z X 𝑝𝑚 x + j Z k j k dom F Z F k X F k D F j < x
33 metxmet D Met X D ∞Met X
34 3 33 syl φ D ∞Met X
35 eqidd φ k Z F k = F k
36 eqidd φ j Z F j = F j
37 1 34 2 35 36 iscau4 φ F Cau D F X 𝑝𝑚 x + j Z k j k dom F F k X F k D F j < x
38 fvres k Z F Z k = F k
39 38 adantl φ k Z F Z k = F k
40 fvres j Z F Z j = F j
41 40 adantl φ j Z F Z j = F j
42 1 34 2 39 41 iscau4 φ F Z Cau D F Z X 𝑝𝑚 x + j Z k j k dom F Z F k X F k D F j < x
43 32 37 42 3bitr4d φ F Cau D F Z Cau D