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 sselid 
 |-  ( ( 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 sselid 
 |-  ( ( 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 )
23 22 adantr 
 |-  ( ( ( 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 )
25 24 adantr 
 |-  ( ( ( 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 )
27 26 adantr 
 |-  ( ( ( 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 )
29 28 adantr 
 |-  ( ( ( 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 )
38 24 adantr 
 |-  ( ( ( 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 )
39 22 adantr 
 |-  ( ( ( 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 )
40 28 adantr 
 |-  ( ( ( 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 )
41 26 adantr 
 |-  ( ( ( 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 ) )