Metamath Proof Explorer

Theorem plyeq0lem

Description: Lemma for plyeq0 . If A is the coefficient function for a nonzero polynomial such that P ( z ) = sum_ k e. NN0 A ( k ) x. z ^ k = 0 for every z e. CC and A ( M ) is the nonzero leading coefficient, then the function F ( z ) = P ( z ) / z ^ M is a sum of powers of 1 / z , and so the limit of this function as z ~> +oo is the constant term, A ( M ) . But F ( z ) = 0 everywhere, so this limit is also equal to zero so that A ( M ) = 0 , a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses plyeq0.1 
|- ( ph -> S C_ CC )
plyeq0.2 
|- ( ph -> N e. NN0 )
plyeq0.3 
|- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
plyeq0.4 
|- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
plyeq0.5 
|- ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
plyeq0.6 
|- M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
plyeq0.7 
|- ( ph -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
Assertion plyeq0lem 
|- -. ph

Proof

Step Hyp Ref Expression
1 plyeq0.1 
 |-  ( ph -> S C_ CC )
2 plyeq0.2 
 |-  ( ph -> N e. NN0 )
3 plyeq0.3 
 |-  ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
4 plyeq0.4 
 |-  ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
5 plyeq0.5 
 |-  ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
6 plyeq0.6 
 |-  M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
7 plyeq0.7 
 |-  ( ph -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
8 nnuz 
 |-  NN = ( ZZ>= ` 1 )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
11 1zzd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 1 e. ZZ )
12 0cn 
 |-  0 e. CC
13 12 a1i 
 |-  ( ph -> 0 e. CC )
14 13 snssd 
 |-  ( ph -> { 0 } C_ CC )
15 1 14 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
16 cnex 
 |-  CC e. _V
17 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
18 15 16 17 sylancl 
 |-  ( ph -> ( S u. { 0 } ) e. _V )
19 nn0ex 
 |-  NN0 e. _V
20 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
21 18 19 20 sylancl 
 |-  ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
22 3 21 mpbid 
 |-  ( ph -> A : NN0 --> ( S u. { 0 } ) )
23 22 15 fssd 
 |-  ( ph -> A : NN0 --> CC )
24 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
25 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
26 23 24 25 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
27 26 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( A ` k ) e. CC )
28 27 abscld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. RR )
29 28 recnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. CC )
30 divcnv 
 |-  ( ( abs ` ( A ` k ) ) e. CC -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
31 29 30 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
32 nnex 
 |-  NN e. _V
33 32 mptex 
 |-  ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V
34 33 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V )
35 oveq2 
 |-  ( n = m -> ( ( abs ` ( A ` k ) ) / n ) = ( ( abs ` ( A ` k ) ) / m ) )
36 eqid 
 |-  ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) )
37 ovex 
 |-  ( ( abs ` ( A ` k ) ) / m ) e. _V
38 35 36 37 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
39 38 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
40 nndivre 
 |-  ( ( ( abs ` ( A ` k ) ) e. RR /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
41 28 40 sylan 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
42 39 41 eqeltrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) e. RR )
43 oveq1 
 |-  ( n = m -> ( n ^ ( k - M ) ) = ( m ^ ( k - M ) ) )
44 43 oveq2d 
 |-  ( n = m -> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
45 eqid 
 |-  ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) )
46 ovex 
 |-  ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. _V
47 44 45 46 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
48 47 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
49 26 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( A ` k ) e. CC )
50 49 abscld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. RR )
51 nnrp 
 |-  ( m e. NN -> m e. RR+ )
52 51 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR+ )
53 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
54 cnvimass 
 |-  ( `' A " ( S \ { 0 } ) ) C_ dom A
55 54 22 fssdm 
 |-  ( ph -> ( `' A " ( S \ { 0 } ) ) C_ NN0 )
56 nn0ssz 
 |-  NN0 C_ ZZ
57 55 56 sstrdi 
 |-  ( ph -> ( `' A " ( S \ { 0 } ) ) C_ ZZ )
58 2 nn0red 
 |-  ( ph -> N e. RR )
59 22 ffnd 
 |-  ( ph -> A Fn NN0 )
60 elpreima 
 |-  ( A Fn NN0 -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
61 59 60 syl 
 |-  ( ph -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
62 61 simplbda 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) e. ( S \ { 0 } ) )
63 eldifsni 
 |-  ( ( A ` z ) e. ( S \ { 0 } ) -> ( A ` z ) =/= 0 )
64 62 63 syl 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) =/= 0 )
65 fveq2 
 |-  ( k = z -> ( A ` k ) = ( A ` z ) )
66 65 neeq1d 
 |-  ( k = z -> ( ( A ` k ) =/= 0 <-> ( A ` z ) =/= 0 ) )
67 breq1 
 |-  ( k = z -> ( k <_ N <-> z <_ N ) )
68 66 67 imbi12d 
 |-  ( k = z -> ( ( ( A ` k ) =/= 0 -> k <_ N ) <-> ( ( A ` z ) =/= 0 -> z <_ N ) ) )
69 plyco0 
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
70 2 23 69 syl2anc 
 |-  ( ph -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
71 4 70 mpbid 
 |-  ( ph -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
72 71 adantr 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
73 55 sselda 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z e. NN0 )
74 68 72 73 rspcdva 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( ( A ` z ) =/= 0 -> z <_ N ) )
75 64 74 mpd 
 |-  ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z <_ N )
76 75 ralrimiva 
 |-  ( ph -> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N )
77 brralrspcev 
 |-  ( ( N e. RR /\ A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
78 58 76 77 syl2anc 
 |-  ( ph -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
79 suprzcl 
 |-  ( ( ( `' A " ( S \ { 0 } ) ) C_ ZZ /\ ( `' A " ( S \ { 0 } ) ) =/= (/) /\ E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x ) -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. ( `' A " ( S \ { 0 } ) ) )
80 57 7 78 79 syl3anc 
 |-  ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. ( `' A " ( S \ { 0 } ) ) )
81 6 80 eqeltrid 
 |-  ( ph -> M e. ( `' A " ( S \ { 0 } ) ) )
82 55 81 sseldd 
 |-  ( ph -> M e. NN0 )
83 82 nn0zd 
 |-  ( ph -> M e. ZZ )
84 zsubcl 
 |-  ( ( k e. ZZ /\ M e. ZZ ) -> ( k - M ) e. ZZ )
85 53 83 84 syl2anr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
86 85 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. ZZ )
87 52 86 rpexpcld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR+ )
88 87 rpred 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR )
89 50 88 remulcld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. RR )
90 48 89 eqeltrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. RR )
91 nnrecre 
 |-  ( m e. NN -> ( 1 / m ) e. RR )
92 91 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( 1 / m ) e. RR )
93 27 absge0d 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 0 <_ ( abs ` ( A ` k ) ) )
94 93 adantr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( abs ` ( A ` k ) ) )
95 nnre 
 |-  ( m e. NN -> m e. RR )
96 95 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR )
97 nnge1 
 |-  ( m e. NN -> 1 <_ m )
98 97 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ m )
99 1red 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 e. RR )
100 86 zred 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. RR )
101 simplr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k < M )
102 53 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ZZ )
103 102 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. ZZ )
104 83 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. ZZ )
105 zltp1le 
 |-  ( ( k e. ZZ /\ M e. ZZ ) -> ( k < M <-> ( k + 1 ) <_ M ) )
106 103 104 105 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k < M <-> ( k + 1 ) <_ M ) )
107 101 106 mpbid 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k + 1 ) <_ M )
108 24 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
109 108 nn0red 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. RR )
110 109 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. RR )
111 82 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> M e. NN0 )
112 111 nn0red 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> M e. RR )
113 112 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. RR )
114 110 99 113 leaddsub2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( k + 1 ) <_ M <-> 1 <_ ( M - k ) ) )
115 107 114 mpbid 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ ( M - k ) )
116 109 recnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
117 116 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. CC )
118 112 recnd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> M e. CC )
119 118 ad2antrr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. CC )
120 117 119 negsubdi2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u ( k - M ) = ( M - k ) )
121 115 120 breqtrrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ -u ( k - M ) )
122 99 100 121 lenegcon2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) <_ -u 1 )
123 neg1z 
 |-  -u 1 e. ZZ
124 eluz 
 |-  ( ( ( k - M ) e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
125 86 123 124 sylancl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
126 122 125 mpbird 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u 1 e. ( ZZ>= ` ( k - M ) ) )
127 96 98 126 leexp2ad 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( m ^ -u 1 ) )
128 nncn 
 |-  ( m e. NN -> m e. CC )
129 128 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. CC )
130 expn1 
 |-  ( m e. CC -> ( m ^ -u 1 ) = ( 1 / m ) )
131 129 130 syl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ -u 1 ) = ( 1 / m ) )
132 127 131 breqtrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( 1 / m ) )
133 88 92 50 94 132 lemul2ad 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
134 29 adantr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. CC )
135 nnne0 
 |-  ( m e. NN -> m =/= 0 )
136 135 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m =/= 0 )
137 134 129 136 divrecd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) = ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
138 39 137 eqtrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
139 133 48 138 3brtr4d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) <_ ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) )
140 87 rpge0d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( m ^ ( k - M ) ) )
141 50 88 94 140 mulge0d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
142 141 48 breqtrrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
143 8 11 31 34 42 90 139 142 climsqz2 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
144 32 mptex 
 |-  ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V
145 144 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V )
146 43 oveq2d 
 |-  ( n = m -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
147 eqid 
 |-  ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) )
148 ovex 
 |-  ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. _V
149 146 147 148 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
150 149 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
151 23 adantr 
 |-  ( ( ph /\ m e. NN ) -> A : NN0 --> CC )
152 151 24 25 syl2an 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
153 128 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m e. CC )
154 135 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m =/= 0 )
155 83 adantr 
 |-  ( ( ph /\ m e. NN ) -> M e. ZZ )
156 53 155 84 syl2anr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
157 153 154 156 expclzd 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) e. CC )
158 152 157 mulcld 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. CC )
159 150 158 eqeltrd 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
160 159 an32s 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
161 160 adantlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
162 88 recnd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. CC )
163 49 162 absmuld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( ( A ` k ) x. ( m ^ ( k - M ) ) ) ) = ( ( abs ` ( A ` k ) ) x. ( abs ` ( m ^ ( k - M ) ) ) ) )
164 88 140 absidd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( m ^ ( k - M ) ) ) = ( m ^ ( k - M ) ) )
165 164 oveq2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( abs ` ( m ^ ( k - M ) ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
166 163 165 eqtrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( ( A ` k ) x. ( m ^ ( k - M ) ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
167 149 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
168 167 fveq2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) ) = ( abs ` ( ( A ` k ) x. ( m ^ ( k - M ) ) ) ) )
169 166 168 48 3eqtr4rd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( abs ` ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) ) )
170 8 11 145 34 161 169 climabs0 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 <-> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 ) )
171 143 170 mpbird 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
172 109 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k e. RR )
173 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k < M )
174 172 173 ltned 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k =/= M )
175 velsn 
 |-  ( k e. { M } <-> k = M )
176 175 necon3bbii 
 |-  ( -. k e. { M } <-> k =/= M )
177 174 176 sylibr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> -. k e. { M } )
178 177 iffalsed 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
179 171 178 breqtrrd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
180 nncn 
 |-  ( n e. NN -> n e. CC )
181 180 ad2antlr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n e. CC )
182 nnne0 
 |-  ( n e. NN -> n =/= 0 )
183 182 ad2antlr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n =/= 0 )
184 85 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( k - M ) e. ZZ )
185 181 183 184 expclzd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( n ^ ( k - M ) ) e. CC )
186 185 mul02d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( 0 x. ( n ^ ( k - M ) ) ) = 0 )
187 simpr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( A ` k ) = 0 )
188 187 oveq1d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( 0 x. ( n ^ ( k - M ) ) ) )
189 187 ifeq1d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = if ( k e. { M } , 0 , 0 ) )
190 ifid 
 |-  if ( k e. { M } , 0 , 0 ) = 0
191 189 190 eqtrdi 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
192 186 188 191 3eqtr4d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = if ( k e. { M } , ( A ` k ) , 0 ) )
193 26 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( A ` k ) e. CC )
194 193 ad2antrr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. CC )
195 194 mulridd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. 1 ) = ( A ` k ) )
196 nn0ssre 
 |-  NN0 C_ RR
197 55 196 sstrdi 
 |-  ( ph -> ( `' A " ( S \ { 0 } ) ) C_ RR )
198 197 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) C_ RR )
199 7 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
200 78 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
201 24 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. NN0 )
202 ffvelcdm 
 |-  ( ( A : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( A ` k ) e. ( S u. { 0 } ) )
203 22 24 202 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. ( S u. { 0 } ) )
204 203 anim1i 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
205 eldifsn 
 |-  ( ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) <-> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
206 204 205 sylibr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) )
207 difun2 
 |-  ( ( S u. { 0 } ) \ { 0 } ) = ( S \ { 0 } )
208 206 207 eleqtrdi 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( S \ { 0 } ) )
209 elpreima 
 |-  ( A Fn NN0 -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
210 59 209 syl 
 |-  ( ph -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
211 210 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
212 201 208 211 mpbir2and 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. ( `' A " ( S \ { 0 } ) ) )
213 198 199 200 212 suprubd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) )
214 213 6 breqtrrdi 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
215 214 ad4ant14 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
216 simpllr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M <_ k )
217 109 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. RR )
218 112 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. RR )
219 217 218 letri3d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k = M <-> ( k <_ M /\ M <_ k ) ) )
220 215 216 219 mpbir2and 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k = M )
221 220 oveq1d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = ( M - M ) )
222 118 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. CC )
223 222 subidd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( M - M ) = 0 )
224 221 223 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = 0 )
225 224 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = ( n ^ 0 ) )
226 180 ad2antlr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> n e. CC )
227 226 exp0d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ 0 ) = 1 )
228 225 227 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = 1 )
229 228 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. 1 ) )
230 220 175 sylibr 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. { M } )
231 230 iftrued 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` k ) )
232 195 229 231 3eqtr4d 
 |-  ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = if ( k e. { M } , ( A ` k ) , 0 ) )
233 192 232 pm2.61dane 
 |-  ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = if ( k e. { M } , ( A ` k ) , 0 ) )
234 233 mpteq2dva 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> if ( k e. { M } , ( A ` k ) , 0 ) ) )
235 fconstmpt 
 |-  ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) = ( n e. NN |-> if ( k e. { M } , ( A ` k ) , 0 ) )
236 234 235 eqtr4di 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) )
237 ifcl 
 |-  ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
238 193 12 237 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
239 1z 
 |-  1 e. ZZ
240 8 eqimss2i 
 |-  ( ZZ>= ` 1 ) C_ NN
241 240 32 climconst2 
 |-  ( ( if ( k e. { M } , ( A ` k ) , 0 ) e. CC /\ 1 e. ZZ ) -> ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
242 238 239 241 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
243 236 242 eqbrtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
244 179 243 109 112 ltlecasei 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
245 snex 
 |-  { 0 } e. _V
246 32 245 xpex 
 |-  ( NN X. { 0 } ) e. _V
247 246 a1i 
 |-  ( ph -> ( NN X. { 0 } ) e. _V )
248 160 anasss 
 |-  ( ( ph /\ ( k e. ( 0 ... N ) /\ m e. NN ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
249 5 fveq1d 
 |-  ( ph -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
250 249 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
251 128 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
252 0pval 
 |-  ( m e. CC -> ( 0p ` m ) = 0 )
253 251 252 syl 
 |-  ( ( ph /\ m e. NN ) -> ( 0p ` m ) = 0 )
254 oveq1 
 |-  ( z = m -> ( z ^ k ) = ( m ^ k ) )
255 254 oveq2d 
 |-  ( z = m -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( m ^ k ) ) )
256 255 sumeq2sdv 
 |-  ( z = m -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
257 eqid 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) )
258 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) e. _V
259 256 257 258 fvmpt 
 |-  ( m e. CC -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
260 251 259 syl 
 |-  ( ( ph /\ m e. NN ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
261 250 253 260 3eqtr3d 
 |-  ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
262 261 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = ( sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
263 expcl 
 |-  ( ( m e. CC /\ M e. NN0 ) -> ( m ^ M ) e. CC )
264 128 82 263 syl2anr 
 |-  ( ( ph /\ m e. NN ) -> ( m ^ M ) e. CC )
265 135 adantl 
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
266 251 265 155 expne0d 
 |-  ( ( ph /\ m e. NN ) -> ( m ^ M ) =/= 0 )
267 264 266 div0d 
 |-  ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = 0 )
268 fzfid 
 |-  ( ( ph /\ m e. NN ) -> ( 0 ... N ) e. Fin )
269 expcl 
 |-  ( ( m e. CC /\ k e. NN0 ) -> ( m ^ k ) e. CC )
270 251 24 269 syl2an 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ k ) e. CC )
271 152 270 mulcld 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ k ) ) e. CC )
272 268 264 271 266 fsumdivc 
 |-  ( ( ph /\ m e. NN ) -> ( sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
273 262 267 272 3eqtr3d 
 |-  ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
274 fvconst2g 
 |-  ( ( 0 e. CC /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
275 13 274 sylan 
 |-  ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
276 155 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> M e. ZZ )
277 53 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> k e. ZZ )
278 153 154 276 277 expsubd 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) = ( ( m ^ k ) / ( m ^ M ) ) )
279 278 oveq2d 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
280 264 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) e. CC )
281 266 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) =/= 0 )
282 152 270 280 281 divassd 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
283 279 150 282 3eqtr4d 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
284 283 sumeq2dv 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 0 ... N ) ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
285 273 275 284 3eqtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = sum_ k e. ( 0 ... N ) ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
286 8 9 10 244 247 248 285 climfsum 
 |-  ( ph -> ( NN X. { 0 } ) ~~> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
287 suprleub 
 |-  ( ( ( ( `' A " ( S \ { 0 } ) ) C_ RR /\ ( `' A " ( S \ { 0 } ) ) =/= (/) /\ E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x ) /\ N e. RR ) -> ( sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
288 197 7 78 58 287 syl31anc 
 |-  ( ph -> ( sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
289 76 288 mpbird 
 |-  ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N )
290 6 289 eqbrtrid 
 |-  ( ph -> M <_ N )
291 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
292 82 291 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
293 2 nn0zd 
 |-  ( ph -> N e. ZZ )
294 elfz5 
 |-  ( ( M e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( M e. ( 0 ... N ) <-> M <_ N ) )
295 292 293 294 syl2anc 
 |-  ( ph -> ( M e. ( 0 ... N ) <-> M <_ N ) )
296 290 295 mpbird 
 |-  ( ph -> M e. ( 0 ... N ) )
297 296 snssd 
 |-  ( ph -> { M } C_ ( 0 ... N ) )
298 23 82 ffvelcdmd 
 |-  ( ph -> ( A ` M ) e. CC )
299 elsni 
 |-  ( k e. { M } -> k = M )
300 299 fveq2d 
 |-  ( k e. { M } -> ( A ` k ) = ( A ` M ) )
301 300 eleq1d 
 |-  ( k e. { M } -> ( ( A ` k ) e. CC <-> ( A ` M ) e. CC ) )
302 298 301 syl5ibrcom 
 |-  ( ph -> ( k e. { M } -> ( A ` k ) e. CC ) )
303 302 ralrimiv 
 |-  ( ph -> A. k e. { M } ( A ` k ) e. CC )
304 10 olcd 
 |-  ( ph -> ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin ) )
305 sumss2 
 |-  ( ( ( { M } C_ ( 0 ... N ) /\ A. k e. { M } ( A ` k ) e. CC ) /\ ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin ) ) -> sum_ k e. { M } ( A ` k ) = sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
306 297 303 304 305 syl21anc 
 |-  ( ph -> sum_ k e. { M } ( A ` k ) = sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
307 ltso 
 |-  < Or RR
308 307 supex 
 |-  sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. _V
309 6 308 eqeltri 
 |-  M e. _V
310 fveq2 
 |-  ( k = M -> ( A ` k ) = ( A ` M ) )
311 310 sumsn 
 |-  ( ( M e. _V /\ ( A ` M ) e. CC ) -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
312 309 298 311 sylancr 
 |-  ( ph -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
313 306 312 eqtr3d 
 |-  ( ph -> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` M ) )
314 286 313 breqtrd 
 |-  ( ph -> ( NN X. { 0 } ) ~~> ( A ` M ) )
315 240 32 climconst2 
 |-  ( ( 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ~~> 0 )
316 12 239 315 mp2an 
 |-  ( NN X. { 0 } ) ~~> 0
317 climuni 
 |-  ( ( ( NN X. { 0 } ) ~~> ( A ` M ) /\ ( NN X. { 0 } ) ~~> 0 ) -> ( A ` M ) = 0 )
318 314 316 317 sylancl 
 |-  ( ph -> ( A ` M ) = 0 )
319 fvex 
 |-  ( A ` M ) e. _V
320 319 elsn 
 |-  ( ( A ` M ) e. { 0 } <-> ( A ` M ) = 0 )
321 318 320 sylibr 
 |-  ( ph -> ( A ` M ) e. { 0 } )
322 elpreima 
 |-  ( A Fn NN0 -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
323 59 322 syl 
 |-  ( ph -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
324 81 323 mpbid 
 |-  ( ph -> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) )
325 324 simprd 
 |-  ( ph -> ( A ` M ) e. ( S \ { 0 } ) )
326 325 eldifbd 
 |-  ( ph -> -. ( A ` M ) e. { 0 } )
327 321 326 pm2.65i 
 |-  -. ph