Theorem logtayl 23605

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 11193	. . . 4 |- NN0 = ( ZZ>= ` 0 )
2		0zd 10949	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3		eqeq1 2455	. . . . . . . 8 |- ( k = n -> ( k = 0 <-> n = 0 ) )
4		oveq2 6298	. . . . . . . 8 |- ( k = n -> ( 1 / k ) = ( 1 / n ) )
5	3, 4	ifbieq2d 3906	. . . . . . 7 |- ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
6		oveq2 6298	. . . . . . 7 |- ( k = n -> ( A ^ k ) = ( A ^ n ) )
7	5, 6	oveq12d 6308	. . . . . 6 |- ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
8		eqid 2451	. . . . . 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 6318	. . . . . 6 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
10	7, 8, 9	fvmpt 5948	. . . . 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 468	. . . 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 9636	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
13		simpr 463	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
14		elnn0 10871	. . . . . . . . . . . 12 |- ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
15	13, 14	sylib 200	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
16	15	ord 379	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
17	16	con1d 128	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
18	17	imp 431	. . . . . . . 8 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
19	18	nnrecred 10655	. . . . . . 7 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
20	19	recnd 9669	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
21	12, 20	ifclda 3913	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
22		expcl 12290	. . . . . 6 |- ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
23	22	adantlr 721	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
24	21, 23	mulcld 9663	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
25		logtayllem 23604	. . . 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 13819	. . 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 459	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
28		0cn 9635	. . . . . . . 8 |- 0 e. CC
29		eqid 2451	. . . . . . . . 9 |- ( abs o. - ) = ( abs o. - )
30	29	cnmetdval 21791	. . . . . . . 8 |- ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
31	27, 28, 30	sylancl 668	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32		subid1 9894	. . . . . . . . 9 |- ( A e. CC -> ( A - 0 ) = A )
33	32	adantr 467	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
34	33	fveq2d 5869	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
35	31, 34	eqtrd 2485	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
36		simpr 463	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
37	35, 36	eqbrtrd 4423	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
38		cnxmet 21793	. . . . . . 7 |- ( abs o. - ) e. ( *Met ` CC )
39		1rp 11306	. . . . . . . 8 |- 1 e. RR+
40		rpxr 11309	. . . . . . . 8 |- ( 1 e. RR+ -> 1 e. RR* )
41	39, 40	ax-mp 5	. . . . . . 7 |- 1 e. RR*
42		elbl3 21407	. . . . . . 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 688	. . . . . 6 |- ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
44	28, 27, 43	sylancr 669	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
45	37, 44	mpbird 236	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
46		tru 1448	. . . . . 6 |- T.
47		eqid 2451	. . . . . . . 8 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
48		0cnd 9636	. . . . . . . 8 |- ( T. -> 0 e. CC )
49	41	a1i 11	. . . . . . . 8 |- ( T. -> 1 e. RR* )
50		ax-1cn 9597	. . . . . . . . . . . . 13 |- 1 e. CC
51		blssm 21433	. . . . . . . . . . . . . . 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 1364	. . . . . . . . . . . . . 14 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
53	52	sseli 3428	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
54		subcl 9874	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
55	50, 53, 54	sylancr 669	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
56	53	abscld 13498	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
57	29	cnmetdval 21791	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
58	53, 28, 57	sylancl 668	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
59	53	subid1d 9975	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
60	59	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
61	58, 60	eqtrd 2485	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
62		elbl3 21407	. . . . . . . . . . . . . . . . . . 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 688	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
64	28, 53, 63	sylancr 669	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
65	64	ibi 245	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
66	61, 65	eqbrtrrd 4425	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
67	56, 66	gtned 9770	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
68		abs1 13360	. . . . . . . . . . . . . . . 16 |- ( abs ` 1 ) = 1
69		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
70	68, 69	syl5eqr 2499	. . . . . . . . . . . . . . 15 |- ( 1 = y -> 1 = ( abs ` y ) )
71	70	necon3i 2656	. . . . . . . . . . . . . 14 |- ( 1 =/= ( abs ` y ) -> 1 =/= y )
72	67, 71	syl 17	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
73		subeq0 9900	. . . . . . . . . . . . . . 15 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
74	73	necon3bid 2668	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
75	50, 53, 74	sylancr 669	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
76	72, 75	mpbird 236	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
77	55, 76	logcld 23520	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
78	77	negcld 9973	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
79	78	adantl 468	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
80		eqid 2451	. . . . . . . . 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 6046	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
82	53	absge0d 13506	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
83	56	rexrd 9690	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
84		peano2re 9806	. . . . . . . . . . . . . . . 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 10859	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
87	86	rexrd 9690	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
88		iccssxr 11717	. . . . . . . . . . . . . . 15 |- ( 0 [,] +oo ) C_ RR*
89		eqeq1 2455	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( m = 0 <-> j = 0 ) )
90		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( 1 / m ) = ( 1 / j ) )
91	89, 90	ifbieq2d 3906	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
92		eqid 2451	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) )
93		c0ex 9637	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
94		ovex 6318	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / j ) e. _V
95	93, 94	ifex 3949	. . . . . . . . . . . . . . . . . . . . 21 |- if ( j = 0 , 0 , ( 1 / j ) ) e. _V
96	91, 92, 95	fvmpt 5948	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
97	96	eqcomd 2457	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
98	97	oveq1d 6305	. . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . 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 4486	. . . . . . . . . . . . . . . 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 9636	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
102		nn0cn 10879	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN0 -> m e. CC )
103	102	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ m e. NN0 ) -> m e. CC )
104		df-ne 2624	. . . . . . . . . . . . . . . . . . . 20 |- ( m =/= 0 <-> -. m = 0 )
105	104	biimpri 210	. . . . . . . . . . . . . . . . . . 19 |- ( -. m = 0 -> m =/= 0 )
106		reccl 10277	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
107	103, 105, 106	syl2an 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
108	101, 107	ifclda 3913	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
109	108, 92	fmptd 6046	. . . . . . . . . . . . . . . 16 |- ( T. -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
110		recn 9629	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. RR -> r e. CC )
111		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = r -> ( x ^ j ) = ( r ^ j ) )
112	111	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
113	112	mpteq2dv 4490	. . . . . . . . . . . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . . . . . . . . . . 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 10875	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
116	115	mptex 6136	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
117	113, 114, 116	fvmpt 5948	. . . . . . . . . . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . . . . . . . . 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 12221	. . . . . . . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . . . . . . 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 3033	. . . . . . . . . . . . . . . . 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 7961	. . . . . . . . . . . . . . . 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 23372	. . . . . . . . . . . . . . 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 3430	. . . . . . . . . . . . . 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 9642	. . . . . . . . . . . . . . 15 |- 1 e. RR
128		avglt1 10850	. . . . . . . . . . . . . . 15 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
129	56, 127, 128	sylancl 668	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
130	66, 129	mpbid 214	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
131		0red 9644	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
132	131, 56, 86, 82, 130	lelttrd 9793	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
133	131, 86, 132	ltled 9783	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
134	86, 133	absidd 13484	. . . . . . . . . . . . . 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 9669	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
137		oveq1 6297	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
138	137	oveq2d 6306	. . . . . . . . . . . . . . . . . . . 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 4490	. . . . . . . . . . . . . . . . . . 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 6136	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
141	139, 114, 140	fvmpt 5948	. . . . . . . . . . . . . . . . . 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 12221	. . . . . . . . . . . . . . . 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 10851	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
145	56, 127, 144	sylancl 668	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
146	66, 145	mpbid 214	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
147	134, 146	eqbrtrd 4423	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
148		logtayllem 23604	. . . . . . . . . . . . . . . . 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 667	. . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . 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 23375	. . . . . . . . . . . . . 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 4425	. . . . . . . . . . . . 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 11458	. . . . . . . . . . . 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 9643	. . . . . . . . . . . . 13 |- 0 e. RR
155		elico2 11698	. . . . . . . . . . . . 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 669	. . . . . . . . . . . 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 1191	. . . . . . . . . . 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 13400	. . . . . . . . . . . 12 |- abs : CC --> RR
159		ffn 5728	. . . . . . . . . . . 12 |- ( abs : CC --> RR -> abs Fn CC )
160		elpreima 6002	. . . . . . . . . . . 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 670	. . . . . . . . . 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 5188	. . . . . . . . . . . . . . . . . 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 5734	. . . . . . . . . . . . . . . . . 18 |- dom abs = CC
165	163, 164	sseqtri 3464	. . . . . . . . . . . . . . . . 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 3428	. . . . . . . . . . . . . . . 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 6297	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x ^ j ) = ( y ^ j ) )
168	167	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
169	168	mpteq2dv 4490	. . . . . . . . . . . . . . . . . . . . 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 6136	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
171	169, 114, 170	fvmpt 5948	. . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . 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 5867	. . . . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( j = 0 <-> n = 0 ) )
175		oveq2 6298	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( 1 / j ) = ( 1 / n ) )
176	174, 175	ifbieq2d 3906	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
177		oveq2 6298	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> ( y ^ j ) = ( y ^ n ) )
178	176, 177	oveq12d 6308	. . . . . . . . . . . . . . . . . . . 20 |- ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
179		eqid 2451	. . . . . . . . . . . . . . . . . . . 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 6318	. . . . . . . . . . . . . . . . . . . 20 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
181	178, 179, 180	fvmpt 5948	. . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . 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 2486	. . . . . . . . . . . . . . . . 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 13769	. . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . 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 23381	. . . . . . . . . . . . 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 21925	. . . . . . . . . . . . 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 2451	. . . . . . . . . . . . 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 6043	. . . . . . . . . . . 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 216	. . . . . . . . . . 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 2757	. . . . . . . . . 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 477	. . . . . . . . 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 2451	. . . . . . . . 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 6046	. . . . . . . 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 9632	. . . . . . . . . . . . 13 |- CC e. { RR , CC }
200	199	a1i 11	. . . . . . . . . . . 12 |- ( T. -> CC e. { RR , CC } )
201	77	adantl 468	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
202		ovex 6318	. . . . . . . . . . . . 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 21791	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
205	50, 55, 204	sylancr 669	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
206		nncan 9903	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
207	50, 53, 206	sylancr 669	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
208	207	fveq2d 5869	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
209	205, 208	eqtrd 2485	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
210	209, 66	eqbrtrd 4423	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
211		elbl 21403	. . . . . . . . . . . . . . . 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 1364	. . . . . . . . . . . . . . 15 |- ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
213	55, 210, 212	sylanbrc 670	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
214	213	adantl 468	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
215		neg1cn 10713	. . . . . . . . . . . . . 14 |- -u 1 e. CC
216	215	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
217		eqid 2451	. . . . . . . . . . . . . . . . . 18 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
218	217	dvlog2lem 23597	. . . . . . . . . . . . . . . . 17 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
219	218	sseli 3428	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
220	219	eldifad 3416	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
221		eqid 2451	. . . . . . . . . . . . . . . . 17 |- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
222	221	logdmn0 23585	. . . . . . . . . . . . . . . 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 23520	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
225	224	adantl 468	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
226		ovex 6318	. . . . . . . . . . . . . 14 |- ( 1 / x ) e. _V
227	226	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
228		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( T. /\ y e. CC ) -> y e. CC )
229	50, 228, 54	sylancr 669	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
230	215	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> -u 1 e. CC )
231		1cnd 9659	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 1 e. CC )
232		0cnd 9636	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 0 e. CC )
233		1cnd 9659	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. CC )
234	200, 233	dvmptc 22912	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> 1 ) ) = ( y e. CC |-> 0 ) )
235	200	dvmptid 22911	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
236	200, 231, 232, 234, 228, 231, 235	dvmptsub 22921	. . . . . . . . . . . . . . 15 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> ( 0 - 1 ) ) )
237		df-neg 9863	. . . . . . . . . . . . . . . 16 |- -u 1 = ( 0 - 1 )
238	237	mpteq2i 4486	. . . . . . . . . . . . . . 15 |- ( y e. CC |-> -u 1 ) = ( y e. CC |-> ( 0 - 1 ) )
239	236, 238	syl6eqr 2503	. . . . . . . . . . . . . 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 2451	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
242	241	cnfldtop 21804	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) e. Top
243	241	cnfldtopon 21803	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
244	243	toponunii 19947	. . . . . . . . . . . . . . . . 17 |- CC = U. ( TopOpen ` ℂfld )
245	244	restid 15332	. . . . . . . . . . . . . . . 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 2460	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
248	241	cnfldtopn 21802	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
249	248	blopn 21515	. . . . . . . . . . . . . . . 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 1364	. . . . . . . . . . . . . . 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 22917	. . . . . . . . . . . . 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 23598	. . . . . . . . . . . . . 14 |- ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) )
254		logf1o 23514	. . . . . . . . . . . . . . . . . . . 20 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
255		f1of 5814	. . . . . . . . . . . . . . . . . . . 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 23587	. . . . . . . . . . . . . . . . . . . 20 |- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
258	218, 257	sstri 3441	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
259		fssres 5749	. . . . . . . . . . . . . . . . . . 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 678	. . . . . . . . . . . . . . . . . 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 5918	. . . . . . . . . . . . . . . 16 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
263		fvres 5879	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
264	263	mpteq2ia 4485	. . . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . 15 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) )
266	265	oveq2d 6306	. . . . . . . . . . . . . 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 2500	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) ) )
268		fveq2 5865	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
269		oveq2 6298	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
270	200, 200, 214, 216, 225, 227, 252, 267, 268, 269	dvmptco 22926	. . . . . . . . . . . 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 22920	. . . . . . . . . . 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 10376	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
273		mulcom 9625	. . . . . . . . . . . . . . . 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 668	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
275	272	mulm1d 10070	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
276	274, 275	eqtrd 2485	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
277	276	negeqd 9869	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
278	272	negnegd 9977	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
279	277, 278	eqtrd 2485	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
280	279	mpteq2ia 4485	. . . . . . . . . . 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 2501	. . . . . . . . . 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 5037	. . . . . . . . 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 5332	. . . . . . . . . 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 6318	. . . . . . . . . . 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 2751	. . . . . . . . 9 |- dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
287	282, 286	syl6eq 2501	. . . . . . . 8 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
288		sumex 13754	. . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . 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 13762	. . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . 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 4485	. . . . . . . . . . . 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 2451	. . . . . . . . . . . 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 23385	. . . . . . . . . . 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 3436	. . . . . . . . . . . 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 22917	. . . . . . . . . 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 10876	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. NN -> n e. NN0 )
300	299	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
301		eqeq1 2455	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( m = 0 <-> n = 0 ) )
302		oveq2 6298	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( 1 / m ) = ( 1 / n ) )
303	301, 302	ifbieq2d 3906	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
304		ovex 6318	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / n ) e. _V
305	93, 304	ifex 3949	. . . . . . . . . . . . . . . . . . . 20 |- if ( n = 0 , 0 , ( 1 / n ) ) e. _V
306	303, 92, 305	fvmpt 5948	. . . . . . . . . . . . . . . . . . 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 10642	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. NN -> n =/= 0 )
309	308	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
310	309	neneqd 2629	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
311	310	iffalsed 3892	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
312	307, 311	eqtrd 2485	. . . . . . . . . . . . . . . . 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 6306	. . . . . . . . . . . . . . . 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 10617	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> n e. CC )
315	314	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
316	315, 309	recidd 10378	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
317	313, 316	eqtrd 2485	. . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . 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 10911	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( n - 1 ) e. NN0 )
320		expcl 12290	. . . . . . . . . . . . . . . 16 |- ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
321	53, 319, 320	syl2an 480	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
322	321	mulid2d 9661	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
323	318, 322	eqtrd 2485	. . . . . . . . . . . . 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 13769	. . . . . . . . . . . 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 11194	. . . . . . . . . . . . . . 15 |- NN = ( ZZ>= ` 1 )
326		1e0p1 11079	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
327	326	fveq2i 5868	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
328	325, 327	eqtri 2473	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` ( 0 + 1 ) )
329		oveq1 6297	. . . . . . . . . . . . . . 15 |- ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
330	329	oveq2d 6306	. . . . . . . . . . . . . 14 |- ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
331		1zzd 10968	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
332		0zd 10949	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
333	1, 328, 330, 331, 332, 321	isumshft 13897	. . . . . . . . . . . . 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 9882	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
335	50, 102, 334	sylancr 669	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
336	335	oveq2d 6306	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
337	336	sumeq2i 13765	. . . . . . . . . . . . 13 |- sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
338	333, 337	syl6eq 2501	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
339		geoisum 13933	. . . . . . . . . . . . 13 |- ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
340	53, 66, 339	syl2anc 667	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
341	324, 338, 340	3eqtrd 2489	. . . . . . . . . . 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 4485	. . . . . . . . . 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 2501	. . . . . . . . 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 2488	. . . . . . . 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 21428	. . . . . . . . . 10 |- ( (