Metamath Proof Explorer


Theorem clim2

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A , with more general quantifier restrictions than clim . (Contributed by NM, 6-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses clim2.1 Z=M
clim2.2 φM
clim2.3 φFV
clim2.4 φkZFk=B
Assertion clim2 φFAAx+jZkjBBA<x

Proof

Step Hyp Ref Expression
1 clim2.1 Z=M
2 clim2.2 φM
3 clim2.3 φFV
4 clim2.4 φkZFk=B
5 eqidd φkFk=Fk
6 3 5 clim φFAAx+jkjFkFkA<x
7 1 uztrn2 jZkjkZ
8 4 eleq1d φkZFkB
9 4 fvoveq1d φkZFkA=BA
10 9 breq1d φkZFkA<xBA<x
11 8 10 anbi12d φkZFkFkA<xBBA<x
12 7 11 sylan2 φjZkjFkFkA<xBBA<x
13 12 anassrs φjZkjFkFkA<xBBA<x
14 13 ralbidva φjZkjFkFkA<xkjBBA<x
15 14 rexbidva φjZkjFkFkA<xjZkjBBA<x
16 1 rexuz3 MjZkjFkFkA<xjkjFkFkA<x
17 2 16 syl φjZkjFkFkA<xjkjFkFkA<x
18 15 17 bitr3d φjZkjBBA<xjkjFkFkA<x
19 18 ralbidv φx+jZkjBBA<xx+jkjFkFkA<x
20 19 anbi2d φAx+jZkjBBA<xAx+jkjFkFkA<x
21 6 20 bitr4d φFAAx+jZkjBBA<x