logtayl

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0uz	\|- NN0 = ( ZZ>= ` 0 )
2		0zd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3		eqeq1	\|- ( k = n -> ( k = 0 <-> n = 0 ) )
4		oveq2	\|- ( k = n -> ( 1 / k ) = ( 1 / n ) )
5	3 4	ifbieq2d	\|- ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
6		oveq2	\|- ( k = n -> ( A ^ k ) = ( A ^ n ) )
7	5 6	oveq12d	\|- ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
8		eqid	\|- ( 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	\|- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
10	7 8 9	fvmpt	\|- ( 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	\|- ( ( ( 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	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
13		simpr	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
14		elnn0	\|- ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
15	13 14	sylib	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
16	15	ord	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
17	16	con1d	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
18	17	imp	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
19	18	nnrecred	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
20	19	recnd	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
21	12 20	ifclda	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
22		expcl	\|- ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
23	22	adantlr	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
24	21 23	mulcld	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
25		logtayllem	\|- ( ( 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	\|- ( ( 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	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
28		0cn	\|- 0 e. CC
29		eqid	\|- ( abs o. - ) = ( abs o. - )
30	29	cnmetdval	\|- ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
31	27 28 30	sylancl	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32		subid1	\|- ( A e. CC -> ( A - 0 ) = A )
33	32	adantr	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
34	33	fveq2d	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
35	31 34	eqtrd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
36		simpr	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
37	35 36	eqbrtrd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
38		cnxmet	\|- ( abs o. - ) e. ( *Met ` CC )
39		1xr	\|- 1 e. RR*
40		elbl3	\|- ( ( ( ( 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 ) )
41	38 39 40	mpanl12	\|- ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
42	28 27 41	sylancr	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
43	37 42	mpbird	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
44		tru	\|- T.
45		eqid	\|- ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
46		0cnd	\|- ( T. -> 0 e. CC )
47	39	a1i	\|- ( T. -> 1 e. RR* )
48		ax-1cn	\|- 1 e. CC
49		blssm	\|- ( ( ( abs o. - ) e. ( Met ` CC ) /\ 0 e. CC /\ 1 e. RR ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
50	38 28 39 49	mp3an	\|- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
51	50	sseli	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
52		subcl	\|- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
53	48 51 52	sylancr	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
54	51	abscld	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
55	29	cnmetdval	\|- ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
56	51 28 55	sylancl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
57	51	subid1d	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
58	57	fveq2d	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
59	56 58	eqtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
60		elbl3	\|- ( ( ( ( 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 ) )
61	38 39 60	mpanl12	\|- ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
62	28 51 61	sylancr	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
63	62	ibi	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
64	59 63	eqbrtrrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
65	54 64	gtned	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
66		abs1	\|- ( abs ` 1 ) = 1
67		fveq2	\|- ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
68	66 67	eqtr3id	\|- ( 1 = y -> 1 = ( abs ` y ) )
69	68	necon3i	\|- ( 1 =/= ( abs ` y ) -> 1 =/= y )
70	65 69	syl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
71		subeq0	\|- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
72	71	necon3bid	\|- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
73	48 51 72	sylancr	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
74	70 73	mpbird	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
75	53 74	logcld	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
76	75	negcld	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
77	76	adantl	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
78	77	fmpttd	\|- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
79	51	absge0d	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
80	54	rexrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
81		peano2re	\|- ( ( abs ` y ) e. RR -> ( ( abs ` y ) + 1 ) e. RR )
82	54 81	syl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) + 1 ) e. RR )
83	82	rehalfcld	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
84	83	rexrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
85		iccssxr	\|- ( 0 [,] +oo ) C_ RR*
86		eqeq1	\|- ( m = j -> ( m = 0 <-> j = 0 ) )
87		oveq2	\|- ( m = j -> ( 1 / m ) = ( 1 / j ) )
88	86 87	ifbieq2d	\|- ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
89		eqid	\|- ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) )
90		c0ex	\|- 0 e. _V
91		ovex	\|- ( 1 / j ) e. _V
92	90 91	ifex	\|- if ( j = 0 , 0 , ( 1 / j ) ) e. _V
93	88 89 92	fvmpt	\|- ( j e. NN0 -> ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
94	93	eqcomd	\|- ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
95	94	oveq1d	\|- ( 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 ) ) )
96	95	mpteq2ia	\|- ( 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 ) ) )
97	96	mpteq2i	\|- ( 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 ) ) ) )
98		0cnd	\|- ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
99		nn0cn	\|- ( m e. NN0 -> m e. CC )
100	99	adantl	\|- ( ( T. /\ m e. NN0 ) -> m e. CC )
101		neqne	\|- ( -. m = 0 -> m =/= 0 )
102		reccl	\|- ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
103	100 101 102	syl2an	\|- ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
104	98 103	ifclda	\|- ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
105	104	fmpttd	\|- ( T. -> ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
106		recn	\|- ( r e. RR -> r e. CC )
107		oveq1	\|- ( x = r -> ( x ^ j ) = ( r ^ j ) )
108	107	oveq2d	\|- ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
109	108	mpteq2dv	\|- ( 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 ) ) ) )
110		eqid	\|- ( 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 ) ) ) )
111		nn0ex	\|- NN0 e. _V
112	111	mptex	\|- ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
113	109 110 112	fvmpt	\|- ( 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 ) ) ) )
114	106 113	syl	\|- ( 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 ) ) ) )
115	114	eqcomd	\|- ( 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 ) )
116	115	seqeq3d	\|- ( 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 ) ) )
117	116	eleq1d	\|- ( 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 ~~> ) )
118	117	rabbiia	\|- { 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 ~~> }
119	118	supeq1i	\|- 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* , < )
120	97 105 119	radcnvcl	\|- ( 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 ) )
121	85 120	sselid	\|- ( T. -> sup ( { r e. RR \| seq 0 ( + , ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
122	44 121	mp1i	\|- ( 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* )
123		1re	\|- 1 e. RR
124		avglt1	\|- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
125	54 123 124	sylancl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
126	64 125	mpbid	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
127		0red	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
128	127 54 83 79 126	lelttrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
129	127 83 128	ltled	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
130	83 129	absidd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( ( ( abs ` y ) + 1 ) / 2 ) )
131	44 105	mp1i	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
132	83	recnd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
133		oveq1	\|- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
134	133	oveq2d	\|- ( 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 ) ) )
135	134	mpteq2dv	\|- ( 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 ) ) ) )
136	111	mptex	\|- ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
137	135 110 136	fvmpt	\|- ( ( ( ( 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 ) ) ) )
138	132 137	syl	\|- ( 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 ) ) ) )
139	138	seqeq3d	\|- ( 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 ) ) ) ) )
140		avglt2	\|- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
141	54 123 140	sylancl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
142	64 141	mpbid	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
143	130 142	eqbrtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
144		logtayllem	\|- ( ( ( ( ( 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 ~~> )
145	132 143 144	syl2anc	\|- ( 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 ~~> )
146	139 145	eqeltrd	\|- ( 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 ~~> )
147	97 131 119 132 146	radcnvle	\|- ( 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* , < ) )
148	130 147	eqbrtrrd	\|- ( 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* , < ) )
149	80 84 122 126 148	xrltletrd	\|- ( 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* , < ) )
150		0re	\|- 0 e. RR
151		elico2	\|- ( ( 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* , < ) ) ) )
152	150 122 151	sylancr	\|- ( 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* , < ) ) ) )
153	54 79 149 152	mpbir3and	\|- ( 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* , < ) ) )
154		absf	\|- abs : CC --> RR
155		ffn	\|- ( abs : CC --> RR -> abs Fn CC )
156		elpreima	\|- ( 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* , < ) ) ) ) )
157	154 155 156	mp2b	\|- ( 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* , < ) ) ) )
158	51 153 157	sylanbrc	\|- ( 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* , < ) ) ) )
159		cnvimass	\|- ( `' 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
160	154	fdmi	\|- dom abs = CC
161	159 160	sseqtri	\|- ( `' 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
162	161	sseli	\|- ( 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 )
163		oveq1	\|- ( x = y -> ( x ^ j ) = ( y ^ j ) )
164	163	oveq2d	\|- ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
165	164	mpteq2dv	\|- ( 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 ) ) ) )
166	111	mptex	\|- ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
167	165 110 166	fvmpt	\|- ( 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 ) ) ) )
168	167	adantr	\|- ( ( 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 ) ) ) )
169	168	fveq1d	\|- ( ( 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 ) )
170		eqeq1	\|- ( j = n -> ( j = 0 <-> n = 0 ) )
171		oveq2	\|- ( j = n -> ( 1 / j ) = ( 1 / n ) )
172	170 171	ifbieq2d	\|- ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
173		oveq2	\|- ( j = n -> ( y ^ j ) = ( y ^ n ) )
174	172 173	oveq12d	\|- ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
175		eqid	\|- ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) = ( j e. NN0 \|-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
176		ovex	\|- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
177	174 175 176	fvmpt	\|- ( 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 ) ) )
178	177	adantl	\|- ( ( 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 ) ) )
179	169 178	eqtr2d	\|- ( ( 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 ) )
180	179	sumeq2dv	\|- ( 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 ) )
181	162 180	syl	\|- ( 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 ) )
182	181	mpteq2ia	\|- ( 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 ) )
183		eqid	\|- ( `' 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* , < ) ) )
184		eqid	\|- 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 ) )
185	97 182 105 119 183 184	psercn	\|- ( 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 ) )
186		cncff	\|- ( ( 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 )
187	185 186	syl	\|- ( 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 )
188	187	fvmptelcdm	\|- ( ( 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 )
189	158 188	sylan2	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
190	189	fmpttd	\|- ( 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 )
191		cnelprrecn	\|- CC e. { RR , CC }
192	191	a1i	\|- ( T. -> CC e. { RR , CC } )
193	75	adantl	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
194		ovexd	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V )
195	29	cnmetdval	\|- ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
196	48 53 195	sylancr	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
197		nncan	\|- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
198	48 51 197	sylancr	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
199	198	fveq2d	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
200	196 199	eqtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
201	200 64	eqbrtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
202		elbl	\|- ( ( ( 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 ) ) )
203	38 48 39 202	mp3an	\|- ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
204	53 201 203	sylanbrc	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
205	204	adantl	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
206		neg1cn	\|- -u 1 e. CC
207	206	a1i	\|- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
208		eqid	\|- ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
209	208	dvlog2lem	\|- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
210	209	sseli	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
211	210	eldifad	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
212		eqid	\|- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
213	212	logdmn0	\|- ( x e. ( CC \ ( -oo (,] 0 ) ) -> x =/= 0 )
214	210 213	syl	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x =/= 0 )
215	211 214	logcld	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
216	215	adantl	\|- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
217		ovexd	\|- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
218		simpr	\|- ( ( T. /\ y e. CC ) -> y e. CC )
219	48 218 52	sylancr	\|- ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
220	206	a1i	\|- ( ( T. /\ y e. CC ) -> -u 1 e. CC )
221		1cnd	\|- ( ( T. /\ y e. CC ) -> 1 e. CC )
222		0cnd	\|- ( ( T. /\ y e. CC ) -> 0 e. CC )
223		1cnd	\|- ( T. -> 1 e. CC )
224	192 223	dvmptc	\|- ( T. -> ( CC _D ( y e. CC \|-> 1 ) ) = ( y e. CC \|-> 0 ) )
225	192	dvmptid	\|- ( T. -> ( CC _D ( y e. CC \|-> y ) ) = ( y e. CC \|-> 1 ) )
226	192 221 222 224 218 221 225	dvmptsub	\|- ( T. -> ( CC _D ( y e. CC \|-> ( 1 - y ) ) ) = ( y e. CC \|-> ( 0 - 1 ) ) )
227		df-neg	\|- -u 1 = ( 0 - 1 )
228	227	mpteq2i	\|- ( y e. CC \|-> -u 1 ) = ( y e. CC \|-> ( 0 - 1 ) )
229	226 228	eqtr4di	\|- ( T. -> ( CC _D ( y e. CC \|-> ( 1 - y ) ) ) = ( y e. CC \|-> -u 1 ) )
230	50	a1i	\|- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
231		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
232	231	cnfldtopon	\|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
233	232	toponrestid	\|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) \|`t CC )
234	231	cnfldtopn	\|- ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
235	234	blopn	\|- ( ( ( abs o. - ) e. ( Met ` CC ) /\ 0 e. CC /\ 1 e. RR ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) )
236	38 28 39 235	mp3an	\|- ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld )
237	236	a1i	\|- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` CCfld ) )
238	192 219 220 229 230 233 231 237	dvmptres	\|- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u 1 ) )
239		logf1o	\|- log : ( CC \ { 0 } ) -1-1-onto-> ran log
240		f1of	\|- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
241	239 240	ax-mp	\|- log : ( CC \ { 0 } ) --> ran log
242	212	logdmss	\|- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
243	209 242	sstri	\|- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
244		fssres	\|- ( ( 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 )
245	241 243 244	mp2an	\|- ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log
246	245	a1i	\|- ( T. -> ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
247	246	feqmptd	\|- ( T. -> ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
248		fvres	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
249	248	mpteq2ia	\|- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( log ` x ) )
250	247 249	eqtrdi	\|- ( T. -> ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( log ` x ) ) )
251	250	oveq2d	\|- ( T. -> ( CC _D ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( log ` x ) ) ) )
252	208	dvlog2	\|- ( CC _D ( log \|` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 / x ) )
253	251 252	eqtr3di	\|- ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 / x ) ) )
254		fveq2	\|- ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
255		oveq2	\|- ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
256	192 192 205 207 216 217 238 253 254 255	dvmptco	\|- ( 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 ) ) )
257	192 193 194 256	dvmptneg	\|- ( 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 ) ) )
258	53 74	reccld	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
259		mulcom	\|- ( ( ( 1 / ( 1 - y ) ) e. CC /\ -u 1 e. CC ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
260	258 206 259	sylancl	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
261	258	mulm1d	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
262	260 261	eqtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
263	262	negeqd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
264	258	negnegd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
265	263 264	eqtrd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
266	265	mpteq2ia	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 / ( 1 - y ) ) )
267	257 266	eqtrdi	\|- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 / ( 1 - y ) ) ) )
268	267	dmeqd	\|- ( 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 ) ) ) )
269		dmmptg	\|- ( 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 ) )
270		ovexd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. _V )
271	269 270	mprg	\|- dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
272	268 271	eqtrdi	\|- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
273		sumex	\|- sum_ n e. NN ( ( n x. ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V
274	273	a1i	\|- ( ( 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 )
275		fveq2	\|- ( 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 ) )
276	275	cbvsumv	\|- 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 )
277	181 276	eqtrdi	\|- ( 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 ) )
278	277	mpteq2ia	\|- ( 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 ) )
279		eqid	\|- ( 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 ) )
280	97 278 105 119 183 184 279	pserdv2	\|- ( 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 ) ) ) ) )
281	158	ssriv	\|- ( 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* , < ) ) )
282	281	a1i	\|- ( 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* , < ) ) ) )
283	192 188 274 280 282 233 231 237	dvmptres	\|- ( 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 ) ) ) ) )
284		nnnn0	\|- ( n e. NN -> n e. NN0 )
285	284	adantl	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
286		eqeq1	\|- ( m = n -> ( m = 0 <-> n = 0 ) )
287		oveq2	\|- ( m = n -> ( 1 / m ) = ( 1 / n ) )
288	286 287	ifbieq2d	\|- ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
289		ovex	\|- ( 1 / n ) e. _V
290	90 289	ifex	\|- if ( n = 0 , 0 , ( 1 / n ) ) e. _V
291	288 89 290	fvmpt	\|- ( n e. NN0 -> ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
292	285 291	syl	\|- ( ( 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 ) ) )
293		nnne0	\|- ( n e. NN -> n =/= 0 )
294	293	adantl	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
295	294	neneqd	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
296	295	iffalsed	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
297	292 296	eqtrd	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = ( 1 / n ) )
298	297	oveq2d	\|- ( ( 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 ) ) )
299		nncn	\|- ( n e. NN -> n e. CC )
300	299	adantl	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
301	300 294	recidd	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
302	298 301	eqtrd	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 \|-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = 1 )
303	302	oveq1d	\|- ( ( 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 ) ) ) )
304		nnm1nn0	\|- ( n e. NN -> ( n - 1 ) e. NN0 )
305		expcl	\|- ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
306	51 304 305	syl2an	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
307	306	mullidd	\|- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
308	303 307	eqtrd	\|- ( ( 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 ) ) )
309	308	sumeq2dv	\|- ( 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 ) ) )
310		nnuz	\|- NN = ( ZZ>= ` 1 )
311		1e0p1	\|- 1 = ( 0 + 1 )
312	311	fveq2i	\|- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
313	310 312	eqtri	\|- NN = ( ZZ>= ` ( 0 + 1 ) )
314		oveq1	\|- ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
315	314	oveq2d	\|- ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
316		1zzd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
317		0zd	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
318	1 313 315 316 317 306	isumshft	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) )
319		pncan2	\|- ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
320	48 99 319	sylancr	\|- ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
321	320	oveq2d	\|- ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
322	321	sumeq2i	\|- sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
323	318 322	eqtrdi	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
324		geoisum	\|- ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
325	51 64 324	syl2anc	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
326	309 323 325	3eqtrd	\|- ( 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 ) ) )
327	326	mpteq2ia	\|- ( 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 ) ) )
328	283 327	eqtrdi	\|- ( 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 ) ) ) )
329	267 328	eqtr4d	\|- ( 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 ) ) ) ) )
330		1rp	\|- 1 e. RR+
331		blcntr	\|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR+ ) -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
332	38 28 330 331	mp3an	\|- 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 )
333	332	a1i	\|- ( T. -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
334		oveq2	\|- ( y = 0 -> ( 1 - y ) = ( 1 - 0 ) )
335		1m0e1	\|- ( 1 - 0 ) = 1
336	334 335	eqtrdi	\|- ( y = 0 -> ( 1 - y ) = 1 )
337	336	fveq2d	\|- ( y = 0 -> ( log ` ( 1 - y ) ) = ( log ` 1 ) )
338		log1	\|- ( log ` 1 ) = 0
339	337 338	eqtrdi	\|- ( y = 0 -> ( log ` ( 1 - y ) ) = 0 )
340	339	negeqd	\|- ( y = 0 -> -u ( log ` ( 1 - y ) ) = -u 0 )
341		neg0	\|- -u 0 = 0
342	340 341	eqtrdi	\|- ( y = 0 -> -u ( log ` ( 1 - y ) ) = 0 )
343		eqid	\|- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) )
344	342 343 90	fvmpt	\|- ( 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
345	332 344	mp1i	\|- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
346		oveq1	\|- ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( 0 x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
347	346	eqeq1d	\|- ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 0 x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
348		oveq1	\|- ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
349	348	eqeq1d	\|- ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( ( 1 / n ) x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
350		simpll	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y = 0 )
351	350 28	eqeltrdi	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y e. CC )
352		simplr	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> n e. NN0 )
353	351 352	expcld	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( y ^ n ) e. CC )
354	353	mul02d	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( 0 x. ( y ^ n ) ) = 0 )
355		simpll	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> y = 0 )
356	355	oveq1d	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = ( 0 ^ n ) )
357		simpr	\|- ( ( y = 0 /\ n e. NN0 ) -> n e. NN0 )
358	357 14	sylib	\|- ( ( y = 0 /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
359	358	ord	\|- ( ( y = 0 /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
360	359	con1d	\|- ( ( y = 0 /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
361	360	imp	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
362	361	0expd	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 0 ^ n ) = 0 )
363	356 362	eqtrd	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = 0 )
364	363	oveq2d	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( ( 1 / n ) x. 0 ) )
365	361	nnrecred	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
366	365	recnd	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
367	366	mul01d	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. 0 ) = 0 )
368	364 367	eqtrd	\|- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = 0 )
369	347 349 354 368	ifbothda	\|- ( ( y = 0 /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
370	369	sumeq2dv	\|- ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 0 )
371	1	eqimssi	\|- NN0 C_ ( ZZ>= ` 0 )
372	371	orci	\|- ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin )
373		sumz	\|- ( ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin ) -> sum_ n e. NN0 0 = 0 )
374	372 373	ax-mp	\|- sum_ n e. NN0 0 = 0
375	370 374	eqtrdi	\|- ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
376		eqid	\|- ( 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 ) ) )
377	375 376 90	fvmpt	\|- ( 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) = 0 )
378	332 377	mp1i	\|- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) = 0 )
379	345 378	eqtr4d	\|- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) )
380	45 46 47 78 190 272 329 333 379	dv11cn	\|- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) )
381	380	fveq1d	\|- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` A ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) )
382	44 381	mp1i	\|- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` A ) = ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) )
383		oveq2	\|- ( y = A -> ( 1 - y ) = ( 1 - A ) )
384	383	fveq2d	\|- ( y = A -> ( log ` ( 1 - y ) ) = ( log ` ( 1 - A ) ) )
385	384	negeqd	\|- ( y = A -> -u ( log ` ( 1 - y ) ) = -u ( log ` ( 1 - A ) ) )
386		negex	\|- -u ( log ` ( 1 - A ) ) e. _V
387	385 343 386	fvmpt	\|- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> -u ( log ` ( 1 - y ) ) ) ` A ) = -u ( log ` ( 1 - A ) ) )
388		oveq1	\|- ( y = A -> ( y ^ n ) = ( A ^ n ) )
389	388	oveq2d	\|- ( y = A -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
390	389	sumeq2sdv	\|- ( y = A -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
391		sumex	\|- sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
392	390 376 391	fvmpt	\|- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) \|-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` A ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
393	382 387 392	3eqtr3d	\|- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
394	43 393	syl	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
395	26 394	breqtrrd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> -u ( log ` ( 1 - A ) ) )
396		seqex	\|- seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V
397	396	a1i	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V )
398		seqex	\|- seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) e. _V
399	398	a1i	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) e. _V )
400		1zzd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ZZ )
401		elnnuz	\|- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
402		fvres	\|- ( n e. ( ZZ>= ` 1 ) -> ( ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) ` n ) = ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) )
403	401 402	sylbi	\|- ( n e. NN -> ( ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) ` n ) = ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) )
404	403	eqcomd	\|- ( n e. NN -> ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) = ( ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) ` n ) )
405		addlid	\|- ( n e. CC -> ( 0 + n ) = n )
406	405	adantl	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. CC ) -> ( 0 + n ) = n )
407		0cnd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. CC )
408		1eluzge0	\|- 1 e. ( ZZ>= ` 0 )
409	408	a1i	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ( ZZ>= ` 0 ) )
410		0cnd	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ k = 0 ) -> 0 e. CC )
411		nn0cn	\|- ( k e. NN0 -> k e. CC )
412	411	adantl	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> k e. CC )
413		neqne	\|- ( -. k = 0 -> k =/= 0 )
414		reccl	\|- ( ( k e. CC /\ k =/= 0 ) -> ( 1 / k ) e. CC )
415	412 413 414	syl2an	\|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ -. k = 0 ) -> ( 1 / k ) e. CC )
416	410 415	ifclda	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> if ( k = 0 , 0 , ( 1 / k ) ) e. CC )
417		expcl	\|- ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
418	417	adantlr	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
419	416 418	mulcld	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. CC )
420	419	fmpttd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) : NN0 --> CC )
421		1nn0	\|- 1 e. NN0
422		ffvelcdm	\|- ( ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) : NN0 --> CC /\ 1 e. NN0 ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 1 ) e. CC )
423	420 421 422	sylancl	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 1 ) e. CC )
424		elfz1eq	\|- ( n e. ( 0 ... 0 ) -> n = 0 )
425		1m1e0	\|- ( 1 - 1 ) = 0
426	425	oveq2i	\|- ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
427	424 426	eleq2s	\|- ( n e. ( 0 ... ( 1 - 1 ) ) -> n = 0 )
428	427	fveq2d	\|- ( n e. ( 0 ... ( 1 - 1 ) ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) )
429		0nn0	\|- 0 e. NN0
430		iftrue	\|- ( k = 0 -> if ( k = 0 , 0 , ( 1 / k ) ) = 0 )
431		oveq2	\|- ( k = 0 -> ( A ^ k ) = ( A ^ 0 ) )
432	430 431	oveq12d	\|- ( k = 0 -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( 0 x. ( A ^ 0 ) ) )
433		ovex	\|- ( 0 x. ( A ^ 0 ) ) e. _V
434	432 8 433	fvmpt	\|- ( 0 e. NN0 -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) ) )
435	429 434	ax-mp	\|- ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) )
436		expcl	\|- ( ( A e. CC /\ 0 e. NN0 ) -> ( A ^ 0 ) e. CC )
437	27 429 436	sylancl	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 0 ) e. CC )
438	437	mul02d	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 0 x. ( A ^ 0 ) ) = 0 )
439	435 438	eqtrid	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = 0 )
440	428 439	sylan9eqr	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. ( 0 ... ( 1 - 1 ) ) ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = 0 )
441	406 407 409 423 440	seqid	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) )
442	293	adantl	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n =/= 0 )
443	442	neneqd	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> -. n = 0 )
444	443	iffalsed	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
445	444	oveq1d	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( 1 / n ) x. ( A ^ n ) ) )
446	284 23	sylan2	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( A ^ n ) e. CC )
447	299	adantl	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n e. CC )
448	446 447 442	divrec2d	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( A ^ n ) / n ) = ( ( 1 / n ) x. ( A ^ n ) ) )
449	445 448	eqtr4d	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( A ^ n ) / n ) )
450	284 11	sylan2	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
451		id	\|- ( k = n -> k = n )
452	6 451	oveq12d	\|- ( k = n -> ( ( A ^ k ) / k ) = ( ( A ^ n ) / n ) )
453		eqid	\|- ( k e. NN \|-> ( ( A ^ k ) / k ) ) = ( k e. NN \|-> ( ( A ^ k ) / k ) )
454		ovex	\|- ( ( A ^ n ) / n ) e. _V
455	452 453 454	fvmpt	\|- ( n e. NN -> ( ( k e. NN \|-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
456	455	adantl	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN \|-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
457	449 450 456	3eqtr4d	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN \|-> ( ( A ^ k ) / k ) ) ` n ) )
458	401 457	sylan2br	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. ( ZZ>= ` 1 ) ) -> ( ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( ( k e. NN \|-> ( ( A ^ k ) / k ) ) ` n ) )
459	400 458	seqfeq	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) = seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) )
460	441 459	eqtrd	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) = seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) )
461	460	fveq1d	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) \|` ( ZZ>= ` 1 ) ) ` n ) = ( seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) ` n ) )
462	404 461	sylan9eqr	\|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ` n ) = ( seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) ` n ) )
463	310 397 399 400 462	climeq	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( k e. NN0 \|-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> -u ( log ` ( 1 - A ) ) <-> seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) ) )
464	395 463	mpbid	\|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN \|-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )

Metamath Proof Explorer

Theorem logtayl

Proof