Theorem logtayl 24406

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

Assertion

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

Distinct variable group:   A, k

Proof of Theorem logtayl

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

Step	Hyp	Ref	Expression
1		nn0uz 11722	. . . 4 |- NN0 = ( ZZ>= ` 0 )
2		0zd 11389	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. ZZ )
3		eqeq1 2626	. . . . . . . 8 |- ( k = n -> ( k = 0 <-> n = 0 ) )
4		oveq2 6658	. . . . . . . 8 |- ( k = n -> ( 1 / k ) = ( 1 / n ) )
5	3, 4	ifbieq2d 4111	. . . . . . 7 |- ( k = n -> if ( k = 0 , 0 , ( 1 / k ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
6		oveq2 6658	. . . . . . 7 |- ( k = n -> ( A ^ k ) = ( A ^ n ) )
7	5, 6	oveq12d 6668	. . . . . 6 |- ( k = n -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
8		eqid 2622	. . . . . 6 |- ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) = ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
9		ovex 6678	. . . . . 6 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
10	7, 8, 9	fvmpt 6282	. . . . 5 |- ( n e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
11	10	adantl 482	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
12		0cnd 10033	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ n = 0 ) -> 0 e. CC )
13		simpr 477	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
14		elnn0 11294	. . . . . . . . . . . 12 |- ( n e. NN0 <-> ( n e. NN \/ n = 0 ) )
15	13, 14	sylib 208	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
16	15	ord 392	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
17	16	con1d 139	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
18	17	imp 445	. . . . . . . 8 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
19	18	nnrecred 11066	. . . . . . 7 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
20	19	recnd 10068	. . . . . 6 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
21	12, 20	ifclda 4120	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> if ( n = 0 , 0 , ( 1 / n ) ) e. CC )
22		expcl 12878	. . . . . 6 |- ( ( A e. CC /\ n e. NN0 ) -> ( A ^ n ) e. CC )
23	22	adantlr 751	. . . . 5 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ n ) e. CC )
24	21, 23	mulcld 10060	. . . 4 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. CC )
25		logtayllem 24405	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. dom ~~> )
26	1, 2, 11, 24, 25	isumclim2 14489	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
27		simpl 473	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
28		0cn 10032	. . . . . . . 8 |- 0 e. CC
29		eqid 2622	. . . . . . . . 9 |- ( abs o. - ) = ( abs o. - )
30	29	cnmetdval 22574	. . . . . . . 8 |- ( ( A e. CC /\ 0 e. CC ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
31	27, 28, 30	sylancl 694	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` ( A - 0 ) ) )
32		subid1 10301	. . . . . . . . 9 |- ( A e. CC -> ( A - 0 ) = A )
33	32	adantr 481	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A - 0 ) = A )
34	33	fveq2d 6195	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A - 0 ) ) = ( abs ` A ) )
35	31, 34	eqtrd 2656	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) = ( abs ` A ) )
36		simpr 477	. . . . . 6 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
37	35, 36	eqbrtrd 4675	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ( abs o. - ) 0 ) < 1 )
38		cnxmet 22576	. . . . . . 7 |- ( abs o. - ) e. ( *Met ` CC )
39		1rp 11836	. . . . . . . 8 |- 1 e. RR+
40		rpxr 11840	. . . . . . . 8 |- ( 1 e. RR+ -> 1 e. RR* )
41	39, 40	ax-mp 5	. . . . . . 7 |- 1 e. RR*
42		elbl3 22197	. . . . . . 7 |- ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ A e. CC ) ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
43	38, 41, 42	mpanl12 718	. . . . . 6 |- ( ( 0 e. CC /\ A e. CC ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
44	28, 27, 43	sylancr 695	. . . . 5 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( A ( abs o. - ) 0 ) < 1 ) )
45	37, 44	mpbird 247	. . . 4 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
46		tru 1487	. . . . . 6 |- T.
47		eqid 2622	. . . . . . . 8 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
48		0cnd 10033	. . . . . . . 8 |- ( T. -> 0 e. CC )
49	41	a1i 11	. . . . . . . 8 |- ( T. -> 1 e. RR* )
50		ax-1cn 9994	. . . . . . . . . . . . 13 |- 1 e. CC
51		blssm 22223	. . . . . . . . . . . . . . 15 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
52	38, 28, 41, 51	mp3an 1424	. . . . . . . . . . . . . 14 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
53	52	sseli 3599	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. CC )
54		subcl 10280	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - y ) e. CC )
55	50, 53, 54	sylancr 695	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. CC )
56	53	abscld 14175	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR )
57	29	cnmetdval 22574	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ 0 e. CC ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
58	53, 28, 57	sylancl 694	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` ( y - 0 ) ) )
59	53	subid1d 10381	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y - 0 ) = y )
60	59	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( y - 0 ) ) = ( abs ` y ) )
61	58, 60	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) = ( abs ` y ) )
62		elbl3 22197	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ y e. CC ) ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
63	38, 41, 62	mpanl12 718	. . . . . . . . . . . . . . . . . 18 |- ( ( 0 e. CC /\ y e. CC ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
64	28, 53, 63	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) 0 ) < 1 ) )
65	64	ibi 256	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( y ( abs o. - ) 0 ) < 1 )
66	61, 65	eqbrtrrd 4677	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < 1 )
67	56, 66	gtned 10172	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= ( abs ` y ) )
68		abs1 14037	. . . . . . . . . . . . . . . 16 |- ( abs ` 1 ) = 1
69		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( 1 = y -> ( abs ` 1 ) = ( abs ` y ) )
70	68, 69	syl5eqr 2670	. . . . . . . . . . . . . . 15 |- ( 1 = y -> 1 = ( abs ` y ) )
71	70	necon3i 2826	. . . . . . . . . . . . . 14 |- ( 1 =/= ( abs ` y ) -> 1 =/= y )
72	67, 71	syl 17	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 =/= y )
73		subeq0 10307	. . . . . . . . . . . . . . 15 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) = 0 <-> 1 = y ) )
74	73	necon3bid 2838	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ y e. CC ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
75	50, 53, 74	sylancr 695	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 - y ) =/= 0 <-> 1 =/= y ) )
76	72, 75	mpbird 247	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) =/= 0 )
77	55, 76	logcld 24317	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` ( 1 - y ) ) e. CC )
78	77	negcld 10379	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - y ) ) e. CC )
79	78	adantl 482	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u ( log ` ( 1 - y ) ) e. CC )
80		eqid 2622	. . . . . . . . 9 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) )
81	79, 80	fmptd 6385	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
82	53	absge0d 14183	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( abs ` y ) )
83	56	rexrd 10089	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. RR* )
84		peano2re 10209	. . . . . . . . . . . . . . . 16 |- ( ( abs ` y ) e. RR -> ( ( abs ` y ) + 1 ) e. RR )
85	56, 84	syl 17	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) + 1 ) e. RR )
86	85	rehalfcld 11279	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR )
87	86	rexrd 10089	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. RR* )
88		iccssxr 12256	. . . . . . . . . . . . . . 15 |- ( 0 [,] +oo ) C_ RR*
89		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( m = 0 <-> j = 0 ) )
90		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = j -> ( 1 / m ) = ( 1 / j ) )
91	89, 90	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = j -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( j = 0 , 0 , ( 1 / j ) ) )
92		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) = ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) )
93		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
94		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 1 / j ) e. _V
95	93, 94	ifex 4156	. . . . . . . . . . . . . . . . . . . . 21 |- if ( j = 0 , 0 , ( 1 / j ) ) e. _V
96	91, 92, 95	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) = if ( j = 0 , 0 , ( 1 / j ) ) )
97	96	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 -> if ( j = 0 , 0 , ( 1 / j ) ) = ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) )
98	97	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN0 -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) )
99	98	mpteq2ia 4740	. . . . . . . . . . . . . . . . 17 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) )
100	99	mpteq2i 4741	. . . . . . . . . . . . . . . 16 |- ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) = ( x e. CC |-> ( j e. NN0 |-> ( ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` j ) x. ( x ^ j ) ) ) )
101		0cnd 10033	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ m = 0 ) -> 0 e. CC )
102		nn0cn 11302	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN0 -> m e. CC )
103	102	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ m e. NN0 ) -> m e. CC )
104		df-ne 2795	. . . . . . . . . . . . . . . . . . . 20 |- ( m =/= 0 <-> -. m = 0 )
105	104	biimpri 218	. . . . . . . . . . . . . . . . . . 19 |- ( -. m = 0 -> m =/= 0 )
106		reccl 10692	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
107	103, 105, 106	syl2an 494	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ m e. NN0 ) /\ -. m = 0 ) -> ( 1 / m ) e. CC )
108	101, 107	ifclda 4120	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ m e. NN0 ) -> if ( m = 0 , 0 , ( 1 / m ) ) e. CC )
109	108, 92	fmptd 6385	. . . . . . . . . . . . . . . 16 |- ( T. -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
110		recn 10026	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. RR -> r e. CC )
111		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = r -> ( x ^ j ) = ( r ^ j ) )
112	111	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = r -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) )
113	112	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = r -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
114		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) = ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) )
115		nn0ex 11298	. . . . . . . . . . . . . . . . . . . . . . . 24 |- NN0 e. _V
116	115	mptex 6486	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) e. _V
117	113, 114, 116	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . 22 |- ( r e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
118	110, 117	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( r e. RR -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) )
119	118	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20 |- ( r e. RR -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) = ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) )
120	119	seqeq3d 12809	. . . . . . . . . . . . . . . . . . 19 |- ( r e. RR -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) = seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) )
121	120	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( r e. RR -> ( seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> <-> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> ) )
122	121	rabbiia 3185	. . . . . . . . . . . . . . . . 17 |- { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } = { r e. RR | seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> }
123	122	supeq1i 8353	. . . . . . . . . . . . . . . 16 |- sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
124	100, 109, 123	radcnvcl 24171	. . . . . . . . . . . . . . 15 |- ( T. -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. ( 0 [,] +oo ) )
125	88, 124	sseldi 3601	. . . . . . . . . . . . . 14 |- ( T. -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
126	46, 125	mp1i 13	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* )
127		1re 10039	. . . . . . . . . . . . . . 15 |- 1 e. RR
128		avglt1 11270	. . . . . . . . . . . . . . 15 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
129	56, 127, 128	sylancl 694	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) ) )
130	66, 129	mpbid 222	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < ( ( ( abs ` y ) + 1 ) / 2 ) )
131		0red 10041	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. RR )
132	131, 56, 86, 82, 130	lelttrd 10195	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 < ( ( ( abs ` y ) + 1 ) / 2 ) )
133	131, 86, 132	ltled 10185	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 <_ ( ( ( abs ` y ) + 1 ) / 2 ) )
134	86, 133	absidd 14161	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( ( ( abs ` y ) + 1 ) / 2 ) )
135	46, 109	mp1i 13	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) : NN0 --> CC )
136	86	recnd 10068	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) e. CC )
137		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( x ^ j ) = ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) )
138	137	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) )
139	138	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( ( ( abs ` y ) + 1 ) / 2 ) -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
140	115	mptex 6486	. . . . . . . . . . . . . . . . . . 19 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) e. _V
141	139, 114, 140	fvmpt 6282	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( abs ` y ) + 1 ) / 2 ) e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
142	136, 141	syl 17	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) )
143	142	seqeq3d 12809	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) ) = seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) )
144		avglt2 11271	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( abs ` y ) e. RR /\ 1 e. RR ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
145	56, 127, 144	sylancl 694	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) < 1 <-> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 ) )
146	66, 145	mpbid 222	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) < 1 )
147	134, 146	eqbrtrd 4675	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 )
148		logtayllem 24405	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( abs ` y ) + 1 ) / 2 ) e. CC /\ ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) < 1 ) -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) e. dom ~~> )
149	136, 147, 148	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( ( ( ( abs ` y ) + 1 ) / 2 ) ^ j ) ) ) ) e. dom ~~> )
150	143, 149	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> seq 0 ( + , ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` ( ( ( abs ` y ) + 1 ) / 2 ) ) ) e. dom ~~> )
151	100, 135, 123, 136, 150	radcnvle 24174	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( ( ( abs ` y ) + 1 ) / 2 ) ) <_ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
152	134, 151	eqbrtrrd 4677	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( ( abs ` y ) + 1 ) / 2 ) <_ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
153	83, 87, 126, 130, 152	xrltletrd 11992	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) )
154		0re 10040	. . . . . . . . . . . . 13 |- 0 e. RR
155		elico2 12237	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR* ) -> ( ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
156	154, 126, 155	sylancr 695	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) <-> ( ( abs ` y ) e. RR /\ 0 <_ ( abs ` y ) /\ ( abs ` y ) < sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
157	56, 82, 153, 156	mpbir3and 1245	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
158		absf 14077	. . . . . . . . . . . 12 |- abs : CC --> RR
159		ffn 6045	. . . . . . . . . . . 12 |- ( abs : CC --> RR -> abs Fn CC )
160		elpreima 6337	. . . . . . . . . . . 12 |- ( abs Fn CC -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) )
161	158, 159, 160	mp2b 10	. . . . . . . . . . 11 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) <-> ( y e. CC /\ ( abs ` y ) e. ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
162	53, 157, 161	sylanbrc 698	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
163		cnvimass 5485	. . . . . . . . . . . . . . . . . 18 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) C_ dom abs
164	158	fdmi 6052	. . . . . . . . . . . . . . . . . 18 |- dom abs = CC
165	163, 164	sseqtri 3637	. . . . . . . . . . . . . . . . 17 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) C_ CC
166	165	sseli 3599	. . . . . . . . . . . . . . . 16 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> y e. CC )
167		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x ^ j ) = ( y ^ j ) )
168	167	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) = ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
169	168	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
170	115	mptex 6486	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) e. _V
171	169, 114, 170	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
172	171	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) )
173	172	fveq1d 6193	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) )
174		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( j = 0 <-> n = 0 ) )
175		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = n -> ( 1 / j ) = ( 1 / n ) )
176	174, 175	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> if ( j = 0 , 0 , ( 1 / j ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
177		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = n -> ( y ^ j ) = ( y ^ n ) )
178	176, 177	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 |- ( j = n -> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
179		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) = ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) )
180		ovex 6678	. . . . . . . . . . . . . . . . . . . 20 |- ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. _V
181	178, 179, 180	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN0 -> ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
182	181	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC /\ n e. NN0 ) -> ( ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( y ^ j ) ) ) ` n ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
183	173, 182	eqtr2d 2657	. . . . . . . . . . . . . . . . 17 |- ( ( y e. CC /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
184	183	sumeq2dv 14433	. . . . . . . . . . . . . . . 16 |- ( y e. CC -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
185	166, 184	syl 17	. . . . . . . . . . . . . . 15 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
186	185	mpteq2ia 4740	. . . . . . . . . . . . . 14 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) )
187		eqid 2622	. . . . . . . . . . . . . 14 |- ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) = ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
188		eqid 2622	. . . . . . . . . . . . . 14 |- if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) = if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) )
189	100, 186, 109, 123, 187, 188	psercn 24180	. . . . . . . . . . . . 13 |- ( T. -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) )
190		cncff 22696	. . . . . . . . . . . . 13 |- ( ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) e. ( ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -cn-> CC ) -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
191	189, 190	syl 17	. . . . . . . . . . . 12 |- ( T. -> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
192		eqid 2622	. . . . . . . . . . . . 13 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
193	192	fmpt 6381	. . . . . . . . . . . 12 |- ( A. y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC <-> ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) --> CC )
194	191, 193	sylibr 224	. . . . . . . . . . 11 |- ( T. -> A. y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
195	194	r19.21bi 2932	. . . . . . . . . 10 |- ( ( T. /\ y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
196	162, 195	sylan2 491	. . . . . . . . 9 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) e. CC )
197		eqid 2622	. . . . . . . . 9 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
198	196, 197	fmptd 6385	. . . . . . . 8 |- ( T. -> ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) : ( 0 ( ball ` ( abs o. - ) ) 1 ) --> CC )
199		cnelprrecn 10029	. . . . . . . . . . . . 13 |- CC e. { RR , CC }
200	199	a1i 11	. . . . . . . . . . . 12 |- ( T. -> CC e. { RR , CC } )
201	77	adantl 482	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` ( 1 - y ) ) e. CC )
202		ovexd 6680	. . . . . . . . . . . 12 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) e. _V )
203	29	cnmetdval 22574	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ ( 1 - y ) e. CC ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
204	50, 55, 203	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` ( 1 - ( 1 - y ) ) ) )
205		nncan 10310	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. CC /\ y e. CC ) -> ( 1 - ( 1 - y ) ) = y )
206	50, 53, 205	sylancr 695	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - ( 1 - y ) ) = y )
207	206	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( abs ` ( 1 - ( 1 - y ) ) ) = ( abs ` y ) )
208	204, 207	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) = ( abs ` y ) )
209	208, 66	eqbrtrd 4675	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 ( abs o. - ) ( 1 - y ) ) < 1 )
210		elbl 22193	. . . . . . . . . . . . . . . 16 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. CC /\ 1 e. RR* ) -> ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) ) )
211	38, 50, 41, 210	mp3an 1424	. . . . . . . . . . . . . . 15 |- ( ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) <-> ( ( 1 - y ) e. CC /\ ( 1 ( abs o. - ) ( 1 - y ) ) < 1 ) )
212	55, 209, 211	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
213	212	adantl 482	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 - y ) e. ( 1 ( ball ` ( abs o. - ) ) 1 ) )
214		neg1cn 11124	. . . . . . . . . . . . . 14 |- -u 1 e. CC
215	214	a1i 11	. . . . . . . . . . . . 13 |- ( ( T. /\ y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> -u 1 e. CC )
216		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) = ( 1 ( ball ` ( abs o. - ) ) 1 )
217	216	dvlog2lem 24398	. . . . . . . . . . . . . . . . 17 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ ( -oo (,] 0 ) )
218	217	sseli 3599	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. ( CC \ ( -oo (,] 0 ) ) )
219	218	eldifad 3586	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x e. CC )
220		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
221	220	logdmn0 24386	. . . . . . . . . . . . . . . 16 |- ( x e. ( CC \ ( -oo (,] 0 ) ) -> x =/= 0 )
222	218, 221	syl 17	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> x =/= 0 )
223	219, 222	logcld 24317	. . . . . . . . . . . . . 14 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( log ` x ) e. CC )
224	223	adantl 482	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( log ` x ) e. CC )
225		ovexd 6680	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) ) -> ( 1 / x ) e. _V )
226		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( T. /\ y e. CC ) -> y e. CC )
227	50, 226, 54	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> ( 1 - y ) e. CC )
228	214	a1i 11	. . . . . . . . . . . . . 14 |- ( ( T. /\ y e. CC ) -> -u 1 e. CC )
229		1cnd 10056	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 1 e. CC )
230		0cnd 10033	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ y e. CC ) -> 0 e. CC )
231		1cnd 10056	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. CC )
232	200, 231	dvmptc 23721	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> 1 ) ) = ( y e. CC |-> 0 ) )
233	200	dvmptid 23720	. . . . . . . . . . . . . . . 16 |- ( T. -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
234	200, 229, 230, 232, 226, 229, 233	dvmptsub 23730	. . . . . . . . . . . . . . 15 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> ( 0 - 1 ) ) )
235		df-neg 10269	. . . . . . . . . . . . . . . 16 |- -u 1 = ( 0 - 1 )
236	235	mpteq2i 4741	. . . . . . . . . . . . . . 15 |- ( y e. CC |-> -u 1 ) = ( y e. CC |-> ( 0 - 1 ) )
237	234, 236	syl6eqr 2674	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( y e. CC |-> ( 1 - y ) ) ) = ( y e. CC |-> -u 1 ) )
238	52	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
239		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
240	239	cnfldtop 22587	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) e. Top
241	239	cnfldtopon 22586	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
242	241	toponunii 20721	. . . . . . . . . . . . . . . . 17 |- CC = U. ( TopOpen ` ℂfld )
243	242	restid 16094	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
244	240, 243	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
245	244	eqcomi 2631	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
246	239	cnfldtopn 22585	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
247	246	blopn 22305	. . . . . . . . . . . . . . . 16 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
248	38, 28, 41, 247	mp3an 1424	. . . . . . . . . . . . . . 15 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld )
249	248	a1i 11	. . . . . . . . . . . . . 14 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) e. ( TopOpen ` ℂfld ) )
250	200, 227, 228, 237, 238, 245, 239, 249	dvmptres 23726	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 - y ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u 1 ) )
251	216	dvlog2 24399	. . . . . . . . . . . . . 14 |- ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) )
252		logf1o 24311	. . . . . . . . . . . . . . . . . . . 20 |- log : ( CC \ { 0 } ) -1-1-onto-> ran log
253		f1of 6137	. . . . . . . . . . . . . . . . . . . 20 |- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
254	252, 253	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- log : ( CC \ { 0 } ) --> ran log
255	220	logdmss 24388	. . . . . . . . . . . . . . . . . . . 20 |- ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } )
256	217, 255	sstri 3612	. . . . . . . . . . . . . . . . . . 19 |- ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } )
257		fssres 6070	. . . . . . . . . . . . . . . . . . 19 |- ( ( log : ( CC \ { 0 } ) --> ran log /\ ( 1 ( ball ` ( abs o. - ) ) 1 ) C_ ( CC \ { 0 } ) ) -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
258	254, 256, 257	mp2an 708	. . . . . . . . . . . . . . . . . 18 |- ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log
259	258	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) : ( 1 ( ball ` ( abs o. - ) ) 1 ) --> ran log )
260	259	feqmptd 6249	. . . . . . . . . . . . . . . 16 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) )
261		fvres 6207	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) -> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) = ( log ` x ) )
262	261	mpteq2ia 4740	. . . . . . . . . . . . . . . 16 |- ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ` x ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) )
263	260, 262	syl6eq 2672	. . . . . . . . . . . . . . 15 |- ( T. -> ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) )
264	263	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( T. -> ( CC _D ( log |` ( 1 ( ball ` ( abs o. - ) ) 1 ) ) ) = ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) )
265	251, 264	syl5reqr 2671	. . . . . . . . . . . . 13 |- ( T. -> ( CC _D ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` x ) ) ) = ( x e. ( 1 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / x ) ) )
266		fveq2 6191	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( log ` x ) = ( log ` ( 1 - y ) ) )
267		oveq2 6658	. . . . . . . . . . . . 13 |- ( x = ( 1 - y ) -> ( 1 / x ) = ( 1 / ( 1 - y ) ) )
268	200, 200, 213, 215, 224, 225, 250, 265, 266, 267	dvmptco 23735	. . . . . . . . . . . 12 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) )
269	200, 201, 202, 268	dvmptneg 23729	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) )
270	55, 76	reccld 10794	. . . . . . . . . . . . . . . 16 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. CC )
271		mulcom 10022	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 / ( 1 - y ) ) e. CC /\ -u 1 e. CC ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
272	270, 214, 271	sylancl 694	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( 1 - y ) ) ) )
273	270	mulm1d 10482	. . . . . . . . . . . . . . 15 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( -u 1 x. ( 1 / ( 1 - y ) ) ) = -u ( 1 / ( 1 - y ) ) )
274	272, 273	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u ( 1 / ( 1 - y ) ) )
275	274	negeqd 10275	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = -u -u ( 1 / ( 1 - y ) ) )
276	270	negnegd 10383	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u -u ( 1 / ( 1 - y ) ) = ( 1 / ( 1 - y ) ) )
277	275, 276	eqtrd 2656	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) = ( 1 / ( 1 - y ) ) )
278	277	mpteq2ia 4740	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( ( 1 / ( 1 - y ) ) x. -u 1 ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) )
279	269, 278	syl6eq 2672	. . . . . . . . . 10 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
280	279	dmeqd 5326	. . . . . . . . 9 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
281		dmmptg 5632	. . . . . . . . . 10 |- ( A. y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ( 1 / ( 1 - y ) ) e. _V -> dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
282		ovexd 6680	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( 1 / ( 1 - y ) ) e. _V )
283	281, 282	mprg 2926	. . . . . . . . 9 |- dom ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 )
284	280, 283	syl6eq 2672	. . . . . . . 8 |- ( T. -> dom ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( 0 ( ball ` ( abs o. - ) ) 1 ) )
285		sumex 14418	. . . . . . . . . . . 12 |- sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V
286	285	a1i 11	. . . . . . . . . . 11 |- ( ( T. /\ y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) e. _V )
287		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( n = k -> ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
288	287	cbvsumv 14426	. . . . . . . . . . . . . 14 |- sum_ n e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` n ) = sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k )
289	185, 288	syl6eq 2672	. . . . . . . . . . . . 13 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
290	289	mpteq2ia 4740	. . . . . . . . . . . 12 |- ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ k e. NN0 ( ( ( x e. CC |-> ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( x ^ j ) ) ) ) ` y ) ` k ) )
291		eqid 2622	. . . . . . . . . . . 12 |- ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` z ) + if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` z ) + if ( sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) e. RR , ( ( ( abs ` z ) + sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) / 2 ) , ( ( abs ` z ) + 1 ) ) ) / 2 ) )
292	100, 290, 109, 123, 187, 188, 291	pserdv2 24184	. . . . . . . . . . 11 |- ( T. -> ( CC _D ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
293	162	ssriv 3607	. . . . . . . . . . . 12 |- ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) )
294	293	a1i 11	. . . . . . . . . . 11 |- ( T. -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( j e. NN0 |-> ( if ( j = 0 , 0 , ( 1 / j ) ) x. ( r ^ j ) ) ) ) e. dom ~~> } , RR* , < ) ) ) )
295	200, 195, 286, 292, 294, 245, 239, 249	dvmptres 23726	. . . . . . . . . 10 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) )
296		nnnn0 11299	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. NN -> n e. NN0 )
297	296	adantl 482	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. NN0 )
298		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( m = 0 <-> n = 0 ) )
299		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = n -> ( 1 / m ) = ( 1 / n ) )
300	298, 299	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> if ( m = 0 , 0 , ( 1 / m ) ) = if ( n = 0 , 0 , ( 1 / n ) ) )
301		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 / n ) e. _V
302	93, 301	ifex 4156	. . . . . . . . . . . . . . . . . . . 20 |- if ( n = 0 , 0 , ( 1 / n ) ) e. _V
303	300, 92, 302	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN0 -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
304	297, 303	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = if ( n = 0 , 0 , ( 1 / n ) ) )
305		nnne0 11053	. . . . . . . . . . . . . . . . . . . . 21 |- ( n e. NN -> n =/= 0 )
306	305	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n =/= 0 )
307	306	neneqd 2799	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> -. n = 0 )
308	307	iffalsed 4097	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
309	304, 308	eqtrd 2656	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) = ( 1 / n ) )
310	309	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = ( n x. ( 1 / n ) ) )
311		nncn 11028	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> n e. CC )
312	311	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> n e. CC )
313	312, 306	recidd 10796	. . . . . . . . . . . . . . . 16 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( 1 / n ) ) = 1 )
314	310, 313	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) = 1 )
315	314	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( 1 x. ( y ^ ( n - 1 ) ) ) )
316		nnm1nn0 11334	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( n - 1 ) e. NN0 )
317		expcl 12878	. . . . . . . . . . . . . . . 16 |- ( ( y e. CC /\ ( n - 1 ) e. NN0 ) -> ( y ^ ( n - 1 ) ) e. CC )
318	53, 316, 317	syl2an 494	. . . . . . . . . . . . . . 15 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( y ^ ( n - 1 ) ) e. CC )
319	318	mulid2d 10058	. . . . . . . . . . . . . 14 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( 1 x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
320	315, 319	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) /\ n e. NN ) -> ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( y ^ ( n - 1 ) ) )
321	320	sumeq2dv 14433	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = sum_ n e. NN ( y ^ ( n - 1 ) ) )
322		nnuz 11723	. . . . . . . . . . . . . . 15 |- NN = ( ZZ>= ` 1 )
323		1e0p1 11552	. . . . . . . . . . . . . . . 16 |- 1 = ( 0 + 1 )
324	323	fveq2i 6194	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
325	322, 324	eqtri 2644	. . . . . . . . . . . . . 14 |- NN = ( ZZ>= ` ( 0 + 1 ) )
326		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( n = ( 1 + m ) -> ( n - 1 ) = ( ( 1 + m ) - 1 ) )
327	326	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( n = ( 1 + m ) -> ( y ^ ( n - 1 ) ) = ( y ^ ( ( 1 + m ) - 1 ) ) )
328		1zzd 11408	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 1 e. ZZ )
329		0zd 11389	. . . . . . . . . . . . . 14 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> 0 e. ZZ )
330	1, 325, 327, 328, 329, 318	isumshft 14571	. . . . . . . . . . . . 13 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) )
331		pncan2 10288	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ m e. CC ) -> ( ( 1 + m ) - 1 ) = m )
332	50, 102, 331	sylancr 695	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( ( 1 + m ) - 1 ) = m )
333	332	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( y ^ ( ( 1 + m ) - 1 ) ) = ( y ^ m ) )
334	333	sumeq2i 14429	. . . . . . . . . . . . 13 |- sum_ m e. NN0 ( y ^ ( ( 1 + m ) - 1 ) ) = sum_ m e. NN0 ( y ^ m )
335	330, 334	syl6eq 2672	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( y ^ ( n - 1 ) ) = sum_ m e. NN0 ( y ^ m ) )
336		geoisum 14608	. . . . . . . . . . . . 13 |- ( ( y e. CC /\ ( abs ` y ) < 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
337	53, 66, 336	syl2anc 693	. . . . . . . . . . . 12 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ m e. NN0 ( y ^ m ) = ( 1 / ( 1 - y ) ) )
338	321, 335, 337	3eqtrd 2660	. . . . . . . . . . 11 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) = ( 1 / ( 1 - y ) ) )
339	338	mpteq2ia 4740	. . . . . . . . . 10 |- ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN ( ( n x. ( ( m e. NN0 |-> if ( m = 0 , 0 , ( 1 / m ) ) ) ` n ) ) x. ( y ^ ( n - 1 ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) )
340	295, 339	syl6eq 2672	. . . . . . . . 9 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) = ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> ( 1 / ( 1 - y ) ) ) )
341	279, 340	eqtr4d 2659	. . . . . . . 8 |- ( T. -> ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ) = ( CC _D ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ) )
342		blcntr 22218	. . . . . . . . . 10 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR+ ) -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
343	38, 28, 39, 342	mp3an 1424	. . . . . . . . 9 |- 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 )
344	343	a1i 11	. . . . . . . 8 |- ( T. -> 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
345		oveq2 6658	. . . . . . . . . . . . . . . 16 |- ( y = 0 -> ( 1 - y ) = ( 1 - 0 ) )
346		1m0e1 11131	. . . . . . . . . . . . . . . 16 |- ( 1 - 0 ) = 1
347	345, 346	syl6eq 2672	. . . . . . . . . . . . . . 15 |- ( y = 0 -> ( 1 - y ) = 1 )
348	347	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( y = 0 -> ( log ` ( 1 - y ) ) = ( log ` 1 ) )
349		log1 24332	. . . . . . . . . . . . . 14 |- ( log ` 1 ) = 0
350	348, 349	syl6eq 2672	. . . . . . . . . . . . 13 |- ( y = 0 -> ( log ` ( 1 - y ) ) = 0 )
351	350	negeqd 10275	. . . . . . . . . . . 12 |- ( y = 0 -> -u ( log ` ( 1 - y ) ) = -u 0 )
352		neg0 10327	. . . . . . . . . . . 12 |- -u 0 = 0
353	351, 352	syl6eq 2672	. . . . . . . . . . 11 |- ( y = 0 -> -u ( log ` ( 1 - y ) ) = 0 )
354	353, 80, 93	fvmpt 6282	. . . . . . . . . 10 |- ( 0 e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
355	343, 354	mp1i 13	. . . . . . . . 9 |- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` 0 ) = 0 )
356		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( 0 x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
357	356	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( 0 = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 0 x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
358		oveq1 6657	. . . . . . . . . . . . . . 15 |- ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) )
359	358	eqeq1d 2624	. . . . . . . . . . . . . 14 |- ( ( 1 / n ) = if ( n = 0 , 0 , ( 1 / n ) ) -> ( ( ( 1 / n ) x. ( y ^ n ) ) = 0 <-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 ) )
360		simpll 790	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y = 0 )
361	360, 28	syl6eqel 2709	. . . . . . . . . . . . . . . 16 |- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> y e. CC )
362		simplr 792	. . . . . . . . . . . . . . . 16 |- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> n e. NN0 )
363	361, 362	expcld 13008	. . . . . . . . . . . . . . 15 |- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( y ^ n ) e. CC )
364	363	mul02d 10234	. . . . . . . . . . . . . 14 |- ( ( ( y = 0 /\ n e. NN0 ) /\ n = 0 ) -> ( 0 x. ( y ^ n ) ) = 0 )
365		simpll 790	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> y = 0 )
366	365	oveq1d 6665	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = ( 0 ^ n ) )
367		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y = 0 /\ n e. NN0 ) -> n e. NN0 )
368	367, 14	sylib 208	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y = 0 /\ n e. NN0 ) -> ( n e. NN \/ n = 0 ) )
369	368	ord 392	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y = 0 /\ n e. NN0 ) -> ( -. n e. NN -> n = 0 ) )
370	369	con1d 139	. . . . . . . . . . . . . . . . . . 19 |- ( ( y = 0 /\ n e. NN0 ) -> ( -. n = 0 -> n e. NN ) )
371	370	imp 445	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
372	371	0expd 13024	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 0 ^ n ) = 0 )
373	366, 372	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( y ^ n ) = 0 )
374	373	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = ( ( 1 / n ) x. 0 ) )
375	371	nnrecred 11066	. . . . . . . . . . . . . . . . 17 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. RR )
376	375	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( 1 / n ) e. CC )
377	376	mul01d 10235	. . . . . . . . . . . . . . 15 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. 0 ) = 0 )
378	374, 377	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( y = 0 /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( 1 / n ) x. ( y ^ n ) ) = 0 )
379	357, 359, 364, 378	ifbothda 4123	. . . . . . . . . . . . 13 |- ( ( y = 0 /\ n e. NN0 ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
380	379	sumeq2dv 14433	. . . . . . . . . . . 12 |- ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = sum_ n e. NN0 0 )
381	1	eqimssi 3659	. . . . . . . . . . . . . 14 |- NN0 C_ ( ZZ>= ` 0 )
382	381	orci 405	. . . . . . . . . . . . 13 |- ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin )
383		sumz 14453	. . . . . . . . . . . . 13 |- ( ( NN0 C_ ( ZZ>= ` 0 ) \/ NN0 e. Fin ) -> sum_ n e. NN0 0 = 0 )
384	382, 383	ax-mp 5	. . . . . . . . . . . 12 |- sum_ n e. NN0 0 = 0
385	380, 384	syl6eq 2672	. . . . . . . . . . 11 |- ( y = 0 -> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = 0 )
386	385, 197, 93	fvmpt 6282	. . . . . . . . . 10 |- ( 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 )
387	343, 386	mp1i 13	. . . . . . . . 9 |- ( T. -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) ) ` 0 ) = 0 )
388	355, 387	eqtr4d 2659	. . . . . . . 8 |- ( 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 ) )
389	47, 48, 49, 81, 198, 284, 341, 344, 388	dv11cn 23764	. . . . . . 7 |- ( 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 ) ) ) )
390	389	fveq1d 6193	. . . . . 6 |- ( 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 ) )
391	46, 390	mp1i 13	. . . . 5 |- ( 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 ) )
392		oveq2 6658	. . . . . . . 8 |- ( y = A -> ( 1 - y ) = ( 1 - A ) )
393	392	fveq2d 6195	. . . . . . 7 |- ( y = A -> ( log ` ( 1 - y ) ) = ( log ` ( 1 - A ) ) )
394	393	negeqd 10275	. . . . . 6 |- ( y = A -> -u ( log ` ( 1 - y ) ) = -u ( log ` ( 1 - A ) ) )
395		negex 10279	. . . . . 6 |- -u ( log ` ( 1 - A ) ) e. _V
396	394, 80, 395	fvmpt 6282	. . . . 5 |- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> ( ( y e. ( 0 ( ball ` ( abs o. - ) ) 1 ) |-> -u ( log ` ( 1 - y ) ) ) ` A ) = -u ( log ` ( 1 - A ) ) )
397		oveq1 6657	. . . . . . . 8 |- ( y = A -> ( y ^ n ) = ( A ^ n ) )
398	397	oveq2d 6666	. . . . . . 7 |- ( y = A -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( y ^ n ) ) = ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
399	398	sumeq2sdv 14435	. . . . . 6 |- ( 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 ) ) )
400		sumex 14418	. . . . . 6 |- sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) e. _V
401	399, 197, 400	fvmpt 6282	. . . . 5 |- ( 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 ) ) )
402	391, 396, 401	3eqtr3d 2664	. . . 4 |- ( A e. ( 0 ( ball ` ( abs o. - ) ) 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
403	45, 402	syl 17	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> -u ( log ` ( 1 - A ) ) = sum_ n e. NN0 ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
404	26, 403	breqtrrd 4681	. 2 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) ~~> -u ( log ` ( 1 - A ) ) )
405		seqex 12803	. . . 4 |- seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V
406	405	a1i 11	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ) e. _V )
407		seqex 12803	. . . 4 |- seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) e. _V
408	407	a1i 11	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) e. _V )
409		1zzd 11408	. . 3 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ZZ )
410		elnnuz 11724	. . . . . 6 |- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
411		fvres 6207	. . . . . 6 |- ( 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 ) )
412	410, 411	sylbi 207	. . . . 5 |- ( 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 ) )
413	412	eqcomd 2628	. . . 4 |- ( 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 ) )
414		addid2 10219	. . . . . . . 8 |- ( n e. CC -> ( 0 + n ) = n )
415	414	adantl 482	. . . . . . 7 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. CC ) -> ( 0 + n ) = n )
416		0cnd 10033	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. CC )
417		1eluzge0 11732	. . . . . . . 8 |- 1 e. ( ZZ>= ` 0 )
418	417	a1i 11	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ( ZZ>= ` 0 ) )
419		0cnd 10033	. . . . . . . . . . 11 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ k = 0 ) -> 0 e. CC )
420		nn0cn 11302	. . . . . . . . . . . . 13 |- ( k e. NN0 -> k e. CC )
421	420	adantl 482	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> k e. CC )
422		df-ne 2795	. . . . . . . . . . . . 13 |- ( k =/= 0 <-> -. k = 0 )
423	422	biimpri 218	. . . . . . . . . . . 12 |- ( -. k = 0 -> k =/= 0 )
424		reccl 10692	. . . . . . . . . . . 12 |- ( ( k e. CC /\ k =/= 0 ) -> ( 1 / k ) e. CC )
425	421, 423, 424	syl2an 494	. . . . . . . . . . 11 |- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ -. k = 0 ) -> ( 1 / k ) e. CC )
426	419, 425	ifclda 4120	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> if ( k = 0 , 0 , ( 1 / k ) ) e. CC )
427		expcl 12878	. . . . . . . . . . 11 |- ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
428	427	adantlr 751	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
429	426, 428	mulcld 10060	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. CC )
430	429, 8	fmptd 6385	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) : NN0 --> CC )
431		1nn0 11308	. . . . . . . 8 |- 1 e. NN0
432		ffvelrn 6357	. . . . . . . 8 |- ( ( ( 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 )
433	430, 431, 432	sylancl 694	. . . . . . 7 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 1 ) e. CC )
434		elfz1eq 12352	. . . . . . . . . 10 |- ( n e. ( 0 ... 0 ) -> n = 0 )
435		1m1e0 11089	. . . . . . . . . . 11 |- ( 1 - 1 ) = 0
436	435	oveq2i 6661	. . . . . . . . . 10 |- ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
437	434, 436	eleq2s 2719	. . . . . . . . 9 |- ( n e. ( 0 ... ( 1 - 1 ) ) -> n = 0 )
438	437	fveq2d 6195	. . . . . . . 8 |- ( 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 ) )
439		0nn0 11307	. . . . . . . . . 10 |- 0 e. NN0
440		iftrue 4092	. . . . . . . . . . . 12 |- ( k = 0 -> if ( k = 0 , 0 , ( 1 / k ) ) = 0 )
441		oveq2 6658	. . . . . . . . . . . 12 |- ( k = 0 -> ( A ^ k ) = ( A ^ 0 ) )
442	440, 441	oveq12d 6668	. . . . . . . . . . 11 |- ( k = 0 -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( 0 x. ( A ^ 0 ) ) )
443		ovex 6678	. . . . . . . . . . 11 |- ( 0 x. ( A ^ 0 ) ) e. _V
444	442, 8, 443	fvmpt 6282	. . . . . . . . . 10 |- ( 0 e. NN0 -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) ) )
445	439, 444	ax-mp 5	. . . . . . . . 9 |- ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = ( 0 x. ( A ^ 0 ) )
446		expcl 12878	. . . . . . . . . . 11 |- ( ( A e. CC /\ 0 e. NN0 ) -> ( A ^ 0 ) e. CC )
447	27, 439, 446	sylancl 694	. . . . . . . . . 10 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 0 ) e. CC )
448	447	mul02d 10234	. . . . . . . . 9 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 0 x. ( A ^ 0 ) ) = 0 )
449	445, 448	syl5eq 2668	. . . . . . . 8 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( k e. NN0 |-> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) ` 0 ) = 0 )
450	438, 449	sylan9eqr 2678	. . . . . . 7 |- ( ( ( 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 )
451	415, 416, 418, 433, 450	seqid 12846	. . . . . 6 |- ( ( 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 ) ) ) ) )
452	305	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n =/= 0 )
453	452	neneqd 2799	. . . . . . . . . . . 12 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> -. n = 0 )
454	453	iffalsed 4097	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> if ( n = 0 , 0 , ( 1 / n ) ) = ( 1 / n ) )
455	454	oveq1d 6665	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( 1 / n ) x. ( A ^ n ) ) )
456	296, 23	sylan2 491	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( A ^ n ) e. CC )
457	311	adantl 482	. . . . . . . . . . 11 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> n e. CC )
458	456, 457, 452	divrec2d 10805	. . . . . . . . . 10 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( A ^ n ) / n ) = ( ( 1 / n ) x. ( A ^ n ) ) )
459	455, 458	eqtr4d 2659	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( ( A ^ n ) / n ) )
460	296, 11	sylan2 491	. . . . . . . . 9 |- ( ( ( 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 ) ) )
461		id 22	. . . . . . . . . . . 12 |- ( k = n -> k = n )
462	6, 461	oveq12d 6668	. . . . . . . . . . 11 |- ( k = n -> ( ( A ^ k ) / k ) = ( ( A ^ n ) / n ) )
463		eqid 2622	. . . . . . . . . . 11 |- ( k e. NN |-> ( ( A ^ k ) / k ) ) = ( k e. NN |-> ( ( A ^ k ) / k ) )
464		ovex 6678	. . . . . . . . . . 11 |- ( ( A ^ n ) / n ) e. _V
465	462, 463, 464	fvmpt 6282	. . . . . . . . . 10 |- ( n e. NN -> ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
466	465	adantl 482	. . . . . . . . 9 |- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN ) -> ( ( k e. NN |-> ( ( A ^ k ) / k ) ) ` n ) = ( ( A ^ n ) / n ) )
467	459, 460, 466	3eqtr4d 2666	. . . . . . . 8 |- ( ( ( 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 ) )
468	410, 467	sylan2br 493	. . . . . . 7 |- ( ( ( 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 ) )
469	409, 468	seqfeq 12826	. . . . . 6 |- ( ( 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 ) ) ) )
470	451, 469	eqtrd 2656	. . . . 5 |- ( ( 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 ) ) ) )
471	470	fveq1d 6193	. . . 4 |- ( ( 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 ) )
472	413, 471	sylan9eqr 2678	. . 3 |- ( ( ( 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 ) )
473	322, 406, 408, 409, 472	climeq 14298	. 2 |- ( ( 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 ) ) ) )
474	404, 473	mpbid 222	1 |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   T. wtru 1484   e. wcel 1990   =/= wne 2794   A.wral 2912   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   ifcif 4086   {csn 4177   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   Fincfn 7955   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZ>=cuz 11687   RR+crp 11832   (,]cioc 12176   [,)cico 12177   [,]cicc 12178   ...cfz 12326   seqcseq 12801   ^cexp 12860   abscabs 13974   ~~> cli 14215   sum_csu 14416   ↾_t crest 16081   TopOpenctopn 16082   *Metcxmt 19731   ballcbl 19733  ℂ_fldccnfld 19746   Topctop 20698   -cn->ccncf 22679   _D cdv 23627   logclog 24301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-tan 14802  df-pi 14803  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631  df-ulm 24131  df-log 24303

This theorem is referenced by:  logtaylsum  24407  logtayl2  24408  atantayl  24664  stirlinglem5  40295