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

Metamath Proof Explorer

Theorem logtayl

Proof