Metamath Proof Explorer

Theorem climbdd

Description: A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 climcau.1 
 |-  Z = ( ZZ>= ` M )
2 simp3 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> A. k e. Z ( F ` k ) e. CC )
3 1 climcau 
 |-  ( ( M e. ZZ /\ F e. dom ~~> ) -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y )
4 3 3adant3 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y )
5 1 caubnd 
 |-  ( ( A. k e. Z ( F ` k ) e. CC /\ A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < y ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x )
6 2 4 5 syl2anc 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x )
7 r19.26 
 |-  ( A. k e. Z ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) <-> ( A. k e. Z ( F ` k ) e. CC /\ A. k e. Z ( abs ` ( F ` k ) ) < x ) )
8 simpr 
 |-  ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( F ` k ) e. CC )
9 8 abscld 
 |-  ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( abs ` ( F ` k ) ) e. RR )
10 simpllr 
 |-  ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> x e. RR )
11 ltle 
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( abs ` ( F ` k ) ) < x -> ( abs ` ( F ` k ) ) <_ x ) )
12 9 10 11 syl2anc 
 |-  ( ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) /\ ( F ` k ) e. CC ) -> ( ( abs ` ( F ` k ) ) < x -> ( abs ` ( F ` k ) ) <_ x ) )
13 12 expimpd 
 |-  ( ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) -> ( abs ` ( F ` k ) ) <_ x ) )
14 13 ralimdva 
 |-  ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) -> ( A. k e. Z ( ( F ` k ) e. CC /\ ( abs ` ( F ` k ) ) < x ) -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) )
15 7 14 syl5bir 
 |-  ( ( ( M e. ZZ /\ F e. dom ~~> ) /\ x e. RR ) -> ( ( A. k e. Z ( F ` k ) e. CC /\ A. k e. Z ( abs ` ( F ` k ) ) < x ) -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) )
16 15 exp4b 
 |-  ( ( M e. ZZ /\ F e. dom ~~> ) -> ( x e. RR -> ( A. k e. Z ( F ` k ) e. CC -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) ) )
17 16 com23 
 |-  ( ( M e. ZZ /\ F e. dom ~~> ) -> ( A. k e. Z ( F ` k ) e. CC -> ( x e. RR -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) ) )
18 17 3impia 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> ( x e. RR -> ( A. k e. Z ( abs ` ( F ` k ) ) < x -> A. k e. Z ( abs ` ( F ` k ) ) <_ x ) ) )
19 18 reximdvai 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> ( E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) < x -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x ) )
20 6 19 mpd 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )