Metamath Proof Explorer

Theorem climcl

Description: Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion climcl F A A


Step Hyp Ref Expression
1 climrel Rel
2 1 brrelex1i F A F V
3 eqidd F A k F k = F k
4 2 3 clim F A F A A x + j k j F k F k A < x
5 4 ibi F A A x + j k j F k F k A < x
6 5 simpld F A A