Metamath Proof Explorer


Theorem ntrivcvgmullem

Description: Lemma for ntrivcvgmul . (Contributed by Scott Fenton, 19-Dec-2017)

Ref Expression
Hypotheses ntrivcvgmullem.1
|- Z = ( ZZ>= ` M )
ntrivcvgmullem.2
|- ( ph -> N e. Z )
ntrivcvgmullem.3
|- ( ph -> P e. Z )
ntrivcvgmullem.4
|- ( ph -> X =/= 0 )
ntrivcvgmullem.5
|- ( ph -> Y =/= 0 )
ntrivcvgmullem.6
|- ( ph -> seq N ( x. , F ) ~~> X )
ntrivcvgmullem.7
|- ( ph -> seq P ( x. , G ) ~~> Y )
ntrivcvgmullem.8
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
ntrivcvgmullem.9
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
ntrivcvgmullem.a
|- ( ph -> N <_ P )
ntrivcvgmullem.b
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
Assertion ntrivcvgmullem
|- ( ph -> E. q e. Z E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) )

Proof

Step Hyp Ref Expression
1 ntrivcvgmullem.1
 |-  Z = ( ZZ>= ` M )
2 ntrivcvgmullem.2
 |-  ( ph -> N e. Z )
3 ntrivcvgmullem.3
 |-  ( ph -> P e. Z )
4 ntrivcvgmullem.4
 |-  ( ph -> X =/= 0 )
5 ntrivcvgmullem.5
 |-  ( ph -> Y =/= 0 )
6 ntrivcvgmullem.6
 |-  ( ph -> seq N ( x. , F ) ~~> X )
7 ntrivcvgmullem.7
 |-  ( ph -> seq P ( x. , G ) ~~> Y )
8 ntrivcvgmullem.8
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
9 ntrivcvgmullem.9
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
10 ntrivcvgmullem.a
 |-  ( ph -> N <_ P )
11 ntrivcvgmullem.b
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
12 eqid
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
13 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
14 1 13 eqsstri
 |-  Z C_ ZZ
15 14 2 sselid
 |-  ( ph -> N e. ZZ )
16 14 3 sselid
 |-  ( ph -> P e. ZZ )
17 eluz
 |-  ( ( N e. ZZ /\ P e. ZZ ) -> ( P e. ( ZZ>= ` N ) <-> N <_ P ) )
18 15 16 17 syl2anc
 |-  ( ph -> ( P e. ( ZZ>= ` N ) <-> N <_ P ) )
19 10 18 mpbird
 |-  ( ph -> P e. ( ZZ>= ` N ) )
20 1 uztrn2
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
21 2 20 sylan
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
22 21 8 syldan
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. CC )
23 12 19 6 4 22 ntrivcvgtail
 |-  ( ph -> ( ( ~~> ` seq P ( x. , F ) ) =/= 0 /\ seq P ( x. , F ) ~~> ( ~~> ` seq P ( x. , F ) ) ) )
24 23 simprd
 |-  ( ph -> seq P ( x. , F ) ~~> ( ~~> ` seq P ( x. , F ) ) )
25 climcl
 |-  ( seq P ( x. , F ) ~~> ( ~~> ` seq P ( x. , F ) ) -> ( ~~> ` seq P ( x. , F ) ) e. CC )
26 24 25 syl
 |-  ( ph -> ( ~~> ` seq P ( x. , F ) ) e. CC )
27 climcl
 |-  ( seq P ( x. , G ) ~~> Y -> Y e. CC )
28 7 27 syl
 |-  ( ph -> Y e. CC )
29 23 simpld
 |-  ( ph -> ( ~~> ` seq P ( x. , F ) ) =/= 0 )
30 26 28 29 5 mulne0d
 |-  ( ph -> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) =/= 0 )
31 eqid
 |-  ( ZZ>= ` P ) = ( ZZ>= ` P )
32 seqex
 |-  seq P ( x. , H ) e. _V
33 32 a1i
 |-  ( ph -> seq P ( x. , H ) e. _V )
34 1 uztrn2
 |-  ( ( P e. Z /\ k e. ( ZZ>= ` P ) ) -> k e. Z )
35 3 34 sylan
 |-  ( ( ph /\ k e. ( ZZ>= ` P ) ) -> k e. Z )
36 35 8 syldan
 |-  ( ( ph /\ k e. ( ZZ>= ` P ) ) -> ( F ` k ) e. CC )
37 31 16 36 prodf
 |-  ( ph -> seq P ( x. , F ) : ( ZZ>= ` P ) --> CC )
38 37 ffvelrnda
 |-  ( ( ph /\ j e. ( ZZ>= ` P ) ) -> ( seq P ( x. , F ) ` j ) e. CC )
39 35 9 syldan
 |-  ( ( ph /\ k e. ( ZZ>= ` P ) ) -> ( G ` k ) e. CC )
40 31 16 39 prodf
 |-  ( ph -> seq P ( x. , G ) : ( ZZ>= ` P ) --> CC )
41 40 ffvelrnda
 |-  ( ( ph /\ j e. ( ZZ>= ` P ) ) -> ( seq P ( x. , G ) ` j ) e. CC )
42 simpr
 |-  ( ( ph /\ j e. ( ZZ>= ` P ) ) -> j e. ( ZZ>= ` P ) )
43 simpll
 |-  ( ( ( ph /\ j e. ( ZZ>= ` P ) ) /\ k e. ( P ... j ) ) -> ph )
44 3 adantr
 |-  ( ( ph /\ j e. ( ZZ>= ` P ) ) -> P e. Z )
45 elfzuz
 |-  ( k e. ( P ... j ) -> k e. ( ZZ>= ` P ) )
46 44 45 34 syl2an
 |-  ( ( ( ph /\ j e. ( ZZ>= ` P ) ) /\ k e. ( P ... j ) ) -> k e. Z )
47 43 46 8 syl2anc
 |-  ( ( ( ph /\ j e. ( ZZ>= ` P ) ) /\ k e. ( P ... j ) ) -> ( F ` k ) e. CC )
48 43 46 9 syl2anc
 |-  ( ( ( ph /\ j e. ( ZZ>= ` P ) ) /\ k e. ( P ... j ) ) -> ( G ` k ) e. CC )
49 43 46 11 syl2anc
 |-  ( ( ( ph /\ j e. ( ZZ>= ` P ) ) /\ k e. ( P ... j ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )
50 42 47 48 49 prodfmul
 |-  ( ( ph /\ j e. ( ZZ>= ` P ) ) -> ( seq P ( x. , H ) ` j ) = ( ( seq P ( x. , F ) ` j ) x. ( seq P ( x. , G ) ` j ) ) )
51 31 16 24 33 7 38 41 50 climmul
 |-  ( ph -> seq P ( x. , H ) ~~> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) )
52 ovex
 |-  ( ( ~~> ` seq P ( x. , F ) ) x. Y ) e. _V
53 neeq1
 |-  ( w = ( ( ~~> ` seq P ( x. , F ) ) x. Y ) -> ( w =/= 0 <-> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) =/= 0 ) )
54 breq2
 |-  ( w = ( ( ~~> ` seq P ( x. , F ) ) x. Y ) -> ( seq P ( x. , H ) ~~> w <-> seq P ( x. , H ) ~~> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) ) )
55 53 54 anbi12d
 |-  ( w = ( ( ~~> ` seq P ( x. , F ) ) x. Y ) -> ( ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) <-> ( ( ( ~~> ` seq P ( x. , F ) ) x. Y ) =/= 0 /\ seq P ( x. , H ) ~~> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) ) ) )
56 52 55 spcev
 |-  ( ( ( ( ~~> ` seq P ( x. , F ) ) x. Y ) =/= 0 /\ seq P ( x. , H ) ~~> ( ( ~~> ` seq P ( x. , F ) ) x. Y ) ) -> E. w ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) )
57 30 51 56 syl2anc
 |-  ( ph -> E. w ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) )
58 seqeq1
 |-  ( q = P -> seq q ( x. , H ) = seq P ( x. , H ) )
59 58 breq1d
 |-  ( q = P -> ( seq q ( x. , H ) ~~> w <-> seq P ( x. , H ) ~~> w ) )
60 59 anbi2d
 |-  ( q = P -> ( ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) <-> ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) ) )
61 60 exbidv
 |-  ( q = P -> ( E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) <-> E. w ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) ) )
62 61 rspcev
 |-  ( ( P e. Z /\ E. w ( w =/= 0 /\ seq P ( x. , H ) ~~> w ) ) -> E. q e. Z E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) )
63 3 57 62 syl2anc
 |-  ( ph -> E. q e. Z E. w ( w =/= 0 /\ seq q ( x. , H ) ~~> w ) )