# Metamath Proof Explorer

## Theorem ntrivcvgmul

Description: The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses ntrivcvgmul.1
`|- Z = ( ZZ>= ` M )`
ntrivcvgmul.3
`|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )`
ntrivcvgmul.4
`|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )`
ntrivcvgmul.5
`|- ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )`
ntrivcvgmul.6
`|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )`
ntrivcvgmul.7
`|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )`
Assertion ntrivcvgmul
`|- ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )`

### Proof

Step Hyp Ref Expression
1 ntrivcvgmul.1
` |-  Z = ( ZZ>= ` M )`
2 ntrivcvgmul.3
` |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )`
3 ntrivcvgmul.4
` |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )`
4 ntrivcvgmul.5
` |-  ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )`
5 ntrivcvgmul.6
` |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )`
6 ntrivcvgmul.7
` |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )`
7 exdistrv
` |-  ( E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) <-> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) )`
8 7 2rexbii
` |-  ( E. n e. Z E. m e. Z E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) <-> E. n e. Z E. m e. Z ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) )`
9 reeanv
` |-  ( E. n e. Z E. m e. Z ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) <-> ( E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) )`
10 8 9 bitri
` |-  ( E. n e. Z E. m e. Z E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) <-> ( E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) )`
11 2 4 10 sylanbrc
` |-  ( ph -> E. n e. Z E. m e. Z E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) )`
12 uzssz
` |-  ( ZZ>= ` M ) C_ ZZ`
13 1 12 eqsstri
` |-  Z C_ ZZ`
14 simp2l
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> n e. Z )`
15 13 14 sseldi
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> n e. ZZ )`
16 15 zred
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> n e. RR )`
17 simp2r
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> m e. Z )`
18 13 17 sseldi
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> m e. ZZ )`
19 18 zred
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> m e. RR )`
20 simpl2l
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> n e. Z )`
21 simpl2r
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> m e. Z )`
22 simp3ll
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> y =/= 0 )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> y =/= 0 )`
24 simp3rl
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> z =/= 0 )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> z =/= 0 )`
26 simp3lr
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> seq n ( x. , F ) ~~> y )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> seq n ( x. , F ) ~~> y )`
28 simp3rr
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> seq m ( x. , G ) ~~> z )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> seq m ( x. , G ) ~~> z )`
30 simpl1
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> ph )`
31 30 3 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) /\ k e. Z ) -> ( F ` k ) e. CC )`
32 30 5 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) /\ k e. Z ) -> ( G ` k ) e. CC )`
33 simpr
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> n <_ m )`
34 30 6 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )`
35 1 20 21 23 25 27 29 31 32 33 34 ntrivcvgmullem
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ n <_ m ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )`
36 simpl2r
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> m e. Z )`
37 simpl2l
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> n e. Z )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> z =/= 0 )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> y =/= 0 )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> seq m ( x. , G ) ~~> z )`
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> seq n ( x. , F ) ~~> y )`
42 simpl1
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> ph )`
43 42 5 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) /\ k e. Z ) -> ( G ` k ) e. CC )`
44 42 3 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) /\ k e. Z ) -> ( F ` k ) e. CC )`
45 simpr
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> m <_ n )`
46 3 5 mulcomd
` |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) x. ( G ` k ) ) = ( ( G ` k ) x. ( F ` k ) ) )`
47 6 46 eqtrd
` |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( G ` k ) x. ( F ` k ) ) )`
48 42 47 sylan
` |-  ( ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) /\ k e. Z ) -> ( H ` k ) = ( ( G ` k ) x. ( F ` k ) ) )`
49 1 36 37 38 39 40 41 43 44 45 48 ntrivcvgmullem
` |-  ( ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) /\ m <_ n ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )`
50 16 19 35 49 lecasei
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) /\ ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )`
51 50 3expia
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) ) -> ( ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) ) )`
52 51 exlimdvv
` |-  ( ( ph /\ ( n e. Z /\ m e. Z ) ) -> ( E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) ) )`
53 52 rexlimdvva
` |-  ( ph -> ( E. n e. Z E. m e. Z E. y E. z ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) /\ ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) ) -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) ) )`
54 11 53 mpd
` |-  ( ph -> E. p e. Z E. w ( w =/= 0 /\ seq p ( x. , H ) ~~> w ) )`