Metamath Proof Explorer

Theorem eftlub

Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses eftl.1 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
eftl.2 
|- G = ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) )
eftl.3 
|- H = ( n e. NN0 |-> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ n ) ) )
eftl.4 
|- ( ph -> M e. NN )
eftl.5 
|- ( ph -> A e. CC )
eftl.6 
|- ( ph -> ( abs ` A ) <_ 1 )
Assertion eftlub 
|- ( ph -> ( abs ` sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) <_ ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )

Proof

Step Hyp Ref Expression
1 eftl.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 eftl.2 
 |-  G = ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) )
3 eftl.3 
 |-  H = ( n e. NN0 |-> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ n ) ) )
4 eftl.4 
 |-  ( ph -> M e. NN )
5 eftl.5 
 |-  ( ph -> A e. CC )
6 eftl.6 
 |-  ( ph -> ( abs ` A ) <_ 1 )
7 4 nnnn0d 
 |-  ( ph -> M e. NN0 )
8 1 eftlcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. CC )
9 5 7 8 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. CC )
10 9 abscld 
 |-  ( ph -> ( abs ` sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) e. RR )
11 5 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
12 2 reeftlcl 
 |-  ( ( ( abs ` A ) e. RR /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( G ` k ) e. RR )
13 11 7 12 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( G ` k ) e. RR )
14 11 7 reexpcld 
 |-  ( ph -> ( ( abs ` A ) ^ M ) e. RR )
15 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
16 7 15 syl 
 |-  ( ph -> ( M + 1 ) e. NN0 )
17 16 nn0red 
 |-  ( ph -> ( M + 1 ) e. RR )
18 7 faccld 
 |-  ( ph -> ( ! ` M ) e. NN )
19 18 4 nnmulcld 
 |-  ( ph -> ( ( ! ` M ) x. M ) e. NN )
20 17 19 nndivred 
 |-  ( ph -> ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) e. RR )
21 14 20 remulcld 
 |-  ( ph -> ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) e. RR )
22 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
23 4 nnzd 
 |-  ( ph -> M e. ZZ )
24 eqidd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( F ` k ) )
25 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
26 7 25 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
27 1 eftval 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
28 27 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
29 eftcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
30 5 29 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
31 28 30 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
32 26 31 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
33 1 eftlcvg 
 |-  ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
34 5 7 33 syl2anc 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
35 22 23 24 32 34 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. ( ZZ>= ` M ) ( F ` k ) )
36 eqidd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) = ( G ` k ) )
37 2 eftval 
 |-  ( k e. NN0 -> ( G ` k ) = ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) )
38 37 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) = ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) )
39 reeftcl 
 |-  ( ( ( abs ` A ) e. RR /\ k e. NN0 ) -> ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) e. RR )
40 11 39 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) e. RR )
41 38 40 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) e. RR )
42 26 41 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. RR )
43 42 recnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )
44 11 recnd 
 |-  ( ph -> ( abs ` A ) e. CC )
45 2 eftlcvg 
 |-  ( ( ( abs ` A ) e. CC /\ M e. NN0 ) -> seq M ( + , G ) e. dom ~~> )
46 44 7 45 syl2anc 
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )
47 22 23 36 43 46 isumclim2 
 |-  ( ph -> seq M ( + , G ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
48 eftabs 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( ( A ^ k ) / ( ! ` k ) ) ) = ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) )
49 5 48 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( A ^ k ) / ( ! ` k ) ) ) = ( ( ( abs ` A ) ^ k ) / ( ! ` k ) ) )
50 28 fveq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` ( F ` k ) ) = ( abs ` ( ( A ^ k ) / ( ! ` k ) ) ) )
51 49 50 38 3eqtr4rd 
 |-  ( ( ph /\ k e. NN0 ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
52 26 51 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )
53 22 35 47 23 32 52 iserabs 
 |-  ( ph -> ( abs ` sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) <_ sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
54 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
55 0zd 
 |-  ( ph -> 0 e. ZZ )
56 4 nncnd 
 |-  ( ph -> M e. CC )
57 nn0cn 
 |-  ( j e. NN0 -> j e. CC )
58 nn0ex 
 |-  NN0 e. _V
59 58 mptex 
 |-  ( n e. NN0 |-> ( ( ( abs ` A ) ^ n ) / ( ! ` n ) ) ) e. _V
60 2 59 eqeltri 
 |-  G e. _V
61 60 shftval4 
 |-  ( ( M e. CC /\ j e. CC ) -> ( ( G shift -u M ) ` j ) = ( G ` ( M + j ) ) )
62 56 57 61 syl2an 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( G shift -u M ) ` j ) = ( G ` ( M + j ) ) )
63 nn0addcl 
 |-  ( ( M e. NN0 /\ j e. NN0 ) -> ( M + j ) e. NN0 )
64 7 63 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( M + j ) e. NN0 )
65 2 eftval 
 |-  ( ( M + j ) e. NN0 -> ( G ` ( M + j ) ) = ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) )
66 64 65 syl 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( M + j ) ) = ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) )
67 11 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` A ) e. RR )
68 reeftcl 
 |-  ( ( ( abs ` A ) e. RR /\ ( M + j ) e. NN0 ) -> ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) e. RR )
69 67 64 68 syl2anc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) e. RR )
70 66 69 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( M + j ) ) e. RR )
71 oveq2 
 |-  ( n = j -> ( ( 1 / ( M + 1 ) ) ^ n ) = ( ( 1 / ( M + 1 ) ) ^ j ) )
72 71 oveq2d 
 |-  ( n = j -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ n ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
73 ovex 
 |-  ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) e. _V
74 72 3 73 fvmpt 
 |-  ( j e. NN0 -> ( H ` j ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
75 74 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( H ` j ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
76 14 18 nndivred 
 |-  ( ph -> ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) e. RR )
77 76 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) e. RR )
78 4 peano2nnd 
 |-  ( ph -> ( M + 1 ) e. NN )
79 78 nnrecred 
 |-  ( ph -> ( 1 / ( M + 1 ) ) e. RR )
80 reexpcl 
 |-  ( ( ( 1 / ( M + 1 ) ) e. RR /\ j e. NN0 ) -> ( ( 1 / ( M + 1 ) ) ^ j ) e. RR )
81 79 80 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 / ( M + 1 ) ) ^ j ) e. RR )
82 77 81 remulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) e. RR )
83 67 64 reexpcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ ( M + j ) ) e. RR )
84 14 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ M ) e. RR )
85 64 faccld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` ( M + j ) ) e. NN )
86 85 nnred 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` ( M + j ) ) e. RR )
87 86 82 remulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) e. RR )
88 7 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> M e. NN0 )
89 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
90 23 89 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
91 uzaddcl 
 |-  ( ( M e. ( ZZ>= ` M ) /\ j e. NN0 ) -> ( M + j ) e. ( ZZ>= ` M ) )
92 90 91 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( M + j ) e. ( ZZ>= ` M ) )
93 5 absge0d 
 |-  ( ph -> 0 <_ ( abs ` A ) )
94 93 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> 0 <_ ( abs ` A ) )
95 6 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( abs ` A ) <_ 1 )
96 67 88 92 94 95 leexp2rd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ ( M + j ) ) <_ ( ( abs ` A ) ^ M ) )
97 18 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` M ) e. NN )
98 nnexpcl 
 |-  ( ( ( M + 1 ) e. NN /\ j e. NN0 ) -> ( ( M + 1 ) ^ j ) e. NN )
99 78 98 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( M + 1 ) ^ j ) e. NN )
100 97 99 nnmulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) e. NN )
101 100 nnred 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) e. RR )
102 11 7 93 expge0d 
 |-  ( ph -> 0 <_ ( ( abs ` A ) ^ M ) )
103 14 102 jca 
 |-  ( ph -> ( ( ( abs ` A ) ^ M ) e. RR /\ 0 <_ ( ( abs ` A ) ^ M ) ) )
104 103 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ M ) e. RR /\ 0 <_ ( ( abs ` A ) ^ M ) ) )
105 faclbnd6 
 |-  ( ( M e. NN0 /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) <_ ( ! ` ( M + j ) ) )
106 7 105 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) <_ ( ! ` ( M + j ) ) )
107 lemul1a 
 |-  ( ( ( ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) e. RR /\ ( ! ` ( M + j ) ) e. RR /\ ( ( ( abs ` A ) ^ M ) e. RR /\ 0 <_ ( ( abs ` A ) ^ M ) ) ) /\ ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) <_ ( ! ` ( M + j ) ) ) -> ( ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) x. ( ( abs ` A ) ^ M ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) )
108 101 86 104 106 107 syl31anc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) x. ( ( abs ` A ) ^ M ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) )
109 86 84 remulcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) e. RR )
110 100 nnrpd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) e. RR+ )
111 84 109 110 lemuldiv2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) x. ( ( abs ` A ) ^ M ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) <-> ( ( abs ` A ) ^ M ) <_ ( ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) ) )
112 108 111 mpbid 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ M ) <_ ( ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) )
113 85 nncnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` ( M + j ) ) e. CC )
114 14 recnd 
 |-  ( ph -> ( ( abs ` A ) ^ M ) e. CC )
115 114 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ M ) e. CC )
116 100 nncnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) e. CC )
117 100 nnne0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) =/= 0 )
118 113 115 116 117 divassd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) = ( ( ! ` ( M + j ) ) x. ( ( ( abs ` A ) ^ M ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) ) )
119 78 nncnd 
 |-  ( ph -> ( M + 1 ) e. CC )
120 119 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( M + 1 ) e. CC )
121 78 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( M + 1 ) e. NN )
122 121 nnne0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( M + 1 ) =/= 0 )
123 nn0z 
 |-  ( j e. NN0 -> j e. ZZ )
124 123 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> j e. ZZ )
125 120 122 124 exprecd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 / ( M + 1 ) ) ^ j ) = ( 1 / ( ( M + 1 ) ^ j ) ) )
126 125 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( 1 / ( ( M + 1 ) ^ j ) ) ) )
127 76 recnd 
 |-  ( ph -> ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) e. CC )
128 127 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) e. CC )
129 99 nncnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( M + 1 ) ^ j ) e. CC )
130 99 nnne0d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( M + 1 ) ^ j ) =/= 0 )
131 128 129 130 divrecd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) / ( ( M + 1 ) ^ j ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( 1 / ( ( M + 1 ) ^ j ) ) ) )
132 18 nncnd 
 |-  ( ph -> ( ! ` M ) e. CC )
133 132 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` M ) e. CC )
134 facne0 
 |-  ( M e. NN0 -> ( ! ` M ) =/= 0 )
135 7 134 syl 
 |-  ( ph -> ( ! ` M ) =/= 0 )
136 135 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( ! ` M ) =/= 0 )
137 115 133 129 136 130 divdiv1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) / ( ( M + 1 ) ^ j ) ) = ( ( ( abs ` A ) ^ M ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) )
138 126 131 137 3eqtr2rd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ M ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
139 138 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ! ` ( M + j ) ) x. ( ( ( abs ` A ) ^ M ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) ) = ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) )
140 118 139 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ! ` ( M + j ) ) x. ( ( abs ` A ) ^ M ) ) / ( ( ! ` M ) x. ( ( M + 1 ) ^ j ) ) ) = ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) )
141 112 140 breqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ M ) <_ ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) )
142 83 84 87 96 141 letrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( abs ` A ) ^ ( M + j ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) )
143 85 nngt0d 
 |-  ( ( ph /\ j e. NN0 ) -> 0 < ( ! ` ( M + j ) ) )
144 ledivmul 
 |-  ( ( ( ( abs ` A ) ^ ( M + j ) ) e. RR /\ ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) e. RR /\ ( ( ! ` ( M + j ) ) e. RR /\ 0 < ( ! ` ( M + j ) ) ) ) -> ( ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) <_ ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) <-> ( ( abs ` A ) ^ ( M + j ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) ) )
145 83 82 86 143 144 syl112anc 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) <_ ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) <-> ( ( abs ` A ) ^ ( M + j ) ) <_ ( ( ! ` ( M + j ) ) x. ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) ) ) )
146 142 145 mpbird 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( abs ` A ) ^ ( M + j ) ) / ( ! ` ( M + j ) ) ) <_ ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
147 66 146 eqbrtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( G ` ( M + j ) ) <_ ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
148 0z 
 |-  0 e. ZZ
149 23 znegcld 
 |-  ( ph -> -u M e. ZZ )
150 60 seqshft 
 |-  ( ( 0 e. ZZ /\ -u M e. ZZ ) -> seq 0 ( + , ( G shift -u M ) ) = ( seq ( 0 - -u M ) ( + , G ) shift -u M ) )
151 148 149 150 sylancr 
 |-  ( ph -> seq 0 ( + , ( G shift -u M ) ) = ( seq ( 0 - -u M ) ( + , G ) shift -u M ) )
152 0cn 
 |-  0 e. CC
153 subneg 
 |-  ( ( 0 e. CC /\ M e. CC ) -> ( 0 - -u M ) = ( 0 + M ) )
154 152 153 mpan 
 |-  ( M e. CC -> ( 0 - -u M ) = ( 0 + M ) )
155 addid2 
 |-  ( M e. CC -> ( 0 + M ) = M )
156 154 155 eqtrd 
 |-  ( M e. CC -> ( 0 - -u M ) = M )
157 56 156 syl 
 |-  ( ph -> ( 0 - -u M ) = M )
158 157 seqeq1d 
 |-  ( ph -> seq ( 0 - -u M ) ( + , G ) = seq M ( + , G ) )
159 158 47 eqbrtrd 
 |-  ( ph -> seq ( 0 - -u M ) ( + , G ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
160 seqex 
 |-  seq ( 0 - -u M ) ( + , G ) e. _V
161 climshft 
 |-  ( ( -u M e. ZZ /\ seq ( 0 - -u M ) ( + , G ) e. _V ) -> ( ( seq ( 0 - -u M ) ( + , G ) shift -u M ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) <-> seq ( 0 - -u M ) ( + , G ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) ) )
162 149 160 161 sylancl 
 |-  ( ph -> ( ( seq ( 0 - -u M ) ( + , G ) shift -u M ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) <-> seq ( 0 - -u M ) ( + , G ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) ) )
163 159 162 mpbird 
 |-  ( ph -> ( seq ( 0 - -u M ) ( + , G ) shift -u M ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
164 ovex 
 |-  ( seq ( 0 - -u M ) ( + , G ) shift -u M ) e. _V
165 sumex 
 |-  sum_ k e. ( ZZ>= ` M ) ( G ` k ) e. _V
166 164 165 breldm 
 |-  ( ( seq ( 0 - -u M ) ( + , G ) shift -u M ) ~~> sum_ k e. ( ZZ>= ` M ) ( G ` k ) -> ( seq ( 0 - -u M ) ( + , G ) shift -u M ) e. dom ~~> )
167 163 166 syl 
 |-  ( ph -> ( seq ( 0 - -u M ) ( + , G ) shift -u M ) e. dom ~~> )
168 151 167 eqeltrd 
 |-  ( ph -> seq 0 ( + , ( G shift -u M ) ) e. dom ~~> )
169 4 nnge1d 
 |-  ( ph -> 1 <_ M )
170 1nn 
 |-  1 e. NN
171 nnleltp1 
 |-  ( ( 1 e. NN /\ M e. NN ) -> ( 1 <_ M <-> 1 < ( M + 1 ) ) )
172 170 4 171 sylancr 
 |-  ( ph -> ( 1 <_ M <-> 1 < ( M + 1 ) ) )
173 169 172 mpbid 
 |-  ( ph -> 1 < ( M + 1 ) )
174 16 nn0ge0d 
 |-  ( ph -> 0 <_ ( M + 1 ) )
175 17 174 absidd 
 |-  ( ph -> ( abs ` ( M + 1 ) ) = ( M + 1 ) )
176 173 175 breqtrrd 
 |-  ( ph -> 1 < ( abs ` ( M + 1 ) ) )
177 eqid 
 |-  ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) = ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) )
178 ovex 
 |-  ( ( 1 / ( M + 1 ) ) ^ j ) e. _V
179 71 177 178 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ` j ) = ( ( 1 / ( M + 1 ) ) ^ j ) )
180 179 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ` j ) = ( ( 1 / ( M + 1 ) ) ^ j ) )
181 119 176 180 georeclim 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ) ~~> ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) )
182 81 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 / ( M + 1 ) ) ^ j ) e. CC )
183 180 182 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ` j ) e. CC )
184 180 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ` j ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
185 75 184 eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( H ` j ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( n e. NN0 |-> ( ( 1 / ( M + 1 ) ) ^ n ) ) ` j ) ) )
186 54 55 127 181 183 185 isermulc2 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) ) )
187 ax-1cn 
 |-  1 e. CC
188 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
189 56 187 188 sylancl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
190 189 oveq2d 
 |-  ( ph -> ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) = ( ( M + 1 ) / M ) )
191 190 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / M ) ) )
192 17 4 nndivred 
 |-  ( ph -> ( ( M + 1 ) / M ) e. RR )
193 192 recnd 
 |-  ( ph -> ( ( M + 1 ) / M ) e. CC )
194 114 193 132 135 div23d 
 |-  ( ph -> ( ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / M ) ) / ( ! ` M ) ) = ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / M ) ) )
195 191 194 eqtr4d 
 |-  ( ph -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) ) = ( ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / M ) ) / ( ! ` M ) ) )
196 114 193 132 135 divassd 
 |-  ( ph -> ( ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / M ) ) / ( ! ` M ) ) = ( ( ( abs ` A ) ^ M ) x. ( ( ( M + 1 ) / M ) / ( ! ` M ) ) ) )
197 4 nnne0d 
 |-  ( ph -> M =/= 0 )
198 119 56 132 197 135 divdiv1d 
 |-  ( ph -> ( ( ( M + 1 ) / M ) / ( ! ` M ) ) = ( ( M + 1 ) / ( M x. ( ! ` M ) ) ) )
199 56 132 mulcomd 
 |-  ( ph -> ( M x. ( ! ` M ) ) = ( ( ! ` M ) x. M ) )
200 199 oveq2d 
 |-  ( ph -> ( ( M + 1 ) / ( M x. ( ! ` M ) ) ) = ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) )
201 198 200 eqtrd 
 |-  ( ph -> ( ( ( M + 1 ) / M ) / ( ! ` M ) ) = ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) )
202 201 oveq2d 
 |-  ( ph -> ( ( ( abs ` A ) ^ M ) x. ( ( ( M + 1 ) / M ) / ( ! ` M ) ) ) = ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
203 195 196 202 3eqtrd 
 |-  ( ph -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( M + 1 ) / ( ( M + 1 ) - 1 ) ) ) = ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
204 186 203 breqtrd 
 |-  ( ph -> seq 0 ( + , H ) ~~> ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
205 seqex 
 |-  seq 0 ( + , H ) e. _V
206 ovex 
 |-  ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) e. _V
207 205 206 breldm 
 |-  ( seq 0 ( + , H ) ~~> ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) -> seq 0 ( + , H ) e. dom ~~> )
208 204 207 syl 
 |-  ( ph -> seq 0 ( + , H ) e. dom ~~> )
209 54 55 62 70 75 82 147 168 208 isumle 
 |-  ( ph -> sum_ j e. NN0 ( G ` ( M + j ) ) <_ sum_ j e. NN0 ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) )
210 eqid 
 |-  ( ZZ>= ` ( 0 + M ) ) = ( ZZ>= ` ( 0 + M ) )
211 fveq2 
 |-  ( k = ( M + j ) -> ( G ` k ) = ( G ` ( M + j ) ) )
212 56 addid2d 
 |-  ( ph -> ( 0 + M ) = M )
213 212 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( 0 + M ) ) = ( ZZ>= ` M ) )
214 213 eleq2d 
 |-  ( ph -> ( k e. ( ZZ>= ` ( 0 + M ) ) <-> k e. ( ZZ>= ` M ) ) )
215 214 biimpa 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + M ) ) ) -> k e. ( ZZ>= ` M ) )
216 215 43 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( 0 + M ) ) ) -> ( G ` k ) e. CC )
217 54 210 211 23 55 216 isumshft 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( 0 + M ) ) ( G ` k ) = sum_ j e. NN0 ( G ` ( M + j ) ) )
218 213 sumeq1d 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( 0 + M ) ) ( G ` k ) = sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
219 217 218 eqtr3d 
 |-  ( ph -> sum_ j e. NN0 ( G ` ( M + j ) ) = sum_ k e. ( ZZ>= ` M ) ( G ` k ) )
220 82 recnd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) e. CC )
221 54 55 75 220 204 isumclim 
 |-  ( ph -> sum_ j e. NN0 ( ( ( ( abs ` A ) ^ M ) / ( ! ` M ) ) x. ( ( 1 / ( M + 1 ) ) ^ j ) ) = ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
222 209 219 221 3brtr3d 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( G ` k ) <_ ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )
223 10 13 21 53 222 letrd 
 |-  ( ph -> ( abs ` sum_ k e. ( ZZ>= ` M ) ( F ` k ) ) <_ ( ( ( abs ` A ) ^ M ) x. ( ( M + 1 ) / ( ( ! ` M ) x. M ) ) ) )