Theorem plyeq0lem 21658

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

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 10888	. . . . . 6 |- NN = ( ZZ>= ` 1 )
2		1zzd 10669	. . . . . 6 |- ( ph -> 1 e. ZZ )
3		fzfid 11787	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
4		1zzd 10669	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 1 e. ZZ )
5		plyeq0.3	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> S C_ CC )
7		0cn 9370	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. CC
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 0 e. CC )
9	8	snssd 4013	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { 0 } C_ CC )
10	6, 9	unssd 3527	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( S u. { 0 } ) C_ CC )
11		cnex 9355	. . . . . . . . . . . . . . . . . . 19 |- CC e. _V
12		ssexg 4433	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
13	10, 11, 12	sylancl 662	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S u. { 0 } ) e. _V )
14		nn0ex 10577	. . . . . . . . . . . . . . . . . 18 |- NN0 e. _V
15		elmapg 7219	. . . . . . . . . . . . . . . . . 18 |- ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
16	13, 14, 15	sylancl 662	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
17	5, 16	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ph -> A : NN0 --> ( S u. { 0 } ) )
18		fss 5562	. . . . . . . . . . . . . . . 16 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ ( S u. { 0 } ) C_ CC ) -> A : NN0 --> CC )
19	17, 10, 18	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> A : NN0 --> CC )
20		elfznn0 11473	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... N ) -> k e. NN0 )
21		ffvelrn 5836	. . . . . . . . . . . . . . 15 |- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
22	19, 20, 21	syl2an 477	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
23	22	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( A ` k ) e. CC )
24	23	abscld 12914	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. RR )
25	24	recnd 9404	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. CC )
26		divcnv 13308	. . . . . . . . . . 11 |- ( ( abs ` ( A ` k ) ) e. CC -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
27	25, 26	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ~~> 0 )
28		nnex 10320	. . . . . . . . . . . 12 |- NN e. _V
29	28	mptex 5943	. . . . . . . . . . 11 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V
30	29	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) e. _V )
31		oveq2 6094	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) / n ) = ( ( abs ` ( A ` k ) ) / m ) )
32		eqid 2438	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) )
33		ovex 6111	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) / m ) e. _V
34	31, 32, 33	fvmpt 5769	. . . . . . . . . . . 12 |- ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
35	34	adantl 466	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
36		nndivre 10349	. . . . . . . . . . . 12 |- ( ( ( abs ` ( A ` k ) ) e. RR /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
37	24, 36	sylan 471	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
38	35, 37	eqeltrd 2512	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) e. RR )
39		oveq1 6093	. . . . . . . . . . . . . 14 |- ( n = m -> ( n ^ ( k - M ) ) = ( m ^ ( k - M ) ) )
40	39	oveq2d 6102	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
41		eqid 2438	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) )
42		ovex 6111	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. _V
43	40, 41, 42	fvmpt 5769	. . . . . . . . . . . 12 |- ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
44	43	adantl 466	. . . . . . . . . . 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 ) ) ) )
45	22	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( A ` k ) e. CC )
46	45	abscld 12914	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. RR )
47		nnrp 10992	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR+ )
48	47	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR+ )
49		elfzelz 11445	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... N ) -> k e. ZZ )
50		cnvimass 5184	. . . . . . . . . . . . . . . . . . 19 |- ( `' A " ( S \ { 0 } ) ) C_ dom A
51		fdm 5558	. . . . . . . . . . . . . . . . . . . 20 |- ( A : NN0 --> ( S u. { 0 } ) -> dom A = NN0 )
52	17, 51	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom A = NN0 )
53	50, 52	syl5sseq 3399	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ NN0 )
54		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 |- M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
55		nn0ssz 10659	. . . . . . . . . . . . . . . . . . . . 21 |- NN0 C_ ZZ
56	53, 55	syl6ss 3363	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ ZZ )
57		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
58		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> N e. NN0 )
59	58	nn0red 10629	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. RR )
60	53	sselda 3351	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z e. NN0 )
61		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
62		plyco0 21640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
63	58, 19, 62	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )
64	61, 63	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
65	64	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
66		ffn 5554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A : NN0 --> ( S u. { 0 } ) -> A Fn NN0 )
67	17, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A Fn NN0 )
68		elpreima 5818	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A Fn NN0 -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
69	67, 68	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( z e. ( `' A " ( S \ { 0 } ) ) <-> ( z e. NN0 /\ ( A ` z ) e. ( S \ { 0 } ) ) ) )
70	69	simplbda 624	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) e. ( S \ { 0 } ) )
71		eldifsni 3996	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A ` z ) e. ( S \ { 0 } ) -> ( A ` z ) =/= 0 )
72	70, 71	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) =/= 0 )
73		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = z -> ( A ` k ) = ( A ` z ) )
74	73	neeq1d 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = z -> ( ( A ` k ) =/= 0 <-> ( A ` z ) =/= 0 ) )
75		breq1 4290	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = z -> ( k <_ N <-> z <_ N ) )
76	74, 75	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = z -> ( ( ( A ` k ) =/= 0 -> k <_ N ) <-> ( ( A ` z ) =/= 0 -> z <_ N ) ) )
77	76	rspcv 3064	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. NN0 -> ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) -> ( ( A ` z ) =/= 0 -> z <_ N ) ) )
78	60, 65, 72, 77	syl3c 61	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z <_ N )
79	78	ralrimiva 2794	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N )
80		breq2 4291	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = N -> ( z <_ x <-> z <_ N ) )
81	80	ralbidv 2730	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = N -> ( A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
82	81	rspcev 3068	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( N e. RR /\ A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
83	59, 79, 82	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
84		suprzcl 10713	. . . . . . . . . . . . . . . . . . . 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 } ) ) )
85	56, 57, 83, 84	syl3anc 1218	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. ( `' A " ( S \ { 0 } ) ) )
86	54, 85	syl5eqel 2522	. . . . . . . . . . . . . . . . . 18 |- ( ph -> M e. ( `' A " ( S \ { 0 } ) ) )
87	53, 86	sseldd 3352	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. NN0 )
88	87	nn0zd 10737	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. ZZ )
89		zsubcl 10679	. . . . . . . . . . . . . . . 16 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k - M ) e. ZZ )
90	49, 88, 89	syl2anr 478	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
91	90	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. ZZ )
92	48, 91	rpexpcld 12023	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR+ )
93	92	rpred 11019	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR )
94	46, 93	remulcld 9406	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. RR )
95	44, 94	eqeltrd 2512	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. RR )
96		nnrecre 10350	. . . . . . . . . . . . 13 |- ( m e. NN -> ( 1 / m ) e. RR )
97	96	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( 1 / m ) e. RR )
98	23	absge0d 12922	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 0 <_ ( abs ` ( A ` k ) ) )
99	98	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( abs ` ( A ` k ) ) )
100		nnre 10321	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR )
101	100	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR )
102		nnge1 10340	. . . . . . . . . . . . . . 15 |- ( m e. NN -> 1 <_ m )
103	102	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ m )
104		1red 9393	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 e. RR )
105	91	zred 10739	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. RR )
106		simplr 754	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k < M )
107	49	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ZZ )
108	107	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. ZZ )
109	88	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. ZZ )
110		zltp1le 10686	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k < M <-> ( k + 1 ) <_ M ) )
111	108, 109, 110	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k < M <-> ( k + 1 ) <_ M ) )
112	106, 111	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k + 1 ) <_ M )
113	20	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
114	113	nn0red 10629	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. RR )
115	114	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. RR )
116	87	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. NN0 )
117	116	nn0red 10629	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. RR )
118	117	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. RR )
119	115, 104, 118	leaddsub2d 9933	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( k + 1 ) <_ M <-> 1 <_ ( M - k ) ) )
120	112, 119	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ ( M - k ) )
121	114	recnd 9404	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
122	121	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. CC )
123	117	recnd 9404	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. CC )
124	123	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. CC )
125	122, 124	negsubdi2d 9727	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u ( k - M ) = ( M - k ) )
126	120, 125	breqtrrd 4313	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ -u ( k - M ) )
127	104, 105, 126	lenegcon2d 9914	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) <_ -u 1 )
128		neg1z 10673	. . . . . . . . . . . . . . . 16 |- -u 1 e. ZZ
129		eluz 10866	. . . . . . . . . . . . . . . 16 |- ( ( ( k - M ) e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
130	91, 128, 129	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
131	127, 130	mpbird 232	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u 1 e. ( ZZ>= ` ( k - M ) ) )
132	101, 103, 131	leexp2ad 12032	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( m ^ -u 1 ) )
133		nncn 10322	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. CC )
134	133	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. CC )
135		expn1 11867	. . . . . . . . . . . . . 14 |- ( m e. CC -> ( m ^ -u 1 ) = ( 1 / m ) )
136	134, 135	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ -u 1 ) = ( 1 / m ) )
137	132, 136	breqtrd 4311	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( 1 / m ) )
138	93, 97, 46, 99, 137	lemul2ad 10265	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) <_ ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
139	25	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. CC )
140		nnne0 10346	. . . . . . . . . . . . . 14 |- ( m e. NN -> m =/= 0 )
141	140	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m =/= 0 )
142	139, 134, 141	divrecd 10102	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) = ( ( abs ` ( A ` k ) ) x. ( 1 / m ) ) )
143	35, 142	eqtrd 2470	. . . . . . . . . . 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 ) ) )
144	138, 44, 143	3brtr4d 4317	. . . . . . . . . 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 ) )
145	92	rpge0d 11023	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( m ^ ( k - M ) ) )
146	46, 93, 99, 145	mulge0d 9908	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
147	146, 44	breqtrrd 4313	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
148	1, 4, 27, 30, 38, 95, 144, 147	climsqz2 13111	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
149	28	mptex 5943	. . . . . . . . . . 11 |- ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V
150	149	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) e. _V )
151	39	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( n = m -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
152		eqid 2438	. . . . . . . . . . . . . . 15 |- ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) )
153		ovex 6111	. . . . . . . . . . . . . . 15 |- ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. _V
154	151, 152, 153	fvmpt 5769	. . . . . . . . . . . . . 14 |- ( m e. NN -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
155	154	ad2antlr 726	. . . . . . . . . . . . 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 ) ) ) )
156	19	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. NN ) -> A : NN0 --> CC )
157	156, 20, 21	syl2an 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
158	133	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m e. CC )
159	140	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m =/= 0 )
160	88	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. NN ) -> M e. ZZ )
161	49, 160, 89	syl2anr 478	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
162	158, 159, 161	expclzd 12005	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) e. CC )
163	157, 162	mulcld 9398	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. CC )
164	155, 163	eqeltrd 2512	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
165	164	an32s 802	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
166	165	adantlr 714	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
167	93	recnd 9404	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. CC )
168	45, 167	absmuld 12932	. . . . . . . . . . . 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 ) ) ) ) )
169	93, 145	absidd 12901	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( m ^ ( k - M ) ) ) = ( m ^ ( k - M ) ) )
170	169	oveq2d 6102	. . . . . . . . . . . 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 ) ) ) )
171	168, 170	eqtrd 2470	. . . . . . . . . . 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 ) ) ) )
172	154	adantl 466	. . . . . . . . . . . 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 ) ) ) )
173	172	fveq2d 5690	. . . . . . . . . . 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 ) ) ) ) )
174	171, 173, 44	3eqtr4rd 2481	. . . . . . . . . 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 ) ) )
175	1, 4, 150, 30, 166, 174	climabs0 13055	. . . . . . . . 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 ) )
176	148, 175	mpbird 232	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
177	114	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k e. RR )
178		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k < M )
179	177, 178	ltned 9502	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k =/= M )
180		elsn 3886	. . . . . . . . . . 11 |- ( k e. { M } <-> k = M )
181	180	necon3bbii 2634	. . . . . . . . . 10 |- ( -. k e. { M } <-> k =/= M )
182	179, 181	sylibr 212	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> -. k e. { M } )
183		iffalse 3794	. . . . . . . . 9 |- ( -. k e. { M } -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
184	182, 183	syl 16	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
185	176, 184	breqtrrd 4313	. . . . . . 7 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
186		nncn 10322	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n e. CC )
187	186	ad2antlr 726	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n e. CC )
188		nnne0 10346	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n =/= 0 )
189	188	ad2antlr 726	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n =/= 0 )
190	90	ad3antrrr 729	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( k - M ) e. ZZ )
191	187, 189, 190	expclzd 12005	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( n ^ ( k - M ) ) e. CC )
192	191	mul02d 9559	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( 0 x. ( n ^ ( k - M ) ) ) = 0 )
193		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( A ` k ) = 0 )
194	193	oveq1d 6101	. . . . . . . . . . . 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 ) ) ) )
195	193	ifeq1d 3802	. . . . . . . . . . . . 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 ) )
196		ifid 3821	. . . . . . . . . . . . 13 |- if ( k e. { M } , 0 , 0 ) = 0
197	195, 196	syl6eq 2486	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> if ( k e. { M } , ( A ` k ) , 0 ) = 0 )
198	192, 194, 197	3eqtr4d 2480	. . . . . . . . . . 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 ) )
199	22	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( A ` k ) e. CC )
200	199	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. CC )
201	200	mulid1d 9395	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. 1 ) = ( A ` k ) )
202		nn0ssre 10575	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 C_ RR
203	53, 202	syl6ss 3363	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ RR )
204	203	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) C_ RR )
205	57	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
206	83	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
207	20	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. NN0 )
208		ffvelrn 5836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( A ` k ) e. ( S u. { 0 } ) )
209	17, 20, 208	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. ( S u. { 0 } ) )
210	209	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
211		eldifsn 3995	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) <-> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
212	210, 211	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( ( S u. { 0 } ) \ { 0 } ) )
213		difun2 3753	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S u. { 0 } ) \ { 0 } ) = ( S \ { 0 } )
214	212, 213	syl6eleq 2528	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( S \ { 0 } ) )
215		elpreima 5818	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A Fn NN0 -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
216	67, 215	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
217	216	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( k e. ( `' A " ( S \ { 0 } ) ) <-> ( k e. NN0 /\ ( A ` k ) e. ( S \ { 0 } ) ) ) )
218	207, 214, 217	mpbir2and 913	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. ( `' A " ( S \ { 0 } ) ) )
219		suprub 10283	. . . . . . . . . . . . . . . . . . . . . 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 , < ) )
220	204, 205, 206, 218, 219	syl31anc 1221	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) )
221	220, 54	syl6breqr 4327	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
222	221	adantlr 714	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
223	222	adantlr 714	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
224		simpllr 758	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M <_ k )
225	114	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. RR )
226	117	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. RR )
227	225, 226	letri3d 9508	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k = M <-> ( k <_ M /\ M <_ k ) ) )
228	223, 224, 227	mpbir2and 913	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k = M )
229	228	oveq1d 6101	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = ( M - M ) )
230	123	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. CC )
231	230	subidd 9699	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( M - M ) = 0 )
232	229, 231	eqtrd 2470	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = 0 )
233	232	oveq2d 6102	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = ( n ^ 0 ) )
234	186	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> n e. CC )
235	234	exp0d 11994	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ 0 ) = 1 )
236	233, 235	eqtrd 2470	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = 1 )
237	236	oveq2d 6102	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. 1 ) )
238	228, 180	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. { M } )
239		iftrue 3792	. . . . . . . . . . . . 13 |- ( k e. { M } -> if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` k ) )
240	238, 239	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 ) )
241	201, 237, 240	3eqtr4d 2480	. . . . . . . . . . 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 ) )
242	198, 241	pm2.61dane 2684	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = if ( k e. { M } , ( A ` k ) , 0 ) )
243	242	mpteq2dva 4373	. . . . . . . . 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 ) ) )
244		fconstmpt 4877	. . . . . . . . 9 |- ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) = ( n e. NN |-> if ( k e. { M } , ( A ` k ) , 0 ) )
245	243, 244	syl6eqr 2488	. . . . . . . 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 ) } ) )
246		ifcl 3826	. . . . . . . . . 10 |- ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
247	199, 7, 246	sylancl 662	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
248		1z 10668	. . . . . . . . 9 |- 1 e. ZZ
249	1	eqimss2i 3406	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
250	249, 28	climconst2 13018	. . . . . . . . 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 ) )
251	247, 248, 250	sylancl 662	. . . . . . . 8 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
252	245, 251	eqbrtrd 4307	. . . . . . 7 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
253	185, 252, 114, 117	ltlecasei 9474	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
254		snex 4528	. . . . . . . 8 |- { 0 } e. _V
255	28, 254	xpex 6503	. . . . . . 7 |- ( NN X. { 0 } ) e. _V
256	255	a1i 11	. . . . . 6 |- ( ph -> ( NN X. { 0 } ) e. _V )
257	165	anasss 647	. . . . . 6 |- ( ( ph /\ ( k e. ( 0 ... N ) /\ m e. NN ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
258		plyeq0.5	. . . . . . . . . . . 12 |- ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
259	258	fveq1d 5688	. . . . . . . . . . 11 |- ( ph -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
260	259	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
261	133	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN ) -> m e. CC )
262		0pval 21129	. . . . . . . . . . 11 |- ( m e. CC -> ( 0p ` m ) = 0 )
263	261, 262	syl 16	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0p ` m ) = 0 )
264		oveq1 6093	. . . . . . . . . . . . . 14 |- ( z = m -> ( z ^ k ) = ( m ^ k ) )
265	264	oveq2d 6102	. . . . . . . . . . . . 13 |- ( z = m -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( m ^ k ) ) )
266	265	sumeq2sdv 13173	. . . . . . . . . . . 12 |- ( z = m -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
267		eqid 2438	. . . . . . . . . . . 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 ) ) )
268		sumex 13157	. . . . . . . . . . . 12 |- sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) e. _V
269	266, 267, 268	fvmpt 5769	. . . . . . . . . . 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 ) ) )
270	261, 269	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 ) ) )
271	260, 263, 270	3eqtr3d 2478	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
272	271	oveq1d 6101	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = ( sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
273		expcl 11875	. . . . . . . . . 10 |- ( ( m e. CC /\ M e. NN0 ) -> ( m ^ M ) e. CC )
274	133, 87, 273	syl2anr 478	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) e. CC )
275	140	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> m =/= 0 )
276	261, 275, 160	expne0d 12006	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) =/= 0 )
277	274, 276	div0d 10098	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = 0 )
278		fzfid 11787	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( 0 ... N ) e. Fin )
279		expcl 11875	. . . . . . . . . . 11 |- ( ( m e. CC /\ k e. NN0 ) -> ( m ^ k ) e. CC )
280	261, 20, 279	syl2an 477	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ k ) e. CC )
281	157, 280	mulcld 9398	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ k ) ) e. CC )
282	278, 274, 281, 276	fsumdivc 13245	. . . . . . . 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 ) ) )
283	272, 277, 282	3eqtr3d 2478	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
284		fvconst2g 5926	. . . . . . . 8 |- ( ( 0 e. CC /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
285	8, 284	sylan 471	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
286	160	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> M e. ZZ )
287	49	adantl 466	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> k e. ZZ )
288	158, 159, 286, 287	expsubd 12011	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) = ( ( m ^ k ) / ( m ^ M ) ) )
289	288	oveq2d 6102	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
290	274	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) e. CC )
291	276	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) =/= 0 )
292	157, 280, 290, 291	divassd 10134	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) = ( ( A ` k ) x. ( ( m ^ k ) / ( m ^ M ) ) ) )
293	289, 155, 292	3eqtr4d 2480	. . . . . . . 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 ) ) )
294	293	sumeq2dv 13172	. . . . . . 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 ) ) )
295	283, 285, 294	3eqtr4d 2480	. . . . . 6 |- ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = sum_ k e. ( 0 ... N ) ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) )
296	1, 2, 3, 253, 256, 257, 295	climfsum 13275	. . . . 5 |- ( ph -> ( NN X. { 0 } ) ~~> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
297		suprleub 10286	. . . . . . . . . . . 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 ) )
298	203, 57, 83, 59, 297	syl31anc 1221	. . . . . . . . . . 11 |- ( ph -> ( sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
299	79, 298	mpbird 232	. . . . . . . . . 10 |- ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) <_ N )
300	54, 299	syl5eqbr 4320	. . . . . . . . 9 |- ( ph -> M <_ N )
301		nn0uz 10887	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
302	87, 301	syl6eleq 2528	. . . . . . . . . 10 |- ( ph -> M e. ( ZZ>= ` 0 ) )
303	58	nn0zd 10737	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
304		elfz5 11437	. . . . . . . . . 10 |- ( ( M e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( M e. ( 0 ... N ) <-> M <_ N ) )
305	302, 303, 304	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( M e. ( 0 ... N ) <-> M <_ N ) )
306	300, 305	mpbird 232	. . . . . . . 8 |- ( ph -> M e. ( 0 ... N ) )
307	306	snssd 4013	. . . . . . 7 |- ( ph -> { M } C_ ( 0 ... N ) )
308	19, 87	ffvelrnd 5839	. . . . . . . . 9 |- ( ph -> ( A ` M ) e. CC )
309		elsni 3897	. . . . . . . . . . 11 |- ( k e. { M } -> k = M )
310	309	fveq2d 5690	. . . . . . . . . 10 |- ( k e. { M } -> ( A ` k ) = ( A ` M ) )
311	310	eleq1d 2504	. . . . . . . . 9 |- ( k e. { M } -> ( ( A ` k ) e. CC <-> ( A ` M ) e. CC ) )
312	308, 311	syl5ibrcom 222	. . . . . . . 8 |- ( ph -> ( k e. { M } -> ( A ` k ) e. CC ) )
313	312	ralrimiv 2793	. . . . . . 7 |- ( ph -> A. k e. { M } ( A ` k ) e. CC )
314	3	olcd 393	. . . . . . 7 |- ( ph -> ( ( 0 ... N ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... N ) e. Fin ) )
315		sumss2 13195	. . . . . . 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 ) )
316	307, 313, 314, 315	syl21anc 1217	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
317		ltso 9447	. . . . . . . . 9 |- < Or RR
318	317	supex 7705	. . . . . . . 8 |- sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. _V
319	54, 318	eqeltri 2508	. . . . . . 7 |- M e. _V
320		fveq2 5686	. . . . . . . 8 |- ( k = M -> ( A ` k ) = ( A ` M ) )
321	320	sumsn 13209	. . . . . . 7 |- ( ( M e. _V /\ ( A ` M ) e. CC ) -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
322	319, 308, 321	sylancr 663	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
323	316, 322	eqtr3d 2472	. . . . 5 |- ( ph -> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` M ) )
324	296, 323	breqtrd 4311	. . . 4 |- ( ph -> ( NN X. { 0 } ) ~~> ( A ` M ) )
325	249, 28	climconst2 13018	. . . . 5 |- ( ( 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ~~> 0 )
326	7, 248, 325	mp2an 672	. . . 4 |- ( NN X. { 0 } ) ~~> 0
327		climuni 13022	. . . 4 |- ( ( ( NN X. { 0 } ) ~~> ( A ` M ) /\ ( NN X. { 0 } ) ~~> 0 ) -> ( A ` M ) = 0 )
328	324, 326, 327	sylancl 662	. . 3 |- ( ph -> ( A ` M ) = 0 )
329		fvex 5696	. . . 4 |- ( A ` M ) e. _V
330	329	elsnc 3896	. . 3 |- ( ( A ` M ) e. { 0 } <-> ( A ` M ) = 0 )
331	328, 330	sylibr 212	. 2 |- ( ph -> ( A ` M ) e. { 0 } )
332		elpreima 5818	. . . . . 6 |- ( A Fn NN0 -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
333	67, 332	syl 16	. . . . 5 |- ( ph -> ( M e. ( `' A " ( S \ { 0 } ) ) <-> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) ) )
334	86, 333	mpbid 210	. . . 4 |- ( ph -> ( M e. NN0 /\ ( A ` M ) e. ( S \ { 0 } ) ) )
335	334	simprd 463	. . 3 |- ( ph -> ( A ` M ) e. ( S \ { 0 } ) )
336	335	eldifbd 3336	. 2 |- ( ph -> -. ( A ` M ) e. { 0 } )
337	331, 336	pm2.65i 173	1 |- -. ph

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2601   A.wral 2710   E.wrex 2711   _Vcvv 2967   \ cdif 3320   u. cun 3321   C_ wss 3323   (/)c0 3632   ifcif 3786   {csn 3872   class class class wbr 4287   e. cmpt 4345   X. cxp 4833   `'ccnv 4834   dom cdm 4835   "cima 4838   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6086   ^m cmap 7206   Fincfn 7302   supcsup 7682   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275   + caddc 9277   x. cmul 9279   < clt 9410   <_ cle 9411   - cmin 9587   -ucneg 9588   / cdiv 9985   NNcn 10314   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   RR+crp 10983   ...cfz 11429   ^cexp 11857   abscabs 12715   ~~> cli 12954   sum_csu 13155   0pc0p 21127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  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-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-pm 7209  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-sup 7683  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-rp 10984  df-fz 11430  df-fzo 11541  df-fl 11634  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-clim 12958  df-rlim 12959  df-sum 13156  df-0p 21128

This theorem is referenced by:  plyeq0  21659