This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( ZZ>= ` M )
ntrivcvgn0.2 
|- ( ph -> M e. ZZ )
ntrivcvgn0.3 
|- ( ph -> seq M ( x. , F ) ~~> X )
ntrivcvgn0.4 
|- ( ph -> X =/= 0 )
Assertion ntrivcvgn0 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )

Proof

Step Hyp Ref Expression
1 ntrivcvgn0.1 
 |-  Z = ( ZZ>= ` M )
2 ntrivcvgn0.2 
 |-  ( ph -> M e. ZZ )
3 ntrivcvgn0.3 
 |-  ( ph -> seq M ( x. , F ) ~~> X )
4 ntrivcvgn0.4 
 |-  ( ph -> X =/= 0 )
5 2 uzidd 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
6 5 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
7 climrel 
 |-  Rel ~~>
8 7 brrelex2i 
 |-  ( seq M ( x. , F ) ~~> X -> X e. _V )
9 3 8 syl 
 |-  ( ph -> X e. _V )
10 4 3 jca 
 |-  ( ph -> ( X =/= 0 /\ seq M ( x. , F ) ~~> X ) )
11 neeq1 
 |-  ( y = X -> ( y =/= 0 <-> X =/= 0 ) )
12 breq2 
 |-  ( y = X -> ( seq M ( x. , F ) ~~> y <-> seq M ( x. , F ) ~~> X ) )
13 11 12 anbi12d 
 |-  ( y = X -> ( ( y =/= 0 /\ seq M ( x. , F ) ~~> y ) <-> ( X =/= 0 /\ seq M ( x. , F ) ~~> X ) ) )
14 9 10 13 spcedv 
 |-  ( ph -> E. y ( y =/= 0 /\ seq M ( x. , F ) ~~> y ) )
15 seqeq1 
 |-  ( n = M -> seq n ( x. , F ) = seq M ( x. , F ) )
16 15 breq1d 
 |-  ( n = M -> ( seq n ( x. , F ) ~~> y <-> seq M ( x. , F ) ~~> y ) )
17 16 anbi2d 
 |-  ( n = M -> ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> ( y =/= 0 /\ seq M ( x. , F ) ~~> y ) ) )
18 17 exbidv 
 |-  ( n = M -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. y ( y =/= 0 /\ seq M ( x. , F ) ~~> y ) ) )
19 18 rspcev 
 |-  ( ( M e. Z /\ E. y ( y =/= 0 /\ seq M ( x. , F ) ~~> y ) ) -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
20 6 14 19 syl2anc 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )