Metamath Proof Explorer


Theorem ntrivcvgn0

Description: A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses ntrivcvgn0.1 Z=M
ntrivcvgn0.2 φM
ntrivcvgn0.3 φseqM×FX
ntrivcvgn0.4 φX0
Assertion ntrivcvgn0 φnZyy0seqn×Fy

Proof

Step Hyp Ref Expression
1 ntrivcvgn0.1 Z=M
2 ntrivcvgn0.2 φM
3 ntrivcvgn0.3 φseqM×FX
4 ntrivcvgn0.4 φX0
5 2 uzidd φMM
6 5 1 eleqtrrdi φMZ
7 climrel Rel
8 7 brrelex2i seqM×FXXV
9 3 8 syl φXV
10 4 3 jca φX0seqM×FX
11 neeq1 y=Xy0X0
12 breq2 y=XseqM×FyseqM×FX
13 11 12 anbi12d y=Xy0seqM×FyX0seqM×FX
14 9 10 13 spcedv φyy0seqM×Fy
15 seqeq1 n=Mseqn×F=seqM×F
16 15 breq1d n=Mseqn×FyseqM×Fy
17 16 anbi2d n=My0seqn×Fyy0seqM×Fy
18 17 exbidv n=Myy0seqn×Fyyy0seqM×Fy
19 18 rspcev MZyy0seqM×FynZyy0seqn×Fy
20 6 14 19 syl2anc φnZyy0seqn×Fy