Theorem plyeq0lem 20082

Description: Lemma for plyeq0 20083. 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.)

Hypotheses

Ref	Expression
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 -> 0 p = ( 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

Ref	Expression
plyeq0lem	|- -. ph

Distinct variable groups:   z, k, A   k, M   k, N, z   ph, k, z   S, k, z

Allowed substitution hint:   M( z)

Proof of Theorem plyeq0lem

Dummy variables m n x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 10477	. . . . . 6 |- NN = ( ZZ>= ` 1 )
2		1z 10267	. . . . . . 7 |- 1 e. ZZ
3	2	a1i 11	. . . . . 6 |- ( ph -> 1 e. ZZ )
4		fzfid 11267	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
5	2	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 1 e. ZZ )
6		plyeq0.3	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
7		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> S C_ CC )
8		0cn 9040	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. CC
9	8	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 0 e. CC )
10	9	snssd 3903	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { 0 } C_ CC )
11	7, 10	unssd 3483	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( S u. { 0 } ) C_ CC )
12		cnex 9027	. . . . . . . . . . . . . . . . . . 19 |- CC e. _V
13		ssexg 4309	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
14	11, 12, 13	sylancl 644	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S u. { 0 } ) e. _V )
15		nn0ex 10183	. . . . . . . . . . . . . . . . . 18 |- NN0 e. _V
16		elmapg 6990	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
17	14, 15, 16	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
18	6, 17	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ph -> A : NN0 --> ( S u. { 0 } ) )
19		fss 5558	. . . . . . . . . . . . . . . 16 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ ( S u. { 0 } ) C_ CC ) -> A : NN0 --> CC )
20	18, 11, 19	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> A : NN0 --> CC )
21		elfznn0 11039	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... N ) -> k e. NN0 )
22		ffvelrn 5827	. . . . . . . . . . . . . . 15 |- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
23	20, 21, 22	syl2an 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
24	23	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( A ` k ) e. CC )
25	24	abscld 12193	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. RR )
26	25	recnd 9070	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. CC )
27		divcnv 12588	. . . . . . . . . . 11 |- ( ( abs ` ( A ` k ) ) e. CC -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
28	26, 27	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
29		nnex 9962	. . . . . . . . . . . 12 |- NN e. _V
30	29	mptex 5925	. . . . . . . . . . 11 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V
31	30	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V )
32		oveq2 6048	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) / n ) = ( ( abs ` ( A ` k ) ) / m ) )
33		eqid 2404	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) )
34		ovex 6065	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) / m ) e. _V
35	32, 33, 34	fvmpt 5765	. . . . . . . . . . . 12 |- ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
36	35	adantl 453	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
37		nndivre 9991	. . . . . . . . . . . 12 |- ( ( ( abs ` ( A ` k ) ) e. RR /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
38	25, 37	sylan 458	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
39	36, 38	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) e. RR )
40		oveq1 6047	. . . . . . . . . . . . . 14 |- ( n = m -> ( n ^ ( k - M ) ) = ( m ^ ( k - M ) ) )
41	40	oveq2d 6056	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
42		eqid 2404	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) )
43		ovex 6065	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. _V
44	41, 42, 43	fvmpt 5765	. . . . . . . . . . . 12 |- ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
45	44	adantl 453	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
46	23	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( A ` k ) e. CC )
47	46	abscld 12193	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. RR )
48		nnrp 10577	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR+ )
49	48	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR+ )
50		elfzelz 11015	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... N ) -> k e. ZZ )
51		cnvimass 5183	. . . . . . . . . . . . . . . . . . 19 |- ( `' A " ( S \ { 0 } ) ) C_ dom A
52		fdm 5554	. . . . . . . . . . . . . . . . . . . 20 |- ( A : NN0 --> ( S u. { 0 } ) -> dom A = NN0 )
53	18, 52	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom A = NN0 )
54	51, 53	syl5sseq 3356	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ NN0 )
55		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 |- M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
56		nn0ssz 10258	. . . . . . . . . . . . . . . . . . . . 21 |- NN0 C_ ZZ
57	54, 56	syl6ss 3320	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ ZZ )
58		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
59		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> N e. NN0 )
60	59	nn0red 10231	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. RR )
61	54	sselda 3308	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z e. NN0 )
62		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
63		plyco0 20064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
64	59, 20, 63	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
65	62, 64	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
66	65	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
67		ffn 5550	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A : NN0 --> ( S u. { 0 } ) -> A Fn NN0 )
68	18, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A Fn NN0 )
69		elpreima 5809	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A Fn NN0 -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
71	70	simplbda 608	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) e. ( S \ { 0 } ) )
72		eldifsni 3888	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A ` z ) e. ( S \ { 0 } ) -> ( A ` z ) =/= 0 )
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) =/= 0 )
74		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = z -> ( A ` k ) = ( A ` z ) )
75	74	neeq1d 2580	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = z -> ( ( A ` k ) =/= 0 <-> ( A ` z ) =/= 0 ) )
76		breq1 4175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = z -> ( k <_ N <-> z <_ N ) )
77	75, 76	imbi12d 312	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = z -> ( ( ( A ` k ) =/= 0 -> k <_ N ) <-> ( ( A ` z ) =/= 0 -> z <_ N ) ) )
78	77	rspcv 3008	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. NN0 -> ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) -> ( ( A ` z ) =/= 0 -> z <_ N ) ) )
79	61, 66, 73, 78	syl3c 59	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z <_ N )
80	79	ralrimiva 2749	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N )
81		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = N -> ( z <_ x <-> z <_ N ) )
82	81	ralbidv 2686	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = N -> ( A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
83	82	rspcev 3012	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. RR /\ A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
84	60, 80, 83	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
85		suprzcl 10305	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( `' 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 } ) ) )
86	57, 58, 84, 85	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. ( `' A " ( S \ { 0 } ) ) )
87	55, 86	syl5eqel 2488	. . . . . . . . . . . . . . . . . 18 |- ( ph -> M e. ( `' A " ( S \ { 0 } ) ) )
88	54, 87	sseldd 3309	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. NN0 )
89	88	nn0zd 10329	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. ZZ )
90		zsubcl 10275	. . . . . . . . . . . . . . . 16 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k - M ) e. ZZ )
91	50, 89, 90	syl2anr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
92	91	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. ZZ )
93	49, 92	rpexpcld 11501	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR+ )
94	93	rpred 10604	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR )
95	47, 94	remulcld 9072	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. RR )
96	45, 95	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. RR )
97		nnrecre 9992	. . . . . . . . . . . . 13 |- ( m e. NN -> ( 1 / m ) e. RR )
98	97	adantl 453	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( 1 / m ) e. RR )
99	24	absge0d 12201	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 0 <_ ( abs ` ( A ` k ) ) )
100	99	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( abs ` ( A ` k ) ) )
101		nnre 9963	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR )
102	101	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR )
103		nnge1 9982	. . . . . . . . . . . . . . 15 |- ( m e. NN -> 1 <_ m )
104	103	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ m )
105		1re 9046	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
106	105	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 e. RR )
107	92	zred 10331	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. RR )
108		simplr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k < M )
109	50	adantl 453	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ZZ )
110	109	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. ZZ )
111	89	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. ZZ )
112		zltp1le 10281	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k < M <-> ( k + 1 ) <_ M ) )
113	110, 111, 112	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k < M <-> ( k + 1 ) <_ M ) )
114	108, 113	mpbid 202	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k + 1 ) <_ M )
115	21	adantl 453	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
116	115	nn0red 10231	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. RR )
117	116	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. RR )
118	88	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. NN0 )
119	118	nn0red 10231	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. RR )
120	119	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. RR )
121	117, 106, 120	leaddsub2d 9584	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( k + 1 ) <_ M <-> 1 <_ ( M - k ) ) )
122	114, 121	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ ( M - k ) )
123	116	recnd 9070	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
124	123	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. CC )
125	119	recnd 9070	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. CC )
126	125	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. CC )
127	124, 126	negsubdi2d 9383	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u ( k - M ) = ( M - k ) )
128	122, 127	breqtrrd 4198	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ -u ( k - M ) )
129	106, 107, 128	lenegcon2d 9565	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) <_ -u 1 )
130		znegcl 10269	. . . . . . . . . . . . . . . . 17 |- ( 1 e. ZZ -> -u 1 e. ZZ )
131	2, 130	ax-mp 8	. . . . . . . . . . . . . . . 16 |- -u 1 e. ZZ
132		eluz 10455	. . . . . . . . . . . . . . . 16 |- ( ( ( k - M ) e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
133	92, 131, 132	sylancl 644	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
134	129, 133	mpbird 224	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u 1 e. ( ZZ>= ` ( k - M ) ) )
135	102, 104, 134	leexp2ad 11510	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( m ^ -u 1 ) )
136		nncn 9964	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. CC )
137	136	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. CC )
138		expn1 11346	. . . . . . . . . . . . . 14 |- ( m e. CC -> ( m ^ -u 1 ) = ( 1 / m ) )
139	137, 138	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ -u 1 ) = ( 1 / m ) )
140	135, 139	breqtrd 4196	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( 1 / m ) )
141	94, 98, 47, 100, 140	lemul2ad 9907	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
142	26	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. CC )
143		nnne0 9988	. . . . . . . . . . . . . 14 |- ( m e. NN -> m =/= 0 )
144	143	adantl 453	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m =/= 0 )
145	142, 137, 144	divrecd 9749	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) = ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
146	36, 145	eqtrd 2436	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
147	141, 45, 146	3brtr4d 4202	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
148	93	rpge0d 10608	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( m ^ ( k - M ) ) )
149	47, 94, 100, 148	mulge0d 9559	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
150	149, 45	breqtrrd 4198	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
151	1, 5, 28, 31, 39, 96, 147, 150	climsqz2 12390	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
152	29	mptex 5925	. . . . . . . . . . 11 |- ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V
153	152	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V )
154	40	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( n = m -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
155		eqid 2404	. . . . . . . . . . . . . . 15 |- ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) )
156		ovex 6065	. . . . . . . . . . . . . . 15 |- ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. _V
157	154, 155, 156	fvmpt 5765	. . . . . . . . . . . . . 14 |- ( m e. NN -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
158	157	ad2antlr 708	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
159	20	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. NN ) -> A : NN0 --> CC )
160	159, 21, 22	syl2an 464	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
161	136	ad2antlr 708	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m e. CC )
162	143	ad2antlr 708	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m =/= 0 )
163	89	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. NN ) -> M e. ZZ )
164	50, 163, 90	syl2anr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
165	161, 162, 164	expclzd 11483	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) e. CC )
166	160, 165	mulcld 9064	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. CC )
167	158, 166	eqeltrd 2478	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
168	167	an32s 780	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
169	168	adantlr 696	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
170	94	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. CC )
171	46, 170	absmuld 12211	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) ) )
172	94, 148	absidd 12180	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( m ^ ( k - M ) ) ) = ( m ^ ( k - M ) ) )
173	172	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
174	171, 173	eqtrd 2436	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( ( A ` k ) x. ( m ^ ( k - M ) ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
175	157	adantl 453	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
176	175	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) ) )
177	174, 176, 45	3eqtr4rd 2447	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
178	1, 5, 153, 31, 169, 177	climabs0 12334	. . . . . . . . 9 |- ( ( ( 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 ) )
179	151, 178	mpbird 224	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
180	116	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k e. RR )
181		simpr 448	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k < M )
182	180, 181	ltned 9165	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k =/= M )
183		elsn 3789	. . . . . . . . . . 11 |- ( k e. { M } <-> k = M )
184	183	necon3bbii 2598	. . . . . . . . . 10 |- ( -. k e. { M } <-> k =/= M )
185	182, 184	sylibr 204	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> -. k e. { M } )
186		iffalse 3706	. . . . . . . . 9 |- ( -. k e. { M } -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
187	185, 186	syl 16	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
188	179, 187	breqtrrd 4198	. . . . . . 7 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
189		nncn 9964	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n e. CC )
190	189	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n e. CC )
191		nnne0 9988	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n =/= 0 )
192	191	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n =/= 0 )
193	91	ad3antrrr 711	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( k - M ) e. ZZ )
194	190, 192, 193	expclzd 11483	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( n ^ ( k - M ) ) e. CC )
195	194	mul02d 9220	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( 0 x. ( n ^ ( k - M ) ) ) = 0 )
196		simpr 448	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( A ` k ) = 0 )
197	196	oveq1d 6055	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( 0 x. ( n ^ ( k - M ) ) ) )
198	196	ifeq1d 3713	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
199		ifid 3731	. . . . . . . . . . . . 13 |- if ( k e. { M } , 0 , 0 ) = 0
200	198, 199	syl6eq 2452	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
201	195, 197, 200	3eqtr4d 2446	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
202	23	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( A ` k ) e. CC )
203	202	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. CC )
204	203	mulid1d 9061	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. 1 ) = ( A ` k ) )
205		nn0ssre 10181	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 C_ RR
206	54, 205	syl6ss 3320	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ RR )
207	206	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) C_ RR )
208	58	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
209	84	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
210	21	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. NN0 )
211		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( A ` k ) e. ( S u. { 0 } ) )
212	18, 21, 211	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. ( S u. { 0 } ) )
213	212	anim1i 552	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
214		eldifsn 3887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) <-> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
215	213, 214	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) )
216		difun2 3667	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S u. { 0 } ) \ { 0 } ) = ( S \ { 0 } )
217	215, 216	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( S \ { 0 } ) )
218		elpreima 5809	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A Fn NN0 -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
219	68, 218	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
220	219	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
221	210, 217, 220	mpbir2and 889	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. ( `' A " ( S \ { 0 } ) ) )
222		suprub 9925	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( `' A " ( S \ { 0 } ) ) C_ RR /\ ( `' A " ( S \ { 0 } ) ) =/= (/) /\ E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x ) /\ k e. ( `' A " ( S \ { 0 } ) ) ) -> k <_ sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) )
223	207, 208, 209, 221, 222	syl31anc 1187	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) )
224	223, 55	syl6breqr 4212	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
225	224	adantlr 696	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
226	225	adantlr 696	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
227		simpllr 736	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M <_ k )
228	116	ad3antrrr 711	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. RR )
229	119	ad3antrrr 711	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. RR )
230	228, 229	letri3d 9171	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k = M <-> ( k <_ M /\ M <_ k ) ) )
231	226, 227, 230	mpbir2and 889	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k = M )
232	231	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = ( M - M ) )
233	125	ad3antrrr 711	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. CC )
234	233	subidd 9355	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( M - M ) = 0 )
235	232, 234	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = 0 )
236	235	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = ( n ^ 0 ) )
237	189	ad2antlr 708	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> n e. CC )
238	237	exp0d 11472	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ 0 ) = 1 )
239	236, 238	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = 1 )
240	239	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. 1 ) )
241	231, 183	sylibr 204	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. { M } )
242		iftrue 3705	. . . . . . . . . . . . 13 |- ( k e. { M } -> if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` k ) )
243	241, 242	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` k ) )
244	204, 240, 243	3eqtr4d 2446	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
245	201, 244	pm2.61dane 2645	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = if ( k e. { M } , ( A ` k ) , 0 ) )
246	245	mpteq2dva 4255	. . . . . . . . 9 |- ( ( ( 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 ) ) )
247		fconstmpt 4880	. . . . . . . . 9 |- ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) = ( n e. NN |-> if ( k e. { M } , ( A ` k ) , 0 ) )
248	246, 247	syl6eqr 2454	. . . . . . . 8 |- ( ( ( 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 ) } ) )
249		ifcl 3735	. . . . . . . . . 10 |- ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
250	202, 8, 249	sylancl 644	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
251	1	eqimss2i 3363	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
252	251, 29	climconst2 12297	. . . . . . . . 9 |- ( ( 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 ) )
253	250, 2, 252	sylancl 644	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
254	248, 253	eqbrtrd 4192	. . . . . . 7 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
255	188, 254, 116, 119	ltlecasei 9137	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
256		snex 4365	. . . . . . . 8 |- { 0 } e. _V
257	29, 256	xpex 4949	. . . . . . 7 |- ( NN X. { 0 } ) e. _V
258	257	a1i 11	. . . . . 6 |- ( ph -> ( NN X. { 0 } ) e. _V )
259	168	anasss 629	. . . . . 6 |- ( ( ph /\ ( k e. ( 0 ... N ) /\ m e. NN ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
260		plyeq0.5	. . . . . . . . . . . 12 |- ( ph -> 0 p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
261	260	fveq1d 5689	. . . . . . . . . . 11 |- ( ph -> ( 0 p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
262	261	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0 p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
263	136	adantl 453	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN ) -> m e. CC )
264		0pval 19516	. . . . . . . . . . 11 |- ( m e. CC -> ( 0 p ` m ) = 0 )
265	263, 264	syl 16	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0 p ` m ) = 0 )
266		oveq1 6047	. . . . . . . . . . . . . 14 |- ( z = m -> ( z ^ k ) = ( m ^ k ) )
267	266	oveq2d 6056	. . . . . . . . . . . . 13 |- ( z = m -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( m ^ k ) ) )
268	267	sumeq2sdv 12453	. . . . . . . . . . . 12 |- ( z = m -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
269		eqid 2404	. . . . . . . . . . . 12 |- ( 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 ) ) )
270		sumex 12436	. . . . . . . . . . . 12 |- sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) e. _V
271	268, 269, 270	fvmpt 5765	. . . . . . . . . . 11 |- ( 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 ) ) )
272	263, 271	syl 16	. . . . . . . . . 10 |- ( ( 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 ) ) )
273	262, 265, 272	3eqtr3d 2444	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
274	273	oveq1d 6055	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = ( sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
275		expcl 11354	. . . . . . . . . 10 |- ( ( m e. CC /\ M e. NN0 ) -> ( m ^ M ) e. CC )
276	136, 88, 275	syl2anr 465	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) e. CC )
277	143	adantl 453	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> m =/= 0 )
278	263, 277, 163	expne0d 11484	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) =/= 0 )
279	276, 278	div0d 9745	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = 0 )
280		fzfid 11267	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( 0 ... N ) e. Fin )
281		expcl 11354	. . . . . . . . . . 11 |- ( ( m e. CC /\ k e. NN0 ) -> ( m ^ k ) e. CC )
282	263, 21, 281	syl2an 464	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ k ) e. CC )
283	160, 282	mulcld 9064	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ k ) ) e. CC )
284	280, 276, 283, 278	fsumdivc 12524	. . . . . . . 8 |- ( ( 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 ) ) )
285	274, 279, 284	3eqtr3d 2444	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
286		fvconst2g 5904	. . . . . . . 8 |- ( ( 0 e. CC /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
287	9, 286	sylan 458	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
288	163	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> M e. ZZ )
289	50	adantl 453	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> k e. ZZ )
290	161, 162, 288, 289	expsubd 11489	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) = ( ( m ^ k ) / ( m ^ M ) ) )
291	290	oveq2d 6056	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
292	276	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) e. CC )
293	278	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) =/= 0 )
294	160, 282, 292, 293	divassd 9781	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
295	291, 158, 294	3eqtr4d 2446	. . . . . . . 8 |- ( ( ( 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 ) ) )
296	295	sumeq2dv 12452	. . . . . . 7 |- ( ( 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 ) ) )
297	285, 287, 296	3eqtr4d 2446	. . . . . 6 |- ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = sum_ k e. ( 0 ... N ) ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
298	1, 3, 4, 255, 258, 259, 297	climfsum 12554	. . . . 5 |- ( ph -> ( NN X. { 0 } ) ~~> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
299		suprleub 9928	. . . . . . . . . . . 12 |- ( ( ( ( `' 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 ) )
300	206, 58, 84, 60, 299	syl31anc 1187	. . . . . . . . . . 11 |- ( ph -> ( sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
301	80, 300	mpbird 224	. . . . . . . . . 10 |- ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N )
302	55, 301	syl5eqbr 4205	. . . . . . . . 9 |- ( ph -> M <_ N )
303		nn0uz 10476	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
304	88, 303	syl6eleq 2494	. . . . . . . . . 10 |- ( ph -> M e. ( ZZ>= ` 0 ) )
305	59	nn0zd 10329	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
306		elfz5 11007	. . . . . . . . . 10 |- ( ( M e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( M e. ( 0 ... N ) <-> M <_ N ) )
307	304, 305, 306	syl2anc 643	. . . . . . . . 9 |- ( ph -> ( M e. ( 0 ... N ) <-> M <_ N ) )
308	302, 307	mpbird 224	. . . . . . . 8 |- ( ph -> M e. ( 0 ... N ) )
309	308	snssd 3903	. . . . . . 7 |- ( ph -> { M } C_ ( 0 ... N ) )
310	20, 88	ffvelrnd 5830	. . . . . . . . 9 |- ( ph -> ( A ` M ) e. CC )
311		elsni 3798	. . . . . . . . . . 11 |- ( k e. { M } -> k = M )
312	311	fveq2d 5691	. . . . . . . . . 10 |- ( k e. { M } -> ( A ` k ) = ( A ` M ) )
313	312	eleq1d 2470	. . . . . . . . 9 |- ( k e. { M } -> ( ( A ` k ) e. CC <-> ( A ` M ) e. CC ) )
314	310, 313	syl5ibrcom 214	. . . . . . . 8 |- ( ph -> ( k e. { M } -> ( A ` k ) e. CC ) )
315	314	ralrimiv 2748	. . . . . . 7 |- ( ph -> A. k e. { M } ( A ` k ) e. CC )
316	4	olcd 383	. . . . . . 7 |- ( ph -> ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin ) )
317		sumss2 12475	. . . . . . 7 |- ( ( ( { 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 ) )
318	309, 315, 316, 317	syl21anc 1183	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
319		ltso 9112	. . . . . . . . 9 |- < Or RR
320	319	supex 7424	. . . . . . . 8 |- sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. _V
321	55, 320	eqeltri 2474	. . . . . . 7 |- M e. _V
322		fveq2 5687	. . . . . . . 8 |- ( k = M -> ( A ` k ) = ( A ` M ) )
323	322	sumsn 12489	. . . . . . 7 |- ( ( M e. _V /\ ( A ` M ) e. CC ) -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
324	321, 310, 323	sylancr 645	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
325	318, 324	eqtr3d 2438	. . . . 5 |- ( ph -> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` M ) )
326	298, 325	breqtrd 4196	. . . 4 |- ( ph -> ( NN X. { 0 } ) ~~> ( A ` M ) )
327	251, 29	climconst2 12297	. . . . 5 |- ( ( 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ~~> 0 )
328	8, 2, 327	mp2an 654	. . . 4 |- ( NN X. { 0 } ) ~~> 0
329		climuni 12301	. . . 4 |- ( ( ( NN X. { 0 } ) ~~> ( A ` M ) /\ ( NN X. { 0 } ) ~~> 0 ) -> ( A ` M ) = 0 )
330	326, 328, 329	sylancl 644	. . 3 |- ( ph -> ( A ` M ) = 0 )
331		fvex 5701	. . . 4 |- ( A ` M ) e. _V
332	331	elsnc 3797	. . 3 |- ( ( A ` M ) e. { 0 } <-> ( A ` M ) = 0 )
333	330, 332	sylibr 204	. 2 |- ( ph -> ( A ` M ) e. { 0 } )
334		elpreima 5809	. . . . . 6 |- ( A Fn NN0 -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
335	68, 334	syl 16	. . . . 5 |- ( ph -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
336	87, 335	mpbid 202	. . . 4 |- ( ph -> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) )
337	336	simprd 450	. . 3 |- ( ph -> ( A ` M ) e. ( S \ { 0 } ) )
338	337	eldifbd 3293	. 2 |- ( ph -> -. ( A ` M ) e. { 0 } )
339	333, 338	pm2.65i 167	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   \ cdif 3277   u. cun 3278   C_ wss 3280   (/)c0 3588   ifcif 3699   {csn 3774   class class class wbr 4172   e. cmpt 4226   X. cxp 4835   `'ccnv 4836   dom cdm 4837   "cima 4840   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   ^m cmap 6977   Fincfn 7068   supcsup 7403   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   -ucneg 9248   / cdiv 9633   NNcn 9956   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ...cfz 10999   ^cexp 11337   abscabs 11994   ~~> cli 12233   sum_csu 12434   0 pc0p 19514

This theorem is referenced by:  plyeq0  20083

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-0p 19515