Metamath Proof Explorer

Theorem ntrivcvg

Description: A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses ntrivcvg.1 
|- Z = ( ZZ>= ` M )
ntrivcvg.2 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
ntrivcvg.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
Assertion ntrivcvg 
|- ( ph -> seq M ( x. , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 ntrivcvg.1 
 |-  Z = ( ZZ>= ` M )
2 ntrivcvg.2 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
3 ntrivcvg.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 uzm1 
 |-  ( n e. ( ZZ>= ` M ) -> ( n = M \/ ( n - 1 ) e. ( ZZ>= ` M ) ) )
5 4 1 eleq2s 
 |-  ( n e. Z -> ( n = M \/ ( n - 1 ) e. ( ZZ>= ` M ) ) )
6 5 ad2antlr 
 |-  ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> ( n = M \/ ( n - 1 ) e. ( ZZ>= ` M ) ) )
7 seqeq1 
 |-  ( n = M -> seq n ( x. , F ) = seq M ( x. , F ) )
8 7 breq1d 
 |-  ( n = M -> ( seq n ( x. , F ) ~~> y <-> seq M ( x. , F ) ~~> y ) )
9 seqex 
 |-  seq M ( x. , F ) e. _V
10 vex 
 |-  y e. _V
11 9 10 breldm 
 |-  ( seq M ( x. , F ) ~~> y -> seq M ( x. , F ) e. dom ~~> )
12 8 11 syl6bi 
 |-  ( n = M -> ( seq n ( x. , F ) ~~> y -> seq M ( x. , F ) e. dom ~~> ) )
13 12 adantld 
 |-  ( n = M -> ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
14 simplr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) /\ seq n ( x. , F ) ~~> y ) -> ( n - 1 ) e. Z )
15 3 ad5ant15 
 |-  ( ( ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) /\ seq n ( x. , F ) ~~> y ) /\ k e. Z ) -> ( F ` k ) e. CC )
16 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
17 1 16 eqsstri 
 |-  Z C_ ZZ
18 simplr 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> n e. Z )
19 17 18 sselid 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> n e. ZZ )
20 19 zcnd 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> n e. CC )
21 1cnd 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> 1 e. CC )
22 20 21 npcand 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> ( ( n - 1 ) + 1 ) = n )
23 22 seqeq1d 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> seq ( ( n - 1 ) + 1 ) ( x. , F ) = seq n ( x. , F ) )
24 23 breq1d 
 |-  ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) -> ( seq ( ( n - 1 ) + 1 ) ( x. , F ) ~~> y <-> seq n ( x. , F ) ~~> y ) )
25 24 biimpar 
 |-  ( ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq ( ( n - 1 ) + 1 ) ( x. , F ) ~~> y )
26 1 14 15 25 clim2prod 
 |-  ( ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) ~~> ( ( seq M ( x. , F ) ` ( n - 1 ) ) x. y ) )
27 ovex 
 |-  ( ( seq M ( x. , F ) ` ( n - 1 ) ) x. y ) e. _V
28 9 27 breldm 
 |-  ( seq M ( x. , F ) ~~> ( ( seq M ( x. , F ) ` ( n - 1 ) ) x. y ) -> seq M ( x. , F ) e. dom ~~> )
29 26 28 syl 
 |-  ( ( ( ( ph /\ n e. Z ) /\ ( n - 1 ) e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> )
30 29 an32s 
 |-  ( ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) /\ ( n - 1 ) e. Z ) -> seq M ( x. , F ) e. dom ~~> )
31 30 expcom 
 |-  ( ( n - 1 ) e. Z -> ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
32 1 eqcomi 
 |-  ( ZZ>= ` M ) = Z
33 31 32 eleq2s 
 |-  ( ( n - 1 ) e. ( ZZ>= ` M ) -> ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
34 13 33 jaoi 
 |-  ( ( n = M \/ ( n - 1 ) e. ( ZZ>= ` M ) ) -> ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
35 6 34 mpcom 
 |-  ( ( ( ph /\ n e. Z ) /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> )
36 35 ex 
 |-  ( ( ph /\ n e. Z ) -> ( seq n ( x. , F ) ~~> y -> seq M ( x. , F ) e. dom ~~> ) )
37 36 adantld 
 |-  ( ( ph /\ n e. Z ) -> ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
38 37 exlimdv 
 |-  ( ( ph /\ n e. Z ) -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
39 38 rexlimdva 
 |-  ( ph -> ( E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) -> seq M ( x. , F ) e. dom ~~> ) )
40 2 39 mpd 
 |-  ( ph -> seq M ( x. , F ) e. dom ~~> )