Metamath Proof Explorer

Theorem iscmet3lem1

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses iscmet3.1 
|- Z = ( ZZ>= ` M )
iscmet3.2 
|- J = ( MetOpen ` D )
iscmet3.3 
|- ( ph -> M e. ZZ )
iscmet3.4 
|- ( ph -> D e. ( Met ` X ) )
iscmet3.6 
|- ( ph -> F : Z --> X )
iscmet3.9 
|- ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
iscmet3.10 
|- ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
Assertion iscmet3lem1 
|- ( ph -> F e. ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 iscmet3.1 
 |-  Z = ( ZZ>= ` M )
2 iscmet3.2 
 |-  J = ( MetOpen ` D )
3 iscmet3.3 
 |-  ( ph -> M e. ZZ )
4 iscmet3.4 
 |-  ( ph -> D e. ( Met ` X ) )
5 iscmet3.6 
 |-  ( ph -> F : Z --> X )
6 iscmet3.9 
 |-  ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
7 iscmet3.10 
 |-  ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
8 1 iscmet3lem3 
 |-  ( ( M e. ZZ /\ r e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < r )
9 3 8 sylan 
 |-  ( ( ph /\ r e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < r )
10 1 r19.2uz 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < r -> E. k e. Z ( ( 1 / 2 ) ^ k ) < r )
11 9 10 syl 
 |-  ( ( ph /\ r e. RR+ ) -> E. k e. Z ( ( 1 / 2 ) ^ k ) < r )
12 fveq2 
 |-  ( n = k -> ( S ` n ) = ( S ` k ) )
13 12 eleq2d 
 |-  ( n = k -> ( ( F ` k ) e. ( S ` n ) <-> ( F ` k ) e. ( S ` k ) ) )
14 7 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
15 simpl 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> k e. Z )
16 15 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> k e. Z )
17 rsp 
 |-  ( A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) -> ( k e. Z -> A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) ) )
18 14 16 17 sylc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
19 16 1 eleqtrdi 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> k e. ( ZZ>= ` M ) )
20 eluzfz2 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ( M ... k ) )
21 19 20 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> k e. ( M ... k ) )
22 13 18 21 rspcdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( F ` k ) e. ( S ` k ) )
23 12 eleq2d 
 |-  ( n = k -> ( ( F ` j ) e. ( S ` n ) <-> ( F ` j ) e. ( S ` k ) ) )
24 oveq2 
 |-  ( k = j -> ( M ... k ) = ( M ... j ) )
25 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
26 25 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. ( S ` n ) <-> ( F ` j ) e. ( S ` n ) ) )
27 24 26 raleqbidv 
 |-  ( k = j -> ( A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) <-> A. n e. ( M ... j ) ( F ` j ) e. ( S ` n ) ) )
28 1 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
29 28 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> j e. Z )
30 27 14 29 rspcdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> A. n e. ( M ... j ) ( F ` j ) e. ( S ` n ) )
31 simprr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> j e. ( ZZ>= ` k ) )
32 elfzuzb 
 |-  ( k e. ( M ... j ) <-> ( k e. ( ZZ>= ` M ) /\ j e. ( ZZ>= ` k ) ) )
33 19 31 32 sylanbrc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> k e. ( M ... j ) )
34 23 30 33 rspcdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( F ` j ) e. ( S ` k ) )
35 6 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
36 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
37 36 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
38 37 ad2antrl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> k e. ZZ )
39 rsp 
 |-  ( A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) -> ( k e. ZZ -> A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
40 35 38 39 sylc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
41 oveq1 
 |-  ( u = ( F ` k ) -> ( u D v ) = ( ( F ` k ) D v ) )
42 41 breq1d 
 |-  ( u = ( F ` k ) -> ( ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> ( ( F ` k ) D v ) < ( ( 1 / 2 ) ^ k ) ) )
43 oveq2 
 |-  ( v = ( F ` j ) -> ( ( F ` k ) D v ) = ( ( F ` k ) D ( F ` j ) ) )
44 43 breq1d 
 |-  ( v = ( F ` j ) -> ( ( ( F ` k ) D v ) < ( ( 1 / 2 ) ^ k ) <-> ( ( F ` k ) D ( F ` j ) ) < ( ( 1 / 2 ) ^ k ) ) )
45 42 44 rspc2va 
 |-  ( ( ( ( F ` k ) e. ( S ` k ) /\ ( F ` j ) e. ( S ` k ) ) /\ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) -> ( ( F ` k ) D ( F ` j ) ) < ( ( 1 / 2 ) ^ k ) )
46 22 34 40 45 syl21anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) D ( F ` j ) ) < ( ( 1 / 2 ) ^ k ) )
47 4 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> D e. ( Met ` X ) )
48 5 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> F : Z --> X )
49 ffvelrn 
 |-  ( ( F : Z --> X /\ k e. Z ) -> ( F ` k ) e. X )
50 48 15 49 syl2an 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( F ` k ) e. X )
51 ffvelrn 
 |-  ( ( F : Z --> X /\ j e. Z ) -> ( F ` j ) e. X )
52 48 28 51 syl2an 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( F ` j ) e. X )
53 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` k ) D ( F ` j ) ) e. RR )
54 47 50 52 53 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( F ` k ) D ( F ` j ) ) e. RR )
55 1rp 
 |-  1 e. RR+
56 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
57 55 56 ax-mp 
 |-  ( 1 / 2 ) e. RR+
58 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ k e. ZZ ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
59 57 38 58 sylancr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
60 59 rpred 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( 1 / 2 ) ^ k ) e. RR )
61 rpre 
 |-  ( r e. RR+ -> r e. RR )
62 61 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> r e. RR )
63 lttr 
 |-  ( ( ( ( F ` k ) D ( F ` j ) ) e. RR /\ ( ( 1 / 2 ) ^ k ) e. RR /\ r e. RR ) -> ( ( ( ( F ` k ) D ( F ` j ) ) < ( ( 1 / 2 ) ^ k ) /\ ( ( 1 / 2 ) ^ k ) < r ) -> ( ( F ` k ) D ( F ` j ) ) < r ) )
64 54 60 62 63 syl3anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) < ( ( 1 / 2 ) ^ k ) /\ ( ( 1 / 2 ) ^ k ) < r ) -> ( ( F ` k ) D ( F ` j ) ) < r ) )
65 46 64 mpand 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ j e. ( ZZ>= ` k ) ) ) -> ( ( ( 1 / 2 ) ^ k ) < r -> ( ( F ` k ) D ( F ` j ) ) < r ) )
66 65 anassrs 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( 1 / 2 ) ^ k ) < r -> ( ( F ` k ) D ( F ` j ) ) < r ) )
67 66 ralrimdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( 1 / 2 ) ^ k ) < r -> A. j e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` j ) ) < r ) )
68 67 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. k e. Z ( ( 1 / 2 ) ^ k ) < r -> E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` j ) ) < r ) )
69 11 68 mpd 
 |-  ( ( ph /\ r e. RR+ ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` j ) ) < r )
70 69 ralrimiva 
 |-  ( ph -> A. r e. RR+ E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` j ) ) < r )
71 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
72 4 71 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
73 eqidd 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = ( F ` j ) )
74 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
75 1 72 3 73 74 5 iscauf 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> A. r e. RR+ E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` j ) ) < r ) )
76 70 75 mpbird 
 |-  ( ph -> F e. ( Cau ` D ) )