logtayl

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

		Ref	Expression
	Assertion	logtayl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (k \in ℕ ⟼ \frac{A^{k}}{k})) ⇝ (- \log (1 - A))$

Proof

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

Metamath Proof Explorer

Theorem logtayl

Proof