Description: A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ntrivcvgn0.1 | |
|
ntrivcvgn0.2 | |
||
ntrivcvgn0.3 | |
||
ntrivcvgn0.4 | |
||
Assertion | ntrivcvgn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ntrivcvgn0.1 | |
|
2 | ntrivcvgn0.2 | |
|
3 | ntrivcvgn0.3 | |
|
4 | ntrivcvgn0.4 | |
|
5 | 2 | uzidd | |
6 | 5 1 | eleqtrrdi | |
7 | climrel | |
|
8 | 7 | brrelex2i | |
9 | 3 8 | syl | |
10 | 4 3 | jca | |
11 | neeq1 | |
|
12 | breq2 | |
|
13 | 11 12 | anbi12d | |
14 | 9 10 13 | spcedv | |
15 | seqeq1 | |
|
16 | 15 | breq1d | |
17 | 16 | anbi2d | |
18 | 17 | exbidv | |
19 | 18 | rspcev | |
20 | 6 14 19 | syl2anc | |