Metamath Proof Explorer

Theorem caurcvg2

Description: A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses caucvg.1 
|- Z = ( ZZ>= ` M )
caurcvg2.2 
|- ( ph -> F e. V )
caurcvg2.3 
|- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
Assertion caurcvg2 
|- ( ph -> F e. dom ~~> )

Proof

Step Hyp Ref Expression
1 caucvg.1 
 |-  Z = ( ZZ>= ` M )
2 caurcvg2.2 
 |-  ( ph -> F e. V )
3 caurcvg2.3 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
4 1rp 
 |-  1 e. RR+
5 4 ne0ii 
 |-  RR+ =/= (/)
6 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
7 5 3 6 sylancr 
 |-  ( ph -> E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
8 simpl 
 |-  ( ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( F ` k ) e. RR )
9 8 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR )
10 eqid 
 |-  ( ZZ>= ` j ) = ( ZZ>= ` j )
11 simprr 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR )
12 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
13 12 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. RR <-> ( F ` n ) e. RR ) )
14 13 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. RR )
15 11 14 sylan 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) /\ n e. ( ZZ>= ` j ) ) -> ( F ` n ) e. RR )
16 15 fmpttd 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) : ( ZZ>= ` j ) --> RR )
17 fveq2 
 |-  ( j = m -> ( ZZ>= ` j ) = ( ZZ>= ` m ) )
18 fveq2 
 |-  ( j = m -> ( F ` j ) = ( F ` m ) )
19 18 oveq2d 
 |-  ( j = m -> ( ( F ` k ) - ( F ` j ) ) = ( ( F ` k ) - ( F ` m ) ) )
20 19 fveq2d 
 |-  ( j = m -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) = ( abs ` ( ( F ` k ) - ( F ` m ) ) ) )
21 20 breq1d 
 |-  ( j = m -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
22 21 anbi2d 
 |-  ( j = m -> ( ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) )
23 17 22 raleqbidv 
 |-  ( j = m -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. k e. ( ZZ>= ` m ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) )
24 23 cbvrexvw 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> E. m e. Z A. k e. ( ZZ>= ` m ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
25 fveq2 
 |-  ( k = i -> ( F ` k ) = ( F ` i ) )
26 25 eleq1d 
 |-  ( k = i -> ( ( F ` k ) e. RR <-> ( F ` i ) e. RR ) )
27 25 fvoveq1d 
 |-  ( k = i -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) = ( abs ` ( ( F ` i ) - ( F ` m ) ) ) )
28 27 breq1d 
 |-  ( k = i -> ( ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x <-> ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
29 26 28 anbi12d 
 |-  ( k = i -> ( ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) <-> ( ( F ` i ) e. RR /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) ) )
30 29 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` m ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) <-> A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. RR /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
31 recn 
 |-  ( ( F ` i ) e. RR -> ( F ` i ) e. CC )
32 31 anim1i 
 |-  ( ( ( F ` i ) e. RR /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
33 32 ralimi 
 |-  ( A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. RR /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
34 30 33 sylbi 
 |-  ( A. k e. ( ZZ>= ` m ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) -> A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
35 34 reximi 
 |-  ( E. m e. Z A. k e. ( ZZ>= ` m ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
36 24 35 sylbi 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
37 36 ralimi 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
38 3 37 syl 
 |-  ( ph -> A. x e. RR+ E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
39 38 adantr 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> A. x e. RR+ E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
40 1 10 cau4 
 |-  ( j e. Z -> ( A. x e. RR+ E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) ) )
41 40 ad2antrl 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> ( A. x e. RR+ E. m e. Z A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) <-> A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) ) )
42 39 41 mpbid 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
43 simpr 
 |-  ( ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x )
44 10 uztrn2 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> i e. ( ZZ>= ` j ) )
45 fveq2 
 |-  ( n = i -> ( F ` n ) = ( F ` i ) )
46 eqid 
 |-  ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) = ( n e. ( ZZ>= ` j ) |-> ( F ` n ) )
47 fvex 
 |-  ( F ` i ) e. _V
48 45 46 47 fvmpt 
 |-  ( i e. ( ZZ>= ` j ) -> ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) = ( F ` i ) )
49 44 48 syl 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) = ( F ` i ) )
50 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
51 fvex 
 |-  ( F ` m ) e. _V
52 50 46 51 fvmpt 
 |-  ( m e. ( ZZ>= ` j ) -> ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) = ( F ` m ) )
53 52 adantr 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) = ( F ` m ) )
54 49 53 oveq12d 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) = ( ( F ` i ) - ( F ` m ) ) )
55 54 fveq2d 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) = ( abs ` ( ( F ` i ) - ( F ` m ) ) ) )
56 55 breq1d 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x <-> ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) )
57 43 56 imbitrrid 
 |-  ( ( m e. ( ZZ>= ` j ) /\ i e. ( ZZ>= ` m ) ) -> ( ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x ) )
58 57 ralimdva 
 |-  ( m e. ( ZZ>= ` j ) -> ( A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> A. i e. ( ZZ>= ` m ) ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x ) )
59 58 reximia 
 |-  ( E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x )
60 59 ralimi 
 |-  ( A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - ( F ` m ) ) ) < x ) -> A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x )
61 42 60 syl 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> A. x e. RR+ E. m e. ( ZZ>= ` j ) A. i e. ( ZZ>= ` m ) ( abs ` ( ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` i ) - ( ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ` m ) ) ) < x )
62 10 16 61 caurcvg 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) )
63 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
64 63 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
65 64 ad2antrl 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> j e. ZZ )
66 2 adantr 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> F e. V )
67 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
68 67 cbvmptv 
 |-  ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) = ( k e. ( ZZ>= ` j ) |-> ( F ` k ) )
69 10 68 climmpt 
 |-  ( ( j e. ZZ /\ F e. V ) -> ( F ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) <-> ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) ) )
70 65 66 69 syl2anc 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> ( F ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) <-> ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) ) )
71 62 70 mpbird 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> F ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) )
72 climrel 
 |-  Rel ~~>
73 72 releldmi 
 |-  ( F ~~> ( limsup ` ( n e. ( ZZ>= ` j ) |-> ( F ` n ) ) ) -> F e. dom ~~> )
74 71 73 syl 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR ) ) -> F e. dom ~~> )
75 74 expr 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. RR -> F e. dom ~~> ) )
76 9 75 syl5 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> F e. dom ~~> ) )
77 76 rexlimdva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> F e. dom ~~> ) )
78 77 rexlimdvw 
 |-  ( ph -> ( E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> F e. dom ~~> ) )
79 7 78 mpd 
 |-  ( ph -> F e. dom ~~> )