Theorem logtayl 20504

Description: The Taylor series for -u log ( 1 - A ). (Contributed by Mario Carneiro, 1-Apr-2015.)

Assertion

Ref	Expression
logtayl	|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )

Distinct variable group:   A, k

Proof of Theorem logtayl

Dummy variables j m n r x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 10476	. . . 4 |- NN0 = ( ZZ>= ` 0 )
2		0z 10249	. . . . 5 |- 0 e. ZZ
3	2	a1i 11	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
4		eqeq1 2410	. . . . . . . 8 |- ( k = n -> ( k = 0 <-> n = 0 ) )
5		oveq2 6048	. . . . . . . 8 |- ( k = n -> ( 1 / k ) = ( 1 / n ) )
6	4, 5	ifbieq2d 3719	. . . . . . 7 |- ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
7		oveq2 6048	. . . . . . 7 |- ( k = n -> ( A ^ k ) = ( A ^ n ) )
8	6, 7	oveq12d 6058	. . . . . 6 |- ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
9		eqid 2404	. . . . . 6 |- ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) = ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
10		ovex 6065	. . . . . 6 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
11	8, 9, 10	fvmpt 5765	. . . . 5 |- ( n e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
12	11	adantl 453	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
13		0cn 9040	. . . . . . 7 |- 0 e. CC
14	13	a1i 11	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
15		simpr 448	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
16		elnn0 10179	. . . . . . . . . . . 12 |- ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
17	15, 16	sylib 189	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
18	17	ord 367	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
19	18	con1d 118	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
20	19	imp 419	. . . . . . . 8 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
21	20	nnrecred 10001	. . . . . . 7 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
22	21	recnd 9070	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
23	14, 22	ifclda 3726	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
24		expcl 11354	. . . . . 6 |- ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
25	24	adantlr 696	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
26	23, 25	mulcld 9064	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
27		logtayllem 20503	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. dom ~~> )
28	1, 3, 12, 26, 27	isumclim2 12497	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
29		simpl 444	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
30		eqid 2404	. . . . . . . . 9 |- ( abs o. - ) = ( abs o. - )
31	30	cnmetdval 18758	. . . . . . . 8 |- ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32	29, 13, 31	sylancl 644	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
33		subid1 9278	. . . . . . . . 9 |- ( A e. CC -> ( A - 0 ) = A )
34	33	adantr 452	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
35	34	fveq2d 5691	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
36	32, 35	eqtrd 2436	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
37		simpr 448	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
38	36, 37	eqbrtrd 4192	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
39		cnxmet 18760	. . . . . . 7 |- ( abs o. - ) e. ( * Met ` CC )
40		1rp 10572	. . . . . . . 8 |- 1 e. RR+
41		rpxr 10575	. . . . . . . 8 |- ( 1 e. RR+ -> 1 e. RR* )
42	40, 41	ax-mp 8	. . . . . . 7 |- 1 e. RR*
43		elbl3 18375	. . . . . . 7 |- ( ( ( ( abs o. - ) e. ( * Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ A e. CC ) ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
44	39, 42, 43	mpanl12 664	. . . . . 6 |- ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
45	13, 29, 44	sylancr 645	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
46	38, 45	mpbird 224	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
47		tru 1327	. . . . . 6 |- T.
48		eqid 2404	. . . . . . . 8 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
49	13	a1i 11	. . . . . . . 8 |- ( T. -> 0 e. CC )
50	42	a1i 11	. . . . . . . 8 |- ( T. -> 1 e. RR* )
51		ax-1cn 9004	. . . . . . . . . . . . 13 |- 1 e. CC
52		blssm 18401	. . . . . . . . . . . . . . 15 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
53	39, 13, 42, 52	mp3an 1279	. . . . . . . . . . . . . 14 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
54	53	sseli 3304	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
55		subcl 9261	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
56	51, 54, 55	sylancr 645	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
57	54	abscld 12193	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
58	30	cnmetdval 18758	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
59	54, 13, 58	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
60	54	subid1d 9356	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
61	60	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
62	59, 61	eqtrd 2436	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
63		elbl3 18375	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( abs o. - ) e. ( * Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ y e. CC ) ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
64	39, 42, 63	mpanl12 664	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
65	13, 54, 64	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
66	65	ibi 233	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
67	62, 66	eqbrtrrd 4194	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
68	57, 67	gtned 9164	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
69		abs1 12057	. . . . . . . . . . . . . . . 16 |- ( abs ` 1 ) = 1
70		fveq2 5687	. . . . . . . . . . . . . . . 16 |- ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
71	69, 70	syl5eqr 2450	. . . . . . . . . . . . . . 15 |- ( 1 = y -> 1 = ( abs ` y ) )
72	71	necon3i 2606	. . . . . . . . . . . . . 14 |- ( 1 =/= ( abs ` y ) -> 1 =/= y )
73	68, 72	syl 16	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
74		subeq0 9283	. . . . . . . . . . . . . . 15 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
75	74	necon3bid 2602	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
76	51, 54, 75	sylancr 645	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
77	73, 76	mpbird 224	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
78	56, 77	logcld 20421	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
79	78	negcld 9354	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
80	79	adantl 453	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
81		eqid 2404	. . . . . . . . 9 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) )
82	80, 81	fmptd 5852	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
83	54	absge0d 12201	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
84	57	rexrd 9090	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
85		peano2re 9195	. . . . . . . . . . . . . . . 16 |- ( ( abs ` y ) e. RR -> ( ( abs ` y ) + 1 ) e. RR )
86	57, 85	syl 16	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) + 1 ) e. RR )
87	86	rehalfcld 10170	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
88	87	rexrd 9090	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
89		iccssxr 10949	. . . . . . . . . . . . . . 15 |- ( 0 [,] +oo ) C_ RR*
90		eqeq1 2410	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( m = 0 <-> j = 0 ) )
91		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( 1 / m ) = ( 1 / j ) )
92	90, 91	ifbieq2d 3719	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
93		eqid 2404	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) )
94		c0ex 9041	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
95		ovex 6065	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / j ) e. _V
96	94, 95	ifex 3757	. . . . . . . . . . . . . . . . . . . . 21 |- if ( j = 0 , 0 , ( 1 / j ) ) e. _V
97	92, 93, 96	fvmpt 5765	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
98	97	eqcomd 2409	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
99	98	oveq1d 6055	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN0 -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) )
100	99	mpteq2ia 4251	. . . . . . . . . . . . . . . . 17 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) )
101	100	mpteq2i 4252	. . . . . . . . . . . . . . . 16 |- ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) = ( x e. CC |-> ( j e. NN0 |-> ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) ) )
102	13	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
103		nn0cn 10187	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN0 -> m e. CC )
104	103	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ m e. NN0 ) -> m e. CC )
105		df-ne 2569	. . . . . . . . . . . . . . . . . . . 20 |- ( m =/= 0 <-> -. m = 0 )
106	105	biimpri 198	. . . . . . . . . . . . . . . . . . 19 |- ( -. m = 0 -> m =/= 0 )
107		reccl 9641	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
108	104, 106, 107	syl2an 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
109	102, 108	ifclda 3726	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
110	109, 93	fmptd 5852	. . . . . . . . . . . . . . . 16 |- ( T. -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
111		recn 9036	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. RR -> r e. CC )
112		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = r -> ( x ^ j ) = ( r ^ j ) )
113	112	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
114	113	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = r -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
115		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) = ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) )
116		nn0ex 10183	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
117	116	mptex 5925	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
118	114, 115, 117	fvmpt 5765	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
119	111, 118	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( r e. RR -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
120	119	eqcomd 2409	. . . . . . . . . . . . . . . . . . . 20 |- ( r e. RR -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) = ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) )
121	120	seqeq3d 11286	. . . . . . . . . . . . . . . . . . 19 |- ( r e. RR -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) = seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) )
122	121	eleq1d 2470	. . . . . . . . . . . . . . . . . 18 |- ( r e. RR -> ( seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> <-> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> ) )
123	122	rabbiia 2906	. . . . . . . . . . . . . . . . 17 |- { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } = { r e. RR | seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> }
124	123	supeq1i 7410	. . . . . . . . . . . . . . . 16 |- sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
125	101, 110, 124	radcnvcl 20286	. . . . . . . . . . . . . . 15 |- ( T. -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. ( 0 [,] +oo ) )
126	89, 125	sseldi 3306	. . . . . . . . . . . . . 14 |- ( T. -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
127	47, 126	mp1i 12	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
128		1re 9046	. . . . . . . . . . . . . . 15 |- 1 e. RR
129		avglt1 10161	. . . . . . . . . . . . . . 15 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
130	57, 128, 129	sylancl 644	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
131	67, 130	mpbid 202	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
132		0re 9047	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
133	132	a1i 11	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
134	133, 57, 87, 83, 131	lelttrd 9184	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
135	133, 87, 134	ltled 9177	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
136	87, 135	absidd 12180	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( ( ( abs ` y ) + 1 ) / 2 ) )
137	47, 110	mp1i 12	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
138	87	recnd 9070	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
139		oveq1 6047	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
140	139	oveq2d 6056	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) )
141	140	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
142	116	mptex 5925	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
143	141, 115, 142	fvmpt 5765	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( abs ` y ) + 1 ) / 2 ) e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
144	138, 143	syl 16	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
145	144	seqeq3d 11286	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) ) = seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) )
146		avglt2 10162	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
147	57, 128, 146	sylancl 644	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
148	67, 147	mpbid 202	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
149	136, 148	eqbrtrd 4192	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
150		logtayllem 20503	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( abs ` y ) + 1 ) / 2 ) e. CC /\ ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 ) -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) e. dom ~~> )
151	138, 149, 150	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) e. dom ~~> )
152	145, 151	eqeltrd 2478	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) ) e. dom ~~> )
153	101, 137, 124, 138, 152	radcnvle 20289	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) <_ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
154	136, 153	eqbrtrrd 4194	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) <_ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
155	84, 88, 127, 131, 154	xrltletrd 10707	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
156		elico2 10930	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* ) -> ( ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
157	132, 127, 156	sylancr 645	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
158	57, 83, 155, 157	mpbir3and 1137	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
159		absf 12096	. . . . . . . . . . . 12 |- abs : CC --> RR
160		ffn 5550	. . . . . . . . . . . 12 |- ( abs : CC --> RR -> abs Fn CC )
161		elpreima 5809	. . . . . . . . . . . 12 |- ( abs Fn CC -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) )
162	159, 160, 161	mp2b 10	. . . . . . . . . . 11 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
163	54, 158, 162	sylanbrc 646	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
164		cnvimass 5183	. . . . . . . . . . . . . . . . . 18 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) C_ dom abs
165	159	fdmi 5555	. . . . . . . . . . . . . . . . . 18 |- dom abs = CC
166	164, 165	sseqtri 3340	. . . . . . . . . . . . . . . . 17 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) C_ CC
167	166	sseli 3304	. . . . . . . . . . . . . . . 16 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> y e. CC )
168		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x ^ j ) = ( y ^ j ) )
169	168	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
170	169	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
171	116	mptex 5925	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
172	170, 115, 171	fvmpt 5765	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
173	172	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
174	173	fveq1d 5689	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) )
175		eqeq1 2410	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( j = 0 <-> n = 0 ) )
176		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( 1 / j ) = ( 1 / n ) )
177	175, 176	ifbieq2d 3719	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
178		oveq2 6048	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> ( y ^ j ) = ( y ^ n ) )
179	177, 178	oveq12d 6058	. . . . . . . . . . . . . . . . . . . 20 |- ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
180		eqid 2404	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
181		ovex 6065	. . . . . . . . . . . . . . . . . . . 20 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
182	179, 180, 181	fvmpt 5765	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN0 -> ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
183	182	adantl 453	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
184	174, 183	eqtr2d 2437	. . . . . . . . . . . . . . . . 17 |- ( ( y e. CC /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
185	184	sumeq2dv 12452	. . . . . . . . . . . . . . . 16 |- ( y e. CC -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
186	167, 185	syl 16	. . . . . . . . . . . . . . 15 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
187	186	mpteq2ia 4251	. . . . . . . . . . . . . 14 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
188		eqid 2404	. . . . . . . . . . . . . 14 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) = ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
189		eqid 2404	. . . . . . . . . . . . . 14 |- if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) = if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) )
190	101, 187, 110, 124, 188, 189	psercn 20295	. . . . . . . . . . . . 13 |- ( T. -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) )
191		cncff 18876	. . . . . . . . . . . . 13 |- ( ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
192	190, 191	syl 16	. . . . . . . . . . . 12 |- ( T. -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
193		eqid 2404	. . . . . . . . . . . . 13 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
194	193	fmpt 5849	. . . . . . . . . . . 12 |- ( A. y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC <-> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
195	192, 194	sylibr 204	. . . . . . . . . . 11 |- ( T. -> A. y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
196	195	r19.21bi 2764	. . . . . . . . . 10 |- ( ( T. /\ y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
197	163, 196	sylan2 461	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
198		eqid 2404	. . . . . . . . 9 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
199	197, 198	fmptd 5852	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
200		cnex 9027	. . . . . . . . . . . . . 14 |- CC e. _V
201	200	prid2 3873	. . . . . . . . . . . . 13 |- CC e. { RR , CC }
202	201	a1i 11	. . . . . . . . . . . 12 |- ( T. -> CC e. { RR , CC } )
203	78	adantl 453	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
204		ovex 6065	. . . . . . . . . . . . 13 |- ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V
205	204	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V )
206	30	cnmetdval 18758	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
207	51, 56, 206	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
208		nncan 9286	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
209	51, 54, 208	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
210	209	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
211	207, 210	eqtrd 2436	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
212	211, 67	eqbrtrd 4192	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
213		elbl 18371	. . . . . . . . . . . . . . . 16 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) ) )
214	39, 51, 42, 213	mp3an 1279	. . . . . . . . . . . . . . 15 |- ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
215	56, 212, 214	sylanbrc 646	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
216	215	adantl 453	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
217		neg1cn 10023	. . . . . . . . . . . . . 14 |- -u 1 e. CC
218	217	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
219		eqid 2404	. . . . . . . . . . . . . . . . . 18 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
220	219	dvlog2lem 20496	. . . . . . . . . . . . . . . . 17 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
221	220	sseli 3304	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
222	221	eldifad 3292	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
223		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
224	223	logdmn0 20484	. . . . . . . . . . . . . . . 16 |- ( x e. ( CC \ ( -oo (,] 0 ) ) -> x =/= 0 )
225	221, 224	syl 16	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x =/= 0 )
226	222, 225	logcld 20421	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
227	226	adantl 453	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
228		ovex 6065	. . . . . . . . . . . . . 14 |- ( 1 / x ) e. _V
229	228	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
230		simpr 448	. . . . . . . . . . . . . . 15 |- ( ( T. /\ y e. CC ) -> y e. CC )
231	51, 230, 55	sylancr 645	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
232	217	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> -u 1 e. CC )
233	51	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 1 e. CC )
234	13	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 0 e. CC )
235	51	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. CC )
236	202, 235	dvmptc 19797	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> 1 ) ) = ( y e. CC |-> 0 ) )
237	202	dvmptid 19796	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
238	202, 233, 234, 236, 230, 233, 237	dvmptsub 19806	. . . . . . . . . . . . . . 15 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> ( 0 - 1 ) ) )
239		df-neg 9250	. . . . . . . . . . . . . . . 16 |- -u 1 = ( 0 - 1 )
240	239	mpteq2i 4252	. . . . . . . . . . . . . . 15 |- ( y e. CC |-> -u 1 ) = ( y e. CC |-> ( 0 - 1 ) )
241	238, 240	syl6eqr 2454	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> -u 1 ) )
242	53	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
243		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
244	243	cnfldtop 18771	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) e. Top
245	243	cnfldtopon 18770	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
246	245	toponunii 16952	. . . . . . . . . . . . . . . . 17 |- CC = U. ( TopOpen ` ℂfld )
247	246	restid 13616	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
248	244, 247	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
249	248	eqcomi 2408	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
250	243	cnfldtopn 18769	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
251	250	blopn 18483	. . . . . . . . . . . . . . . 16 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
252	39, 13, 42, 251	mp3an 1279	. . . . . . . . . . . . . . 15 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld )
253	252	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
254	202, 231, 232, 241, 242, 249, 243, 253	dvmptres 19802	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u 1 ) )
255	219	dvlog2 20497	. . . . . . . . . . . . . 14 |- ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) )
256		logf1o 20415	. . . . . . . . . . . . . . . . . . . 20 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
257		f1of 5633	. . . . . . . . . . . . . . . . . . . 20 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
258	256, 257	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 |- log : ( CC \ { 0 } ) --> ran log
259	223	logdmss 20486	. . . . . . . . . . . . . . . . . . . 20 |- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
260	220, 259	sstri 3317	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
261		fssres 5569	. . . . . . . . . . . . . . . . . . 19 |- ( ( log : ( CC \ { 0 } ) --> ran log /\ ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } ) ) -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
262	258, 260, 261	mp2an 654	. . . . . . . . . . . . . . . . . 18 |- ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
264	263	feqmptd 5738	. . . . . . . . . . . . . . . 16 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
265		fvres 5704	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
266	265	mpteq2ia 4251	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) )
267	264, 266	syl6eq 2452	. . . . . . . . . . . . . . 15 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) )
268	267	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) )
269	255, 268	syl5reqr 2451	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) ) )
270		fveq2 5687	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
271		oveq2 6048	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
272	202, 202, 216, 218, 227, 229, 254, 269, 270, 271	dvmptco 19811	. . . . . . . . . . . 12 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) )
273	202, 203, 205, 272	dvmptneg 19805	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) )
274	56, 77	reccld 9739	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
275		mulcom 9032	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 / ( 1 - y ) ) e. CC /\ -u 1 e. CC ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
276	274, 217, 275	sylancl 644	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
277	274	mulm1d 9441	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
278	276, 277	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
279	278	negeqd 9256	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
280	274	negnegd 9358	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
281	279, 280	eqtrd 2436	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
282	281	mpteq2ia 4251	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) )
283	273, 282	syl6eq 2452	. . . . . . . . . 10 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
284	283	dmeqd 5031	. . . . . . . . 9 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
285		dmmptg 5326	. . . . . . . . . 10 |- ( A. y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ( 1 / ( 1 - y ) ) e. _V -> dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
286		ovex 6065	. . . . . . . . . . 11 |- ( 1 / ( 1 - y ) ) e. _V
287	286	a1i 11	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. _V )
288	285, 287	mprg 2735	. . . . . . . . 9 |- dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
289	284, 288	syl6eq 2452	. . . . . . . 8 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
290		sumex 12436	. . . . . . . . . . . 12 |- sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V
291	290	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V )
292		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( n = k -> ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
293	292	cbvsumv 12445	. . . . . . . . . . . . . 14 |- sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k )
294	186, 293	syl6eq 2452	. . . . . . . . . . . . 13 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
295	294	mpteq2ia 4251	. . . . . . . . . . . 12 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
296		eqid 2404	. . . . . . . . . . . 12 |- ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` z ) + if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` z ) + if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) ) / 2 ) )
297	101, 295, 110, 124, 188, 189, 296	pserdv2 20299	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
298	163	ssriv 3312	. . . . . . . . . . . 12 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
299	298	a1i 11	. . . . . . . . . . 11 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
300	202, 196, 291, 297, 299, 249, 243, 253	dvmptres 19802	. . . . . . . . . 10 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
301		nnnn0 10184	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. NN -> n e. NN0 )
302	301	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
303		eqeq1 2410	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( m = 0 <-> n = 0 ) )
304		oveq2 6048	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( 1 / m ) = ( 1 / n ) )
305	303, 304	ifbieq2d 3719	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
306		ovex 6065	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / n ) e. _V
307	94, 306	ifex 3757	. . . . . . . . . . . . . . . . . . . 20 |- if ( n = 0 , 0 , ( 1 / n ) ) e. _V
308	305, 93, 307	fvmpt 5765	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
309	302, 308	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
310		nnne0 9988	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. NN -> n =/= 0 )
311	310	adantl 453	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
312	311	neneqd 2583	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
313		iffalse 3706	. . . . . . . . . . . . . . . . . . 19 |- ( -. n = 0 -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
314	312, 313	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
315	309, 314	eqtrd 2436	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = ( 1 / n ) )
316	315	oveq2d 6056	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = ( n x. ( 1 / n ) ) )
317		nncn 9964	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> n e. CC )
318	317	adantl 453	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
319	318, 311	recidd 9741	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
320	316, 319	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = 1 )
321	320	oveq1d 6055	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( 1 x. ( y ^ ( n - 1 ) ) ) )
322		nnm1nn0 10217	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( n - 1 ) e. NN0 )
323		expcl 11354	. . . . . . . . . . . . . . . 16 |- ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
324	54, 322, 323	syl2an 464	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
325	324	mulid2d 9062	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
326	321, 325	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
327	326	sumeq2dv 12452	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = sum_ n e. NN ( y ^ ( n - 1 ) ) )
328		nnuz 10477	. . . . . . . . . . . . . . 15 |- NN = ( ZZ>= ` 1 )
329		1e0p1 10366	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
330	329	fveq2i 5690	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
331	328, 330	eqtri 2424	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` ( 0 + 1 ) )
332		oveq1 6047	. . . . . . . . . . . . . . 15 |- ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
333	332	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
334		1z 10267	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
335	334	a1i 11	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
336	2	a1i 11	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
337	1, 331, 333, 335, 336, 324	isumshft 12574	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) )
338		pncan2 9268	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
339	51, 103, 338	sylancr 645	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
340	339	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
341	340	sumeq2i 12448	. . . . . . . . . . . . 13 |- sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
342	337, 341	syl6eq 2452	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
343		geoisum 12609	. . . . . . . . . . . . 13 |- ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
344	54, 67, 343	syl2anc 643	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
345	327, 342, 344	3eqtrd 2440	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( 1 / ( 1 - y ) ) )
346	345	mpteq2ia 4251	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) )
347	300, 346	syl6eq 2452	. . . . . . . . 9 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
348	283, 347	eqtr4d 2439	. . . . . . . 8 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y )