Metamath Proof Explorer


Theorem serclim0

Description: The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008) (Proof shortened by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion serclim0 MseqM+M×00

Proof

Step Hyp Ref Expression
1 eqid M=M
2 1 ser0f MseqM+M×0=M×0
3 0cn 0
4 ssid MM
5 fvex MV
6 4 5 climconst2 0MM×00
7 3 6 mpan MM×00
8 2 7 eqbrtrd MseqM+M×00