Metamath Proof Explorer

Theorem cvgrat

Description: Ratio test for convergence of a complex infinite series. If the ratio A of the absolute values of successive terms in an infinite sequence F is less than 1 for all terms beyond some index B , then the infinite sum of the terms of F converges to a complex number. Equivalent to first part of Exercise 4 of Gleason p. 182. (Contributed by NM, 26-Apr-2005) (Proof shortened by Mario Carneiro, 27-Apr-2014)

Ref Expression
Hypotheses cvgrat.1 
|- Z = ( ZZ>= ` M )
cvgrat.2 
|- W = ( ZZ>= ` N )
cvgrat.3 
|- ( ph -> A e. RR )
cvgrat.4 
|- ( ph -> A < 1 )
cvgrat.5 
|- ( ph -> N e. Z )
cvgrat.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
cvgrat.7 
|- ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )
Assertion cvgrat 
|- ( ph -> seq M ( + , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 cvgrat.1 
 |-  Z = ( ZZ>= ` M )
2 cvgrat.2 
 |-  W = ( ZZ>= ` N )
3 cvgrat.3 
 |-  ( ph -> A e. RR )
4 cvgrat.4 
 |-  ( ph -> A < 1 )
5 cvgrat.5 
 |-  ( ph -> N e. Z )
6 cvgrat.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 cvgrat.7 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( A x. ( abs ` ( F ` k ) ) ) )
8 5 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
9 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10 8 9 syl 
 |-  ( ph -> N e. ZZ )
11 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
12 10 11 syl 
 |-  ( ph -> N e. ( ZZ>= ` N ) )
13 12 2 eleqtrrdi 
 |-  ( ph -> N e. W )
14 oveq1 
 |-  ( n = k -> ( n - N ) = ( k - N ) )
15 14 oveq2d 
 |-  ( n = k -> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
16 eqid 
 |-  ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) = ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) )
17 ovex 
 |-  ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) e. _V
18 15 16 17 fvmpt 
 |-  ( k e. W -> ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
19 18 adantl 
 |-  ( ( ph /\ k e. W ) -> ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
20 0re 
 |-  0 e. RR
21 ifcl 
 |-  ( ( 0 e. RR /\ A e. RR ) -> if ( A <_ 0 , 0 , A ) e. RR )
22 20 3 21 sylancr 
 |-  ( ph -> if ( A <_ 0 , 0 , A ) e. RR )
23 22 adantr 
 |-  ( ( ph /\ k e. W ) -> if ( A <_ 0 , 0 , A ) e. RR )
24 simpr 
 |-  ( ( ph /\ k e. W ) -> k e. W )
25 24 2 eleqtrdi 
 |-  ( ( ph /\ k e. W ) -> k e. ( ZZ>= ` N ) )
26 uznn0sub 
 |-  ( k e. ( ZZ>= ` N ) -> ( k - N ) e. NN0 )
27 25 26 syl 
 |-  ( ( ph /\ k e. W ) -> ( k - N ) e. NN0 )
28 23 27 reexpcld 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) e. RR )
29 19 28 eqeltrd 
 |-  ( ( ph /\ k e. W ) -> ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) e. RR )
30 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
31 8 30 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
32 31 2 1 3sstr4g 
 |-  ( ph -> W C_ Z )
33 32 sselda 
 |-  ( ( ph /\ k e. W ) -> k e. Z )
34 33 6 syldan 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) e. CC )
35 26 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( k - N ) e. NN0 )
36 oveq2 
 |-  ( n = ( k - N ) -> ( if ( A <_ 0 , 0 , A ) ^ n ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
37 eqid 
 |-  ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) = ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) )
38 36 37 17 fvmpt 
 |-  ( ( k - N ) e. NN0 -> ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` ( k - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
39 35 38 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` ( k - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
40 10 zcnd 
 |-  ( ph -> N e. CC )
41 eluzelz 
 |-  ( k e. ( ZZ>= ` N ) -> k e. ZZ )
42 41 zcnd 
 |-  ( k e. ( ZZ>= ` N ) -> k e. CC )
43 nn0ex 
 |-  NN0 e. _V
44 43 mptex 
 |-  ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) e. _V
45 44 shftval 
 |-  ( ( N e. CC /\ k e. CC ) -> ( ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ` k ) = ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` ( k - N ) ) )
46 40 42 45 syl2an 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ` k ) = ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` ( k - N ) ) )
47 simpr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. ( ZZ>= ` N ) )
48 47 2 eleqtrrdi 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. W )
49 48 18 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) = ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) )
50 39 46 49 3eqtr4rd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) = ( ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ` k ) )
51 10 50 seqfeq 
 |-  ( ph -> seq N ( + , ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) = seq N ( + , ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ) )
52 44 seqshft 
 |-  ( ( N e. ZZ /\ N e. ZZ ) -> seq N ( + , ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ) = ( seq ( N - N ) ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) )
53 10 10 52 syl2anc 
 |-  ( ph -> seq N ( + , ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) shift N ) ) = ( seq ( N - N ) ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) )
54 40 subidd 
 |-  ( ph -> ( N - N ) = 0 )
55 54 seqeq1d 
 |-  ( ph -> seq ( N - N ) ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) = seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) )
56 55 oveq1d 
 |-  ( ph -> ( seq ( N - N ) ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) = ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) )
57 51 53 56 3eqtrd 
 |-  ( ph -> seq N ( + , ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) = ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) )
58 22 recnd 
 |-  ( ph -> if ( A <_ 0 , 0 , A ) e. CC )
59 max2 
 |-  ( ( A e. RR /\ 0 e. RR ) -> 0 <_ if ( A <_ 0 , 0 , A ) )
60 3 20 59 sylancl 
 |-  ( ph -> 0 <_ if ( A <_ 0 , 0 , A ) )
61 22 60 absidd 
 |-  ( ph -> ( abs ` if ( A <_ 0 , 0 , A ) ) = if ( A <_ 0 , 0 , A ) )
62 0lt1 
 |-  0 < 1
63 breq1 
 |-  ( 0 = if ( A <_ 0 , 0 , A ) -> ( 0 < 1 <-> if ( A <_ 0 , 0 , A ) < 1 ) )
64 breq1 
 |-  ( A = if ( A <_ 0 , 0 , A ) -> ( A < 1 <-> if ( A <_ 0 , 0 , A ) < 1 ) )
65 63 64 ifboth 
 |-  ( ( 0 < 1 /\ A < 1 ) -> if ( A <_ 0 , 0 , A ) < 1 )
66 62 4 65 sylancr 
 |-  ( ph -> if ( A <_ 0 , 0 , A ) < 1 )
67 61 66 eqbrtrd 
 |-  ( ph -> ( abs ` if ( A <_ 0 , 0 , A ) ) < 1 )
68 oveq2 
 |-  ( n = k -> ( if ( A <_ 0 , 0 , A ) ^ n ) = ( if ( A <_ 0 , 0 , A ) ^ k ) )
69 ovex 
 |-  ( if ( A <_ 0 , 0 , A ) ^ k ) e. _V
70 68 37 69 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` k ) = ( if ( A <_ 0 , 0 , A ) ^ k ) )
71 70 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ` k ) = ( if ( A <_ 0 , 0 , A ) ^ k ) )
72 58 67 71 geolim 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) )
73 seqex 
 |-  seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) e. _V
74 climshft 
 |-  ( ( N e. ZZ /\ seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) e. _V ) -> ( ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) <-> seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) ) )
75 10 73 74 sylancl 
 |-  ( ph -> ( ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) <-> seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) ) )
76 72 75 mpbird 
 |-  ( ph -> ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) )
77 ovex 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) e. _V
78 ovex 
 |-  ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) e. _V
79 77 78 breldm 
 |-  ( ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) ~~> ( 1 / ( 1 - if ( A <_ 0 , 0 , A ) ) ) -> ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) e. dom ~~> )
80 76 79 syl 
 |-  ( ph -> ( seq 0 ( + , ( n e. NN0 |-> ( if ( A <_ 0 , 0 , A ) ^ n ) ) ) shift N ) e. dom ~~> )
81 57 80 eqeltrd 
 |-  ( ph -> seq N ( + , ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) e. dom ~~> )
82 fveq2 
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
83 82 eleq1d 
 |-  ( k = N -> ( ( F ` k ) e. CC <-> ( F ` N ) e. CC ) )
84 6 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
85 83 84 5 rspcdva 
 |-  ( ph -> ( F ` N ) e. CC )
86 85 abscld 
 |-  ( ph -> ( abs ` ( F ` N ) ) e. RR )
87 2fveq3 
 |-  ( n = N -> ( abs ` ( F ` n ) ) = ( abs ` ( F ` N ) ) )
88 oveq1 
 |-  ( n = N -> ( n - N ) = ( N - N ) )
89 88 oveq2d 
 |-  ( n = N -> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) )
90 89 oveq2d 
 |-  ( n = N -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) )
91 87 90 breq12d 
 |-  ( n = N -> ( ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) <-> ( abs ` ( F ` N ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) ) )
92 91 imbi2d 
 |-  ( n = N -> ( ( ph -> ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) <-> ( ph -> ( abs ` ( F ` N ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) ) ) )
93 2fveq3 
 |-  ( n = k -> ( abs ` ( F ` n ) ) = ( abs ` ( F ` k ) ) )
94 15 oveq2d 
 |-  ( n = k -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) )
95 93 94 breq12d 
 |-  ( n = k -> ( ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) <-> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) )
96 95 imbi2d 
 |-  ( n = k -> ( ( ph -> ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) <-> ( ph -> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) ) )
97 2fveq3 
 |-  ( n = ( k + 1 ) -> ( abs ` ( F ` n ) ) = ( abs ` ( F ` ( k + 1 ) ) ) )
98 oveq1 
 |-  ( n = ( k + 1 ) -> ( n - N ) = ( ( k + 1 ) - N ) )
99 98 oveq2d 
 |-  ( n = ( k + 1 ) -> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) )
100 99 oveq2d 
 |-  ( n = ( k + 1 ) -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) )
101 97 100 breq12d 
 |-  ( n = ( k + 1 ) -> ( ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) <-> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
102 101 imbi2d 
 |-  ( n = ( k + 1 ) -> ( ( ph -> ( abs ` ( F ` n ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ) <-> ( ph -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) ) )
103 86 leidd 
 |-  ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` N ) ) )
104 54 oveq2d 
 |-  ( ph -> ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ 0 ) )
105 58 exp0d 
 |-  ( ph -> ( if ( A <_ 0 , 0 , A ) ^ 0 ) = 1 )
106 104 105 eqtrd 
 |-  ( ph -> ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) = 1 )
107 106 oveq2d 
 |-  ( ph -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) = ( ( abs ` ( F ` N ) ) x. 1 ) )
108 86 recnd 
 |-  ( ph -> ( abs ` ( F ` N ) ) e. CC )
109 108 mulridd 
 |-  ( ph -> ( ( abs ` ( F ` N ) ) x. 1 ) = ( abs ` ( F ` N ) ) )
110 107 109 eqtrd 
 |-  ( ph -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) = ( abs ` ( F ` N ) ) )
111 103 110 breqtrrd 
 |-  ( ph -> ( abs ` ( F ` N ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( N - N ) ) ) )
112 34 abscld 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` k ) ) e. RR )
113 86 adantr 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` N ) ) e. RR )
114 113 28 remulcld 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) e. RR )
115 60 adantr 
 |-  ( ( ph /\ k e. W ) -> 0 <_ if ( A <_ 0 , 0 , A ) )
116 lemul2a 
 |-  ( ( ( ( abs ` ( F ` k ) ) e. RR /\ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) e. RR /\ ( if ( A <_ 0 , 0 , A ) e. RR /\ 0 <_ if ( A <_ 0 , 0 , A ) ) ) /\ ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) -> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) )
117 116 ex 
 |-  ( ( ( abs ` ( F ` k ) ) e. RR /\ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) e. RR /\ ( if ( A <_ 0 , 0 , A ) e. RR /\ 0 <_ if ( A <_ 0 , 0 , A ) ) ) -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) ) )
118 112 114 23 115 117 syl112anc 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) ) )
119 58 adantr 
 |-  ( ( ph /\ k e. W ) -> if ( A <_ 0 , 0 , A ) e. CC )
120 108 adantr 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` N ) ) e. CC )
121 28 recnd 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) e. CC )
122 119 120 121 mul12d 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) )
123 119 27 expp1d 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) ^ ( ( k - N ) + 1 ) ) = ( ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) x. if ( A <_ 0 , 0 , A ) ) )
124 42 2 eleq2s 
 |-  ( k e. W -> k e. CC )
125 ax-1cn 
 |-  1 e. CC
126 addsub 
 |-  ( ( k e. CC /\ 1 e. CC /\ N e. CC ) -> ( ( k + 1 ) - N ) = ( ( k - N ) + 1 ) )
127 125 126 mp3an2 
 |-  ( ( k e. CC /\ N e. CC ) -> ( ( k + 1 ) - N ) = ( ( k - N ) + 1 ) )
128 124 40 127 syl2anr 
 |-  ( ( ph /\ k e. W ) -> ( ( k + 1 ) - N ) = ( ( k - N ) + 1 ) )
129 128 oveq2d 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( ( k - N ) + 1 ) ) )
130 119 121 mulcomd 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) = ( ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) x. if ( A <_ 0 , 0 , A ) ) )
131 123 129 130 3eqtr4rd 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) = ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) )
132 131 oveq2d 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) )
133 122 132 eqtrd 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) )
134 133 breq2d 
 |-  ( ( ph /\ k e. W ) -> ( ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) <-> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
135 118 134 sylibd 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
136 fveq2 
 |-  ( n = ( k + 1 ) -> ( F ` n ) = ( F ` ( k + 1 ) ) )
137 136 eleq1d 
 |-  ( n = ( k + 1 ) -> ( ( F ` n ) e. CC <-> ( F ` ( k + 1 ) ) e. CC ) )
138 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
139 138 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. CC <-> ( F ` n ) e. CC ) )
140 139 cbvralvw 
 |-  ( A. k e. Z ( F ` k ) e. CC <-> A. n e. Z ( F ` n ) e. CC )
141 84 140 sylib 
 |-  ( ph -> A. n e. Z ( F ` n ) e. CC )
142 141 adantr 
 |-  ( ( ph /\ k e. W ) -> A. n e. Z ( F ` n ) e. CC )
143 2 peano2uzs 
 |-  ( k e. W -> ( k + 1 ) e. W )
144 32 sselda 
 |-  ( ( ph /\ ( k + 1 ) e. W ) -> ( k + 1 ) e. Z )
145 143 144 sylan2 
 |-  ( ( ph /\ k e. W ) -> ( k + 1 ) e. Z )
146 137 142 145 rspcdva 
 |-  ( ( ph /\ k e. W ) -> ( F ` ( k + 1 ) ) e. CC )
147 146 abscld 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) e. RR )
148 3 adantr 
 |-  ( ( ph /\ k e. W ) -> A e. RR )
149 148 112 remulcld 
 |-  ( ( ph /\ k e. W ) -> ( A x. ( abs ` ( F ` k ) ) ) e. RR )
150 23 112 remulcld 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) e. RR )
151 34 absge0d 
 |-  ( ( ph /\ k e. W ) -> 0 <_ ( abs ` ( F ` k ) ) )
152 max1 
 |-  ( ( A e. RR /\ 0 e. RR ) -> A <_ if ( A <_ 0 , 0 , A ) )
153 3 20 152 sylancl 
 |-  ( ph -> A <_ if ( A <_ 0 , 0 , A ) )
154 153 adantr 
 |-  ( ( ph /\ k e. W ) -> A <_ if ( A <_ 0 , 0 , A ) )
155 148 23 112 151 154 lemul1ad 
 |-  ( ( ph /\ k e. W ) -> ( A x. ( abs ` ( F ` k ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) )
156 147 149 150 7 155 letrd 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) )
157 peano2uz 
 |-  ( k e. ( ZZ>= ` N ) -> ( k + 1 ) e. ( ZZ>= ` N ) )
158 25 157 syl 
 |-  ( ( ph /\ k e. W ) -> ( k + 1 ) e. ( ZZ>= ` N ) )
159 uznn0sub 
 |-  ( ( k + 1 ) e. ( ZZ>= ` N ) -> ( ( k + 1 ) - N ) e. NN0 )
160 158 159 syl 
 |-  ( ( ph /\ k e. W ) -> ( ( k + 1 ) - N ) e. NN0 )
161 23 160 reexpcld 
 |-  ( ( ph /\ k e. W ) -> ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) e. RR )
162 113 161 remulcld 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) e. RR )
163 letr 
 |-  ( ( ( abs ` ( F ` ( k + 1 ) ) ) e. RR /\ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) e. RR /\ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) e. RR ) -> ( ( ( abs ` ( F ` ( k + 1 ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) /\ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
164 147 150 162 163 syl3anc 
 |-  ( ( ph /\ k e. W ) -> ( ( ( abs ` ( F ` ( k + 1 ) ) ) <_ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) /\ ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
165 156 164 mpand 
 |-  ( ( ph /\ k e. W ) -> ( ( if ( A <_ 0 , 0 , A ) x. ( abs ` ( F ` k ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
166 135 165 syld 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
167 48 166 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) )
168 167 expcom 
 |-  ( k e. ( ZZ>= ` N ) -> ( ph -> ( ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) ) )
169 168 a2d 
 |-  ( k e. ( ZZ>= ` N ) -> ( ( ph -> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) -> ( ph -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( ( k + 1 ) - N ) ) ) ) ) )
170 92 96 102 96 111 169 uzind4i 
 |-  ( k e. ( ZZ>= ` N ) -> ( ph -> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) ) )
171 170 impcom 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) )
172 49 oveq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( abs ` ( F ` N ) ) x. ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) ) = ( ( abs ` ( F ` N ) ) x. ( if ( A <_ 0 , 0 , A ) ^ ( k - N ) ) ) )
173 171 172 breqtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( F ` k ) ) <_ ( ( abs ` ( F ` N ) ) x. ( ( n e. W |-> ( if ( A <_ 0 , 0 , A ) ^ ( n - N ) ) ) ` k ) ) )
174 2 13 29 34 81 86 173 cvgcmpce 
 |-  ( ph -> seq N ( + , F ) e. dom ~~> )
175 1 5 6 iserex 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
176 174 175 mpbird 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )