Metamath Proof Explorer

Theorem climbddf

Description: A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climbddf.1 
|- F/_ k F
climbddf.2 
|- Z = ( ZZ>= ` M )
Assertion climbddf 
|- ( ( 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 climbddf.1 
 |-  F/_ k F
2 climbddf.2 
 |-  Z = ( ZZ>= ` M )
3 simp1 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> M e. ZZ )
4 simp2 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> F e. dom ~~> )
5 nfv 
 |-  F/ j ( F ` k ) e. CC
6 nfcv 
 |-  F/_ k j
7 1 6 nffv 
 |-  F/_ k ( F ` j )
8 nfcv 
 |-  F/_ k CC
9 7 8 nfel 
 |-  F/ k ( F ` j ) e. CC
10 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
11 10 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
12 5 9 11 cbvralw 
 |-  ( A. k e. Z ( F ` k ) e. CC <-> A. j e. Z ( F ` j ) e. CC )
13 12 biimpi 
 |-  ( A. k e. Z ( F ` k ) e. CC -> A. j e. Z ( F ` j ) e. CC )
14 13 3ad2ant3 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> A. j e. Z ( F ` j ) e. CC )
15 2 climbdd 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. j e. Z ( F ` j ) e. CC ) -> E. x e. RR A. j e. Z ( abs ` ( F ` j ) ) <_ x )
16 3 4 14 15 syl3anc 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. j e. Z ( abs ` ( F ` j ) ) <_ x )
17 nfcv 
 |-  F/_ k abs
18 17 7 nffv 
 |-  F/_ k ( abs ` ( F ` j ) )
19 nfcv 
 |-  F/_ k <_
20 nfcv 
 |-  F/_ k x
21 18 19 20 nfbr 
 |-  F/ k ( abs ` ( F ` j ) ) <_ x
22 nfv 
 |-  F/ j ( abs ` ( F ` k ) ) <_ x
23 2fveq3 
 |-  ( j = k -> ( abs ` ( F ` j ) ) = ( abs ` ( F ` k ) ) )
24 23 breq1d 
 |-  ( j = k -> ( ( abs ` ( F ` j ) ) <_ x <-> ( abs ` ( F ` k ) ) <_ x ) )
25 21 22 24 cbvralw 
 |-  ( A. j e. Z ( abs ` ( F ` j ) ) <_ x <-> A. k e. Z ( abs ` ( F ` k ) ) <_ x )
26 25 rexbii 
 |-  ( E. x e. RR A. j e. Z ( abs ` ( F ` j ) ) <_ x <-> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
27 16 26 sylib 
 |-  ( ( 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 )