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 ) )