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 sseldi 
 |-  ( ph -> N e. ZZ )
16 14 3 sseldi 
 |-  ( 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 ) )