Metamath Proof Explorer


Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climd.1 kφ
climd.2 _kF
climd.3 Z=M
climd.4 φM
climd.5 φFA
climd.6 φkZFk=B
climd.7 φX+
Assertion climd φjZkjBBA<X

Proof

Step Hyp Ref Expression
1 climd.1 kφ
2 climd.2 _kF
3 climd.3 Z=M
4 climd.4 φM
5 climd.5 φFA
6 climd.6 φkZFk=B
7 climd.7 φX+
8 climrel Rel
9 8 brrelex1i FAFV
10 5 9 syl φFV
11 1 2 3 4 10 6 clim2f2 φFAAx+jZkjBBA<x
12 5 11 mpbid φAx+jZkjBBA<x
13 12 simprd φx+jZkjBBA<x
14 breq2 x=XBA<xBA<X
15 14 anbi2d x=XBBA<xBBA<X
16 15 rexralbidv x=XjZkjBBA<xjZkjBBA<X
17 16 rspcva X+x+jZkjBBA<xjZkjBBA<X
18 7 13 17 syl2anc φjZkjBBA<X