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 )