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