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 biimtrrid 
 |-  ( 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 )