Theorem logtayl 23467

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 11182	. . . 4 |- NN0 = ( ZZ>= ` 0 )
2		0zd 10938	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3		eqeq1 2424	. . . . . . . 8 |- ( k = n -> ( k = 0 <-> n = 0 ) )
4		oveq2 6304	. . . . . . . 8 |- ( k = n -> ( 1 / k ) = ( 1 / n ) )
5	3, 4	ifbieq2d 3931	. . . . . . 7 |- ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
6		oveq2 6304	. . . . . . 7 |- ( k = n -> ( A ^ k ) = ( A ^ n ) )
7	5, 6	oveq12d 6314	. . . . . 6 |- ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
8		eqid 2420	. . . . . 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 ) ) )
9		ovex 6324	. . . . . 6 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
10	7, 8, 9	fvmpt 5955	. . . . 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 ) ) )
11	10	adantl 467	. . . 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 ) ) )
12		0cnd 9625	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
13		simpr 462	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
14		elnn0 10860	. . . . . . . . . . . 12 |- ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
15	13, 14	sylib 199	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
16	15	ord 378	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
17	16	con1d 127	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
18	17	imp 430	. . . . . . . 8 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
19	18	nnrecred 10644	. . . . . . 7 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
20	19	recnd 9658	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
21	12, 20	ifclda 3938	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
22		expcl 12276	. . . . . 6 |- ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
23	22	adantlr 719	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
24	21, 23	mulcld 9652	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
25		logtayllem 23466	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. dom ~~> )
26	1, 2, 11, 24, 25	isumclim2 13786	. . 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 ) ) )
27		simpl 458	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
28		0cn 9624	. . . . . . . 8 |- 0 e. CC
29		eqid 2420	. . . . . . . . 9 |- ( abs o. - ) = ( abs o. - )
30	29	cnmetdval 21695	. . . . . . . 8 |- ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
31	27, 28, 30	sylancl 666	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32		subid1 9883	. . . . . . . . 9 |- ( A e. CC -> ( A - 0 ) = A )
33	32	adantr 466	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
34	33	fveq2d 5876	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
35	31, 34	eqtrd 2461	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
36		simpr 462	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
37	35, 36	eqbrtrd 4437	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
38		cnxmet 21697	. . . . . . 7 |- ( abs o. - ) e. ( *Met ` CC )
39		1rp 11295	. . . . . . . 8 |- 1 e. RR+
40		rpxr 11298	. . . . . . . 8 |- ( 1 e. RR+ -> 1 e. RR* )
41	39, 40	ax-mp 5	. . . . . . 7 |- 1 e. RR*
42		elbl3 21331	. . . . . . 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 ) )
43	38, 41, 42	mpanl12 686	. . . . . 6 |- ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
44	28, 27, 43	sylancr 667	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
45	37, 44	mpbird 235	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
46		tru 1441	. . . . . 6 |- T.
47		eqid 2420	. . . . . . . 8 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
48		0cnd 9625	. . . . . . . 8 |- ( T. -> 0 e. CC )
49	41	a1i 11	. . . . . . . 8 |- ( T. -> 1 e. RR* )
50		ax-1cn 9586	. . . . . . . . . . . . 13 |- 1 e. CC
51		blssm 21357	. . . . . . . . . . . . . . 15 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
52	38, 28, 41, 51	mp3an 1360	. . . . . . . . . . . . . 14 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
53	52	sseli 3457	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
54		subcl 9863	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
55	50, 53, 54	sylancr 667	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
56	53	abscld 13465	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
57	29	cnmetdval 21695	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
58	53, 28, 57	sylancl 666	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
59	53	subid1d 9964	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
60	59	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
61	58, 60	eqtrd 2461	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
62		elbl3 21331	. . . . . . . . . . . . . . . . . . 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 ) )
63	38, 41, 62	mpanl12 686	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
64	28, 53, 63	sylancr 667	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
65	64	ibi 244	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
66	61, 65	eqbrtrrd 4439	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
67	56, 66	gtned 9759	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
68		abs1 13328	. . . . . . . . . . . . . . . 16 |- ( abs ` 1 ) = 1
69		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
70	68, 69	syl5eqr 2475	. . . . . . . . . . . . . . 15 |- ( 1 = y -> 1 = ( abs ` y ) )
71	70	necon3i 2662	. . . . . . . . . . . . . 14 |- ( 1 =/= ( abs ` y ) -> 1 =/= y )
72	67, 71	syl 17	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
73		subeq0 9889	. . . . . . . . . . . . . . 15 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
74	73	necon3bid 2680	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
75	50, 53, 74	sylancr 667	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
76	72, 75	mpbird 235	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
77	55, 76	logcld 23382	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
78	77	negcld 9962	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
79	78	adantl 467	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
80		eqid 2420	. . . . . . . . 9 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) )
81	79, 80	fmptd 6052	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
82	53	absge0d 13473	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
83	56	rexrd 9679	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
84		peano2re 9795	. . . . . . . . . . . . . . . 16 |- ( ( abs ` y ) e. RR -> ( ( abs ` y ) + 1 ) e. RR )
85	56, 84	syl 17	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) + 1 ) e. RR )
86	85	rehalfcld 10848	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
87	86	rexrd 9679	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
88		iccssxr 11706	. . . . . . . . . . . . . . 15 |- ( 0 [,] +oo ) C_ RR*
89		eqeq1 2424	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( m = 0 <-> j = 0 ) )
90		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( 1 / m ) = ( 1 / j ) )
91	89, 90	ifbieq2d 3931	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
92		eqid 2420	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) )
93		c0ex 9626	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
94		ovex 6324	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / j ) e. _V
95	93, 94	ifex 3974	. . . . . . . . . . . . . . . . . . . . 21 |- if ( j = 0 , 0 , ( 1 / j ) ) e. _V
96	91, 92, 95	fvmpt 5955	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
97	96	eqcomd 2428	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
98	97	oveq1d 6311	. . . . . . . . . . . . . . . . . 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 ) ) )
99	98	mpteq2ia 4499	. . . . . . . . . . . . . . . . 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 ) ) )
100	99	mpteq2i 4500	. . . . . . . . . . . . . . . 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 ) ) ) )
101		0cnd 9625	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
102		nn0cn 10868	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN0 -> m e. CC )
103	102	adantl 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ m e. NN0 ) -> m e. CC )
104		df-ne 2618	. . . . . . . . . . . . . . . . . . . 20 |- ( m =/= 0 <-> -. m = 0 )
105	104	biimpri 209	. . . . . . . . . . . . . . . . . . 19 |- ( -. m = 0 -> m =/= 0 )
106		reccl 10266	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
107	103, 105, 106	syl2an 479	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
108	101, 107	ifclda 3938	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
109	108, 92	fmptd 6052	. . . . . . . . . . . . . . . 16 |- ( T. -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
110		recn 9618	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. RR -> r e. CC )
111		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = r -> ( x ^ j ) = ( r ^ j ) )
112	111	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
113	112	mpteq2dv 4504	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
114		eqid 2420	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
115		nn0ex 10864	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
116	115	mptex 6142	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
117	113, 114, 116	fvmpt 5955	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
118	110, 117	syl 17	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
119	118	eqcomd 2428	. . . . . . . . . . . . . . . . . . . 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 ) )
120	119	seqeq3d 12207	. . . . . . . . . . . . . . . . . . 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 ) ) )
121	120	eleq1d 2489	. . . . . . . . . . . . . . . . . 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 ~~> ) )
122	121	rabbiia 3067	. . . . . . . . . . . . . . . . 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 ~~> }
123	122	supeq1i 7958	. . . . . . . . . . . . . . . 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* , < )
124	100, 109, 123	radcnvcl 23234	. . . . . . . . . . . . . . 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 ) )
125	88, 124	sseldi 3459	. . . . . . . . . . . . . 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* )
126	46, 125	mp1i 13	. . . . . . . . . . . . 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* )
127		1re 9631	. . . . . . . . . . . . . . 15 |- 1 e. RR
128		avglt1 10839	. . . . . . . . . . . . . . 15 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
129	56, 127, 128	sylancl 666	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
130	66, 129	mpbid 213	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
131		0red 9633	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
132	131, 56, 86, 82, 130	lelttrd 9782	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
133	131, 86, 132	ltled 9772	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
134	86, 133	absidd 13452	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( ( ( abs ` y ) + 1 ) / 2 ) )
135	46, 109	mp1i 13	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
136	86	recnd 9658	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
137		oveq1 6303	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
138	137	oveq2d 6312	. . . . . . . . . . . . . . . . . . . 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 ) ) )
139	138	mpteq2dv 4504	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
140	115	mptex 6142	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
141	139, 114, 140	fvmpt 5955	. . . . . . . . . . . . . . . . . 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 ) ) ) )
142	136, 141	syl 17	. . . . . . . . . . . . . . . . 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 ) ) ) )
143	142	seqeq3d 12207	. . . . . . . . . . . . . . . 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 ) ) ) ) )
144		avglt2 10840	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
145	56, 127, 144	sylancl 666	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
146	66, 145	mpbid 213	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
147	134, 146	eqbrtrd 4437	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
148		logtayllem 23466	. . . . . . . . . . . . . . . . 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 ~~> )
149	136, 147, 148	syl2anc 665	. . . . . . . . . . . . . . . 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 ~~> )
150	143, 149	eqeltrd 2508	. . . . . . . . . . . . . . 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 ~~> )
151	100, 135, 123, 136, 150	radcnvle 23237	. . . . . . . . . . . . . 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* , < ) )
152	134, 151	eqbrtrrd 4439	. . . . . . . . . . . . 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* , < ) )
153	83, 87, 126, 130, 152	xrltletrd 11447	. . . . . . . . . . . 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* , < ) )
154		0re 9632	. . . . . . . . . . . . 13 |- 0 e. RR
155		elico2 11687	. . . . . . . . . . . . 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* , < ) ) ) )
156	154, 126, 155	sylancr 667	. . . . . . . . . . . 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* , < ) ) ) )
157	56, 82, 153, 156	mpbir3and 1188	. . . . . . . . . . 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* , < ) ) )
158		absf 13368	. . . . . . . . . . . 12 |- abs : CC --> RR
159		ffn 5737	. . . . . . . . . . . 12 |- ( abs : CC --> RR -> abs Fn CC )
160		elpreima 6008	. . . . . . . . . . . 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* , < ) ) ) ) )
161	158, 159, 160	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* , < ) ) ) )
162	53, 157, 161	sylanbrc 668	. . . . . . . . . 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* , < ) ) ) )
163		cnvimass 5199	. . . . . . . . . . . . . . . . . 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
164	158	fdmi 5742	. . . . . . . . . . . . . . . . . 18 |- dom abs = CC
165	163, 164	sseqtri 3493	. . . . . . . . . . . . . . . . 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
166	165	sseli 3457	. . . . . . . . . . . . . . . 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 )
167		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x ^ j ) = ( y ^ j ) )
168	167	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
169	168	mpteq2dv 4504	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
170	115	mptex 6142	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
171	169, 114, 170	fvmpt 5955	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
172	171	adantr 466	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
173	172	fveq1d 5874	. . . . . . . . . . . . . . . . . 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 ) )
174		eqeq1 2424	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( j = 0 <-> n = 0 ) )
175		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( 1 / j ) = ( 1 / n ) )
176	174, 175	ifbieq2d 3931	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
177		oveq2 6304	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> ( y ^ j ) = ( y ^ n ) )
178	176, 177	oveq12d 6314	. . . . . . . . . . . . . . . . . . . 20 |- ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
179		eqid 2420	. . . . . . . . . . . . . . . . . . . 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 ) ) )
180		ovex 6324	. . . . . . . . . . . . . . . . . . . 20 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
181	178, 179, 180	fvmpt 5955	. . . . . . . . . . . . . . . . . . 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 ) ) )
182	181	adantl 467	. . . . . . . . . . . . . . . . . 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 ) ) )
183	173, 182	eqtr2d 2462	. . . . . . . . . . . . . . . . 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 ) )
184	183	sumeq2dv 13736	. . . . . . . . . . . . . . . 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 ) )
185	166, 184	syl 17	. . . . . . . . . . . . . . 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 ) )
186	185	mpteq2ia 4499	. . . . . . . . . . . . . 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 ) )
187		eqid 2420	. . . . . . . . . . . . . 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* , < ) ) )
188		eqid 2420	. . . . . . . . . . . . . 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 ) )
189	100, 186, 109, 123, 187, 188	psercn 23243	. . . . . . . . . . . . 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 ) )
190		cncff 21814	. . . . . . . . . . . . 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 )
191	189, 190	syl 17	. . . . . . . . . . . 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 )
192		eqid 2420	. . . . . . . . . . . . 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 ) ) )
193	192	fmpt 6049	. . . . . . . . . . . 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 )
194	191, 193	sylibr 215	. . . . . . . . . . 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 )
195	194	r19.21bi 2792	. . . . . . . . . 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 )
196	162, 195	sylan2 476	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
197		eqid 2420	. . . . . . . . 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 ) ) )
198	196, 197	fmptd 6052	. . . . . . . 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 )
199		cnelprrecn 9621	. . . . . . . . . . . . 13 |- CC e. { RR , CC }
200	199	a1i 11	. . . . . . . . . . . 12 |- ( T. -> CC e. { RR , CC } )
201	77	adantl 467	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
202		ovex 6324	. . . . . . . . . . . . 13 |- ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V
203	202	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V )
204	29	cnmetdval 21695	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
205	50, 55, 204	sylancr 667	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
206		nncan 9892	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
207	50, 53, 206	sylancr 667	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
208	207	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
209	205, 208	eqtrd 2461	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
210	209, 66	eqbrtrd 4437	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
211		elbl 21327	. . . . . . . . . . . . . . . 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 ) ) )
212	38, 50, 41, 211	mp3an 1360	. . . . . . . . . . . . . . 15 |- ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
213	55, 210, 212	sylanbrc 668	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
214	213	adantl 467	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
215		neg1cn 10702	. . . . . . . . . . . . . 14 |- -u 1 e. CC
216	215	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
217		eqid 2420	. . . . . . . . . . . . . . . . . 18 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
218	217	dvlog2lem 23459	. . . . . . . . . . . . . . . . 17 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
219	218	sseli 3457	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
220	219	eldifad 3445	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
221		eqid 2420	. . . . . . . . . . . . . . . . 17 |- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
222	221	logdmn0 23447	. . . . . . . . . . . . . . . 16 |- ( x e. ( CC \ ( -oo (,] 0 ) ) -> x =/= 0 )
223	219, 222	syl 17	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x =/= 0 )
224	220, 223	logcld 23382	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
225	224	adantl 467	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
226		ovex 6324	. . . . . . . . . . . . . 14 |- ( 1 / x ) e. _V
227	226	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
228		simpr 462	. . . . . . . . . . . . . . 15 |- ( ( T. /\ y e. CC ) -> y e. CC )
229	50, 228, 54	sylancr 667	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
230	215	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> -u 1 e. CC )
231		1cnd 9648	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 1 e. CC )
232		0cnd 9625	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 0 e. CC )
233		1cnd 9648	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. CC )
234	200, 233	dvmptc 22786	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> 1 ) ) = ( y e. CC |-> 0 ) )
235	200	dvmptid 22785	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
236	200, 231, 232, 234, 228, 231, 235	dvmptsub 22795	. . . . . . . . . . . . . . 15 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> ( 0 - 1 ) ) )
237		df-neg 9852	. . . . . . . . . . . . . . . 16 |- -u 1 = ( 0 - 1 )
238	237	mpteq2i 4500	. . . . . . . . . . . . . . 15 |- ( y e. CC |-> -u 1 ) = ( y e. CC |-> ( 0 - 1 ) )
239	236, 238	syl6eqr 2479	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> -u 1 ) )
240	52	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
241		eqid 2420	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
242	241	cnfldtop 21708	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) e. Top
243	241	cnfldtopon 21707	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
244	243	toponunii 19871	. . . . . . . . . . . . . . . . 17 |- CC = U. ( TopOpen ` ℂfld )
245	244	restid 15284	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
246	242, 245	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
247	246	eqcomi 2433	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
248	241	cnfldtopn 21706	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
249	248	blopn 21439	. . . . . . . . . . . . . . . 16 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
250	38, 28, 41, 249	mp3an 1360	. . . . . . . . . . . . . . 15 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld )
251	250	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
252	200, 229, 230, 239, 240, 247, 241, 251	dvmptres 22791	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u 1 ) )
253	217	dvlog2 23460	. . . . . . . . . . . . . 14 |- ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) )
254		logf1o 23376	. . . . . . . . . . . . . . . . . . . 20 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
255		f1of 5822	. . . . . . . . . . . . . . . . . . . 20 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
256	254, 255	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- log : ( CC \ { 0 } ) --> ran log
257	221	logdmss 23449	. . . . . . . . . . . . . . . . . . . 20 |- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
258	218, 257	sstri 3470	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
259		fssres 5757	. . . . . . . . . . . . . . . . . . 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 )
260	256, 258, 259	mp2an 676	. . . . . . . . . . . . . . . . . 18 |- ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log
261	260	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
262	261	feqmptd 5925	. . . . . . . . . . . . . . . 16 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
263		fvres 5886	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
264	263	mpteq2ia 4499	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) )
265	262, 264	syl6eq 2477	. . . . . . . . . . . . . . 15 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) )
266	265	oveq2d 6312	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) )
267	253, 266	syl5reqr 2476	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) ) )
268		fveq2 5872	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
269		oveq2 6304	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
270	200, 200, 214, 216, 225, 227, 252, 267, 268, 269	dvmptco 22800	. . . . . . . . . . . 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 ) ) )
271	200, 201, 203, 270	dvmptneg 22794	. . . . . . . . . . 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 ) ) )
272	55, 76	reccld 10365	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
273		mulcom 9614	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 / ( 1 - y ) ) e. CC /\ -u 1 e. CC ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
274	272, 215, 273	sylancl 666	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
275	272	mulm1d 10059	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
276	274, 275	eqtrd 2461	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
277	276	negeqd 9858	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
278	272	negnegd 9966	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
279	277, 278	eqtrd 2461	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
280	279	mpteq2ia 4499	. . . . . . . . . . 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 ) ) )
281	271, 280	syl6eq 2477	. . . . . . . . . 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 ) ) ) )
282	281	dmeqd 5048	. . . . . . . . 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 ) ) ) )
283		dmmptg 5343	. . . . . . . . . 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 ) )
284		ovex 6324	. . . . . . . . . . 11 |- ( 1 / ( 1 - y ) ) e. _V
285	284	a1i 11	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. _V )
286	283, 285	mprg 2786	. . . . . . . . 9 |- dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
287	282, 286	syl6eq 2477	. . . . . . . 8 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
288		sumex 13721	. . . . . . . . . . . 12 |- sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V
289	288	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 )
290		fveq2 5872	. . . . . . . . . . . . . . 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 ) )
291	290	cbvsumv 13729	. . . . . . . . . . . . . 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 )
292	185, 291	syl6eq 2477	. . . . . . . . . . . . 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 ) )
293	292	mpteq2ia 4499	. . . . . . . . . . . 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 ) )
294		eqid 2420	. . . . . . . . . . . 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 ) )
295	100, 293, 109, 123, 187, 188, 294	pserdv2 23247	. . . . . . . . . . 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 ) ) ) ) )
296	162	ssriv 3465	. . . . . . . . . . . 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* , < ) ) )
297	296	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* , < ) ) ) )
298	200, 195, 289, 295, 297, 247, 241, 251	dvmptres 22791	. . . . . . . . . 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 ) ) ) ) )
299		nnnn0 10865	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. NN -> n e. NN0 )
300	299	adantl 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
301		eqeq1 2424	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( m = 0 <-> n = 0 ) )
302		oveq2 6304	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( 1 / m ) = ( 1 / n ) )
303	301, 302	ifbieq2d 3931	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
304		ovex 6324	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / n ) e. _V
305	93, 304	ifex 3974	. . . . . . . . . . . . . . . . . . . 20 |- if ( n = 0 , 0 , ( 1 / n ) ) e. _V
306	303, 92, 305	fvmpt 5955	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
307	300, 306	syl 17	. . . . . . . . . . . . . . . . . 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 ) ) )
308		nnne0 10631	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. NN -> n =/= 0 )
309	308	adantl 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
310	309	neneqd 2623	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
311	310	iffalsed 3917	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
312	307, 311	eqtrd 2461	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = ( 1 / n ) )
313	312	oveq2d 6312	. . . . . . . . . . . . . . . 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 ) ) )
314		nncn 10606	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> n e. CC )
315	314	adantl 467	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
316	315, 309	recidd 10367	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
317	313, 316	eqtrd 2461	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = 1 )
318	317	oveq1d 6311	. . . . . . . . . . . . . 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 ) ) ) )
319		nnm1nn0 10900	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( n - 1 ) e. NN0 )
320		expcl 12276	. . . . . . . . . . . . . . . 16 |- ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
321	53, 319, 320	syl2an 479	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
322	321	mulid2d 9650	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
323	318, 322	eqtrd 2461	. . . . . . . . . . . . 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 ) ) )
324	323	sumeq2dv 13736	. . . . . . . . . . . 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 ) ) )
325		nnuz 11183	. . . . . . . . . . . . . . 15 |- NN = ( ZZ>= ` 1 )
326		1e0p1 11068	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
327	326	fveq2i 5875	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
328	325, 327	eqtri 2449	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` ( 0 + 1 ) )
329		oveq1 6303	. . . . . . . . . . . . . . 15 |- ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
330	329	oveq2d 6312	. . . . . . . . . . . . . 14 |- ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
331		1zzd 10957	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
332		0zd 10938	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
333	1, 328, 330, 331, 332, 321	isumshft 13864	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) )
334		pncan2 9871	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
335	50, 102, 334	sylancr 667	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
336	335	oveq2d 6312	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
337	336	sumeq2i 13732	. . . . . . . . . . . . 13 |- sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
338	333, 337	syl6eq 2477	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
339		geoisum 13900	. . . . . . . . . . . . 13 |- ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
340	53, 66, 339	syl2anc 665	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
341	324, 338, 340	3eqtrd 2465	. . . . . . . . . . 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 ) ) )
342	341	mpteq2ia 4499	. . . . . . . . . 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 ) ) )
343	298, 342	syl6eq 2477	. . . . . . . . 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 ) ) ) )
344	281, 343	eqtr4d 2464	. . . . . . . 8 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) )
345		blcntr 21352	. . . . . . . . . 10 |- ( ( ( abs