Metamath Proof Explorer


Theorem climcau

Description: A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of Gleason p. 180 (necessity part). (Contributed by NM, 16-Apr-2005) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypothesis climcau.1
|- Z = ( ZZ>= ` M )
Assertion climcau
|- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )

Proof

Step Hyp Ref Expression
1 climcau.1
 |-  Z = ( ZZ>= ` M )
2 df-br
 |-  ( F ~~> y <-> <. F , y >. e. ~~> )
3 simpll
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> M e. ZZ )
4 rphalfcl
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
5 4 adantl
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
6 eqidd
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
7 simplr
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> F ~~> y )
8 1 3 5 6 7 climi
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) )
9 eluzelz
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
10 uzid
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
11 9 10 syl
 |-  ( j e. ( ZZ>= ` M ) -> j e. ( ZZ>= ` j ) )
12 11 1 eleq2s
 |-  ( j e. Z -> j e. ( ZZ>= ` j ) )
13 12 adantl
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> j e. ( ZZ>= ` j ) )
14 fveq2
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
15 14 eleq1d
 |-  ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
16 14 fvoveq1d
 |-  ( k = j -> ( abs ` ( ( F ` k ) - y ) ) = ( abs ` ( ( F ` j ) - y ) ) )
17 16 breq1d
 |-  ( k = j -> ( ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) <-> ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) )
18 15 17 anbi12d
 |-  ( k = j -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) <-> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) )
19 18 rspcv
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) )
20 13 19 syl
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) )
21 rpre
 |-  ( x e. RR+ -> x e. RR )
22 21 ad2antlr
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> x e. RR )
23 simpllr
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> F ~~> y )
24 climcl
 |-  ( F ~~> y -> y e. CC )
25 23 24 syl
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> y e. CC )
26 simprl
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( F ` k ) e. CC )
27 simplrl
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( F ` j ) e. CC )
28 simpllr
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> y e. CC )
29 simplll
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> x e. RR )
30 simprr
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) )
31 28 27 abssubd
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( y - ( F ` j ) ) ) = ( abs ` ( ( F ` j ) - y ) ) )
32 simplrr
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) )
33 31 32 eqbrtrd
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( y - ( F ` j ) ) ) < ( x / 2 ) )
34 26 27 28 29 30 33 abs3lemd
 |-  ( ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
35 34 ex
 |-  ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
36 35 ralimdv
 |-  ( ( ( x e. RR /\ y e. CC ) /\ ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
37 36 ex
 |-  ( ( x e. RR /\ y e. CC ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
38 37 com23
 |-  ( ( x e. RR /\ y e. CC ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
39 22 25 38 syl2anc
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> ( ( ( F ` j ) e. CC /\ ( abs ` ( ( F ` j ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
40 20 39 mpdd
 |-  ( ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
41 40 reximdva
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - y ) ) < ( x / 2 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
42 8 41 mpd
 |-  ( ( ( M e. ZZ /\ F ~~> y ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
43 42 ralrimiva
 |-  ( ( M e. ZZ /\ F ~~> y ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
44 43 ex
 |-  ( M e. ZZ -> ( F ~~> y -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
45 2 44 syl5bir
 |-  ( M e. ZZ -> ( <. F , y >. e. ~~> -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
46 45 exlimdv
 |-  ( M e. ZZ -> ( E. y <. F , y >. e. ~~> -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
47 eldm2g
 |-  ( F e. dom ~~> -> ( F e. dom ~~> <-> E. y <. F , y >. e. ~~> ) )
48 47 ibi
 |-  ( F e. dom ~~> -> E. y <. F , y >. e. ~~> )
49 46 48 impel
 |-  ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )