Theorem plyeq0lem 21563

Description: Lemma for plyeq0 21564. 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 10884	. . . . . 6 |- NN = ( ZZ>= ` 1 )
2		1zzd 10665	. . . . . 6 |- ( ph -> 1 e. ZZ )
3		fzfid 11779	. . . . . 6 |- ( ph -> ( 0 ... N ) e. Fin )
4		1zzd 10665	. . . . . . . . . 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 9366	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. CC
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 0 e. CC )
9	8	snssd 4006	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { 0 } C_ CC )
10	6, 9	unssd 3520	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( S u. { 0 } ) C_ CC )
11		cnex 9351	. . . . . . . . . . . . . . . . . . 19 |- CC e. _V
12		ssexg 4426	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
13	10, 11, 12	sylancl 655	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S u. { 0 } ) e. _V )
14		nn0ex 10573	. . . . . . . . . . . . . . . . . 18 |- NN0 e. _V
15		elmapg 7215	. . . . . . . . . . . . . . . . . 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 655	. . . . . . . . . . . . . . . . 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 5555	. . . . . . . . . . . . . . . 16 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ ( S u. { 0 } ) C_ CC ) -> A : NN0 --> CC )
19	17, 10, 18	syl2anc 654	. . . . . . . . . . . . . . 15 |- ( ph -> A : NN0 --> CC )
20		elfznn0 11468	. . . . . . . . . . . . . . 15 |- ( k e. ( 0 ... N ) -> k e. NN0 )
21		ffvelrn 5829	. . . . . . . . . . . . . . 15 |- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
22	19, 20, 21	syl2an 474	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
23	22	adantr 462	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( A ` k ) e. CC )
24	23	abscld 12906	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. RR )
25	24	recnd 9400	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( abs ` ( A ` k ) ) e. CC )
26		divcnv 13299	. . . . . . . . . . 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 10316	. . . . . . . . . . . 12 |- NN e. _V
29	28	mptex 5935	. . . . . . . . . . 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 6088	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) / n ) = ( ( abs ` ( A ` k ) ) / m ) )
32		eqid 2433	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) )
33		ovex 6105	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) / m ) e. _V
34	31, 32, 33	fvmpt 5762	. . . . . . . . . . . 12 |- ( m e. NN -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) = ( ( abs ` ( A ` k ) ) / m ) )
35	34	adantl 463	. . . . . . . . . . 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 10345	. . . . . . . . . . . 12 |- ( ( ( abs ` ( A ` k ) ) e. RR /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
37	24, 36	sylan 468	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) / m ) e. RR )
38	35, 37	eqeltrd 2507	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( abs ` ( A ` k ) ) / n ) ) ` m ) e. RR )
39		oveq1 6087	. . . . . . . . . . . . . 14 |- ( n = m -> ( n ^ ( k - M ) ) = ( m ^ ( k - M ) ) )
40	39	oveq2d 6096	. . . . . . . . . . . . 13 |- ( n = m -> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) = ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
41		eqid 2433	. . . . . . . . . . . . 13 |- ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) )
42		ovex 6105	. . . . . . . . . . . . 13 |- ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. _V
43	40, 41, 42	fvmpt 5762	. . . . . . . . . . . 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 463	. . . . . . . . . . 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 718	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( A ` k ) e. CC )
46	45	abscld 12906	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. RR )
47		nnrp 10988	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR+ )
48	47	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR+ )
49		elfzelz 11440	. . . . . . . . . . . . . . . 16 |- ( k e. ( 0 ... N ) -> k e. ZZ )
50		cnvimass 5177	. . . . . . . . . . . . . . . . . . 19 |- ( `' A " ( S \ { 0 } ) ) C_ dom A
51		fdm 5551	. . . . . . . . . . . . . . . . . . . 20 |- ( A : NN0 --> ( S u. { 0 } ) -> dom A = NN0 )
52	17, 51	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> dom A = NN0 )
53	50, 52	syl5sseq 3392	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ NN0 )
54		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 |- M = sup ( ( `' A " ( S \ { 0 } ) ) , RR , < )
55		nn0ssz 10655	. . . . . . . . . . . . . . . . . . . . 21 |- NN0 C_ ZZ
56	53, 55	syl6ss 3356	. . . . . . . . . . . . . . . . . . . 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 10625	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> N e. RR )
60	53	sselda 3344	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> z e. NN0 )
61		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
62		plyco0 21545	. . . . . . . . . . . . . . . . . . . . . . . . . 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 654	. . . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
66		ffn 5547	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A : NN0 --> ( S u. { 0 } ) -> A Fn NN0 )
67	17, 66	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A Fn NN0 )
68		elpreima 5811	. . . . . . . . . . . . . . . . . . . . . . . . . 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 619	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( `' A " ( S \ { 0 } ) ) ) -> ( A ` z ) e. ( S \ { 0 } ) )
71		eldifsni 3989	. . . . . . . . . . . . . . . . . . . . . . . 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 5679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = z -> ( A ` k ) = ( A ` z ) )
74	73	neeq1d 2611	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = z -> ( ( A ` k ) =/= 0 <-> ( A ` z ) =/= 0 ) )
75		breq1 4283	. . . . . . . . . . . . . . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . . . . . . . . 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 2789	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N )
80		breq2 4284	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = N -> ( z <_ x <-> z <_ N ) )
81	80	ralbidv 2725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = N -> ( A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x <-> A. z e. ( `' A " ( S \ { 0 } ) ) z <_ N ) )
82	81	rspcev 3062	. . . . . . . . . . . . . . . . . . . . 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 654	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
84		suprzcl 10709	. . . . . . . . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. ( `' A " ( S \ { 0 } ) ) )
86	54, 85	syl5eqel 2517	. . . . . . . . . . . . . . . . . 18 |- ( ph -> M e. ( `' A " ( S \ { 0 } ) ) )
87	53, 86	sseldd 3345	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. NN0 )
88	87	nn0zd 10733	. . . . . . . . . . . . . . . 16 |- ( ph -> M e. ZZ )
89		zsubcl 10675	. . . . . . . . . . . . . . . 16 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k - M ) e. ZZ )
90	49, 88, 89	syl2anr 475	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
91	90	ad2antrr 718	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. ZZ )
92	48, 91	rpexpcld 12015	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR+ )
93	92	rpred 11015	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. RR )
94	46, 93	remulcld 9402	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) e. RR )
95	44, 94	eqeltrd 2507	. . . . . . . . . 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 10346	. . . . . . . . . . . . 13 |- ( m e. NN -> ( 1 / m ) e. RR )
97	96	adantl 463	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( 1 / m ) e. RR )
98	23	absge0d 12914	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> 0 <_ ( abs ` ( A ` k ) ) )
99	98	adantr 462	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( abs ` ( A ` k ) ) )
100		nnre 10317	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. RR )
101	100	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. RR )
102		nnge1 10336	. . . . . . . . . . . . . . 15 |- ( m e. NN -> 1 <_ m )
103	102	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ m )
104		1red 9389	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 e. RR )
105	91	zred 10735	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) e. RR )
106		simplr 747	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k < M )
107	49	adantl 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ZZ )
108	107	ad2antrr 718	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. ZZ )
109	88	ad3antrrr 722	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. ZZ )
110		zltp1le 10682	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k < M <-> ( k + 1 ) <_ M ) )
111	108, 109, 110	syl2anc 654	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
114	113	nn0red 10625	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. RR )
115	114	ad2antrr 718	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. RR )
116	87	adantr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. NN0 )
117	116	nn0red 10625	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. RR )
118	117	ad2antrr 718	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. RR )
119	115, 104, 118	leaddsub2d 9929	. . . . . . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
122	121	ad2antrr 718	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> k e. CC )
123	117	recnd 9400	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> M e. CC )
124	123	ad2antrr 718	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> M e. CC )
125	122, 124	negsubdi2d 9723	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> -u ( k - M ) = ( M - k ) )
126	120, 125	breqtrrd 4306	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 1 <_ -u ( k - M ) )
127	104, 105, 126	lenegcon2d 9910	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( k - M ) <_ -u 1 )
128		neg1z 10669	. . . . . . . . . . . . . . . 16 |- -u 1 e. ZZ
129		eluz 10862	. . . . . . . . . . . . . . . 16 |- ( ( ( k - M ) e. ZZ /\ -u 1 e. ZZ ) -> ( -u 1 e. ( ZZ>= ` ( k - M ) ) <-> ( k - M ) <_ -u 1 ) )
130	91, 128, 129	sylancl 655	. . . . . . . . . . . . . . 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 12024	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( m ^ -u 1 ) )
133		nncn 10318	. . . . . . . . . . . . . . 15 |- ( m e. NN -> m e. CC )
134	133	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m e. CC )
135		expn1 11859	. . . . . . . . . . . . . 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 4304	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) <_ ( 1 / m ) )
138	93, 97, 46, 99, 137	lemul2ad 10261	. . . . . . . . . . 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 462	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( A ` k ) ) e. CC )
140		nnne0 10342	. . . . . . . . . . . . . 14 |- ( m e. NN -> m =/= 0 )
141	140	adantl 463	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> m =/= 0 )
142	139, 134, 141	divrecd 10098	. . . . . . . . . . . 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 2465	. . . . . . . . . . 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 4310	. . . . . . . . . 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 11019	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( m ^ ( k - M ) ) )
146	46, 93, 99, 145	mulge0d 9904	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> 0 <_ ( ( abs ` ( A ` k ) ) x. ( m ^ ( k - M ) ) ) )
147	146, 44	breqtrrd 4306	. . . . . . . . . 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 13103	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> ( n e. NN |-> ( ( abs ` ( A ` k ) ) x. ( n ^ ( k - M ) ) ) ) ~~> 0 )
149	28	mptex 5935	. . . . . . . . . . 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 6096	. . . . . . . . . . . . . . 15 |- ( n = m -> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
152		eqid 2433	. . . . . . . . . . . . . . 15 |- ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) = ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) )
153		ovex 6105	. . . . . . . . . . . . . . 15 |- ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. _V
154	151, 152, 153	fvmpt 5762	. . . . . . . . . . . . . 14 |- ( m e. NN -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) = ( ( A ` k ) x. ( m ^ ( k - M ) ) ) )
155	154	ad2antlr 719	. . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. NN ) -> A : NN0 --> CC )
157	156, 20, 21	syl2an 474	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
158	133	ad2antlr 719	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m e. CC )
159	140	ad2antlr 719	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> m =/= 0 )
160	88	adantr 462	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. NN ) -> M e. ZZ )
161	49, 160, 89	syl2anr 475	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( k - M ) e. ZZ )
162	158, 159, 161	expclzd 11997	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) e. CC )
163	157, 162	mulcld 9394	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ ( k - M ) ) ) e. CC )
164	155, 163	eqeltrd 2507	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
165	164	an32s 795	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ` m ) e. CC )
166	165	adantlr 707	. . . . . . . . . 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 9400	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( m ^ ( k - M ) ) e. CC )
168	45, 167	absmuld 12924	. . . . . . . . . . . 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 12893	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) /\ m e. NN ) -> ( abs ` ( m ^ ( k - M ) ) ) = ( m ^ ( k - M ) ) )
170	169	oveq2d 6096	. . . . . . . . . . . 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 2465	. . . . . . . . . . 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 463	. . . . . . . . . . . 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 5683	. . . . . . . . . . 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 2476	. . . . . . . . . 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 13047	. . . . . . . . 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 462	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k e. RR )
178		simpr 458	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k < M )
179	177, 178	ltned 9498	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> k =/= M )
180		elsn 3879	. . . . . . . . . . 11 |- ( k e. { M } <-> k = M )
181	180	necon3bbii 2629	. . . . . . . . . 10 |- ( -. k e. { M } <-> k =/= M )
182	179, 181	sylibr 212	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ k < M ) -> -. k e. { M } )
183		iffalse 3787	. . . . . . . . 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 4306	. . . . . . 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 10318	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n e. CC )
187	186	ad2antlr 719	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n e. CC )
188		nnne0 10342	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n =/= 0 )
189	188	ad2antlr 719	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> n =/= 0 )
190	90	ad3antrrr 722	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( k - M ) e. ZZ )
191	187, 189, 190	expclzd 11997	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( n ^ ( k - M ) ) e. CC )
192	191	mul02d 9555	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( 0 x. ( n ^ ( k - M ) ) ) = 0 )
193		simpr 458	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) = 0 ) -> ( A ` k ) = 0 )
194	193	oveq1d 6095	. . . . . . . . . . . 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 3795	. . . . . . . . . . . . 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 3814	. . . . . . . . . . . . 13 |- if ( k e. { M } , 0 , 0 ) = 0
197	195, 196	syl6eq 2481	. . . . . . . . . . . 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 2475	. . . . . . . . . . 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 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> ( A ` k ) e. CC )
200	199	ad2antrr 718	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. CC )
201	200	mulid1d 9391	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) x. 1 ) = ( A ` k ) )
202		nn0ssre 10571	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 C_ RR
203	53, 202	syl6ss 3356	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( `' A " ( S \ { 0 } ) ) C_ RR )
204	203	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) C_ RR )
205	57	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( `' A " ( S \ { 0 } ) ) =/= (/) )
206	83	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> E. x e. RR A. z e. ( `' A " ( S \ { 0 } ) ) z <_ x )
207	20	ad2antlr 719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. NN0 )
208		ffvelrn 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( A ` k ) e. ( S u. { 0 } ) )
209	17, 20, 208	syl2an 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. ( S u. { 0 } ) )
210	209	anim1i 563	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( A ` k ) =/= 0 ) )
211		eldifsn 3988	. . . . . . . . . . . . . . . . . . . . . . . . 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 3746	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S u. { 0 } ) \ { 0 } ) = ( S \ { 0 } )
214	212, 213	syl6eleq 2523	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> ( A ` k ) e. ( S \ { 0 } ) )
215		elpreima 5811	. . . . . . . . . . . . . . . . . . . . . . . . 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 718	. . . . . . . . . . . . . . . . . . . . . . 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 906	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k e. ( `' A " ( S \ { 0 } ) ) )
219		suprub 10279	. . . . . . . . . . . . . . . . . . . . . 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 1214	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) )
221	220, 54	syl6breqr 4320	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
222	221	adantlr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
223	222	adantlr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k <_ M )
224		simpllr 751	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M <_ k )
225	114	ad3antrrr 722	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k e. RR )
226	117	ad3antrrr 722	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. RR )
227	225, 226	letri3d 9504	. . . . . . . . . . . . . . . . . 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 906	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> k = M )
229	228	oveq1d 6095	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = ( M - M ) )
230	123	ad3antrrr 722	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> M e. CC )
231	230	subidd 9695	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( M - M ) = 0 )
232	229, 231	eqtrd 2465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( k - M ) = 0 )
233	232	oveq2d 6096	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = ( n ^ 0 ) )
234	186	ad2antlr 719	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> n e. CC )
235	234	exp0d 11986	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ 0 ) = 1 )
236	233, 235	eqtrd 2465	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) /\ n e. NN ) /\ ( A ` k ) =/= 0 ) -> ( n ^ ( k - M ) ) = 1 )
237	236	oveq2d 6096	. . . . . . . . . . . 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 3785	. . . . . . . . . . . . 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 2475	. . . . . . . . . . 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 2679	. . . . . . . . . 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 4366	. . . . . . . . 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 4869	. . . . . . . . 9 |- ( NN X. { if ( k e. { M } , ( A ` k ) , 0 ) } ) = ( n e. NN |-> if ( k e. { M } , ( A ` k ) , 0 ) )
245	243, 244	syl6eqr 2483	. . . . . . . 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 3819	. . . . . . . . . 10 |- ( ( ( A ` k ) e. CC /\ 0 e. CC ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
247	199, 7, 246	sylancl 655	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 0 ... N ) ) /\ M <_ k ) -> if ( k e. { M } , ( A ` k ) , 0 ) e. CC )
248		1z 10664	. . . . . . . . 9 |- 1 e. ZZ
249	1	eqimss2i 3399	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
250	249, 28	climconst2 13010	. . . . . . . . 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 655	. . . . . . . 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 4300	. . . . . . 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 9470	. . . . . 6 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( n e. NN |-> ( ( A ` k ) x. ( n ^ ( k - M ) ) ) ) ~~> if ( k e. { M } , ( A ` k ) , 0 ) )
254		snex 4521	. . . . . . . 8 |- { 0 } e. _V
255	28, 254	xpex 6497	. . . . . . 7 |- ( NN X. { 0 } ) e. _V
256	255	a1i 11	. . . . . 6 |- ( ph -> ( NN X. { 0 } ) e. _V )
257	165	anasss 640	. . . . . 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 5681	. . . . . . . . . . 11 |- ( ph -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
260	259	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0p ` m ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ` m ) )
261	133	adantl 463	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN ) -> m e. CC )
262		0pval 20991	. . . . . . . . . . 11 |- ( m e. CC -> ( 0p ` m ) = 0 )
263	261, 262	syl 16	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> ( 0p ` m ) = 0 )
264		oveq1 6087	. . . . . . . . . . . . . 14 |- ( z = m -> ( z ^ k ) = ( m ^ k ) )
265	264	oveq2d 6096	. . . . . . . . . . . . 13 |- ( z = m -> ( ( A ` k ) x. ( z ^ k ) ) = ( ( A ` k ) x. ( m ^ k ) ) )
266	265	sumeq2sdv 13165	. . . . . . . . . . . 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 2433	. . . . . . . . . . . 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 13149	. . . . . . . . . . . 12 |- sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) e. _V
269	266, 267, 268	fvmpt 5762	. . . . . . . . . . 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 2473	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) )
272	271	oveq1d 6095	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = ( sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
273		expcl 11867	. . . . . . . . . 10 |- ( ( m e. CC /\ M e. NN0 ) -> ( m ^ M ) e. CC )
274	133, 87, 273	syl2anr 475	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) e. CC )
275	140	adantl 463	. . . . . . . . . 10 |- ( ( ph /\ m e. NN ) -> m =/= 0 )
276	261, 275, 160	expne0d 11998	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( m ^ M ) =/= 0 )
277	274, 276	div0d 10094	. . . . . . . 8 |- ( ( ph /\ m e. NN ) -> ( 0 / ( m ^ M ) ) = 0 )
278		fzfid 11779	. . . . . . . . 9 |- ( ( ph /\ m e. NN ) -> ( 0 ... N ) e. Fin )
279		expcl 11867	. . . . . . . . . . 11 |- ( ( m e. CC /\ k e. NN0 ) -> ( m ^ k ) e. CC )
280	261, 20, 279	syl2an 474	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ k ) e. CC )
281	157, 280	mulcld 9394	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( m ^ k ) ) e. CC )
282	278, 274, 281, 276	fsumdivc 13236	. . . . . . . 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 2473	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> 0 = sum_ k e. ( 0 ... N ) ( ( ( A ` k ) x. ( m ^ k ) ) / ( m ^ M ) ) )
284		fvconst2g 5918	. . . . . . . 8 |- ( ( 0 e. CC /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
285	8, 284	sylan 468	. . . . . . 7 |- ( ( ph /\ m e. NN ) -> ( ( NN X. { 0 } ) ` m ) = 0 )
286	160	adantr 462	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> M e. ZZ )
287	49	adantl 463	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> k e. ZZ )
288	158, 159, 286, 287	expsubd 12003	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ ( k - M ) ) = ( ( m ^ k ) / ( m ^ M ) ) )
289	288	oveq2d 6096	. . . . . . . . 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 462	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) e. CC )
291	276	adantr 462	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN ) /\ k e. ( 0 ... N ) ) -> ( m ^ M ) =/= 0 )
292	157, 280, 290, 291	divassd 10130	. . . . . . . . 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 2475	. . . . . . . 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 13164	. . . . . . 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 2475	. . . . . 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 13266	. . . . 5 |- ( ph -> ( NN X. { 0 } ) ~~> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
297		suprleub 10282	. . . . . . . . . . . 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 1214	. . . . . . . . . . 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 4313	. . . . . . . . 9 |- ( ph -> M <_ N )
301		nn0uz 10883	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
302	87, 301	syl6eleq 2523	. . . . . . . . . 10 |- ( ph -> M e. ( ZZ>= ` 0 ) )
303	58	nn0zd 10733	. . . . . . . . . 10 |- ( ph -> N e. ZZ )
304		elfz5 11432	. . . . . . . . . 10 |- ( ( M e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( M e. ( 0 ... N ) <-> M <_ N ) )
305	302, 303, 304	syl2anc 654	. . . . . . . . 9 |- ( ph -> ( M e. ( 0 ... N ) <-> M <_ N ) )
306	300, 305	mpbird 232	. . . . . . . 8 |- ( ph -> M e. ( 0 ... N ) )
307	306	snssd 4006	. . . . . . 7 |- ( ph -> { M } C_ ( 0 ... N ) )
308	19, 87	ffvelrnd 5832	. . . . . . . . 9 |- ( ph -> ( A ` M ) e. CC )
309		elsni 3890	. . . . . . . . . . 11 |- ( k e. { M } -> k = M )
310	309	fveq2d 5683	. . . . . . . . . 10 |- ( k e. { M } -> ( A ` k ) = ( A ` M ) )
311	310	eleq1d 2499	. . . . . . . . 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 2788	. . . . . . 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 13187	. . . . . . 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 1210	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) )
317		ltso 9443	. . . . . . . . 9 |- < Or RR
318	317	supex 7701	. . . . . . . 8 |- sup ( ( `' A " ( S \ { 0 } ) ) , RR , < ) e. _V
319	54, 318	eqeltri 2503	. . . . . . 7 |- M e. _V
320		fveq2 5679	. . . . . . . 8 |- ( k = M -> ( A ` k ) = ( A ` M ) )
321	320	sumsn 13201	. . . . . . 7 |- ( ( M e. _V /\ ( A ` M ) e. CC ) -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
322	319, 308, 321	sylancr 656	. . . . . 6 |- ( ph -> sum_ k e. { M } ( A ` k ) = ( A ` M ) )
323	316, 322	eqtr3d 2467	. . . . 5 |- ( ph -> sum_ k e. ( 0 ... N ) if ( k e. { M } , ( A ` k ) , 0 ) = ( A ` M ) )
324	296, 323	breqtrd 4304	. . . 4 |- ( ph -> ( NN X. { 0 } ) ~~> ( A ` M ) )
325	249, 28	climconst2 13010	. . . . 5 |- ( ( 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ~~> 0 )
326	7, 248, 325	mp2an 665	. . . 4 |- ( NN X. { 0 } ) ~~> 0
327		climuni 13014	. . . 4 |- ( ( ( NN X. { 0 } ) ~~> ( A ` M ) /\ ( NN X. { 0 } ) ~~> 0 ) -> ( A ` M ) = 0 )
328	324, 326, 327	sylancl 655	. . 3 |- ( ph -> ( A ` M ) = 0 )
329		fvex 5689	. . . 4 |- ( A ` M ) e. _V
330	329	elsnc 3889	. . 3 |- ( ( A ` M ) e. { 0 } <-> ( A ` M ) = 0 )
331	328, 330	sylibr 212	. 2 |- ( ph -> ( A ` M ) e. { 0 } )
332		elpreima 5811	. . . . . 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 460	. . 3 |- ( ph -> ( A ` M ) e. ( S \ { 0 } ) )
336	335	eldifbd 3329	. 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 1362   e. wcel 1755   =/= wne 2596   A.wral 2705   E.wrex 2706   _Vcvv 2962   \ cdif 3313   u. cun 3314   C_ wss 3316   (/)c0 3625   ifcif 3779   {csn 3865   class class class wbr 4280   e. cmpt 4338   X. cxp 4825   `'ccnv 4826   dom cdm 4827   "cima 4830   Fn wfn 5401   -->wf 5402   ` cfv 5406  (class class class)co 6080   ^m cmap 7202   Fincfn 7298   supcsup 7678   CCcc 9268   RRcr 9269   0cc0 9270   1c1 9271   + caddc 9273   x. cmul 9275   < clt 9406   <_ cle 9407   - cmin 9583   -ucneg 9584   / cdiv 9981   NNcn 10310   NN0cn0 10567   ZZcz 10634   ZZ>=cuz 10849   RR+crp 10979   ...cfz 11424   ^cexp 11849   abscabs 12707   ~~> cli 12946   sum_csu 13147   0pc0p 20989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-sup 7679  df-oi 7712  df-card 8097  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-n0 10568  df-z 10635  df-uz 10850  df-rp 10980  df-fz 11425  df-fzo 11533  df-fl 11626  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-clim 12950  df-rlim 12951  df-sum 13148  df-0p 20990

This theorem is referenced by:  plyeq0  21564